interpolation can only be done over previously asserted formulas when re-adding constraints

[leventeBajczi]

Following my discussion with @baierd, I'm providing a (somewhat) minimal working example for the bug where re-adding the same constraint twice makes it impossible to query interpolants.

Setup: add one constraint (A), add a second constraint (B1) making the system UNSAT, then re-add the second constraint (B2), and query interpolants between either A and B1, or A and B2.
Experienced behavior: Some solvers report interpolation can only be done over previously asserted formulas.
Expected behavior: Re-adding constraints should not interfere with the ability to calculate interpolants.

The affected solvers (What I think are considered bugs are in bold):

	OpenSMT	Yices2	Z3	MathSAT5	SMTInterpol	Princess	Boolector	CVC5	CVC4
test 1	error	no itp	no itp	FAIL	FAIL	FAIL	no itp	FAIL	no itp
test 2	error	no itp	no itp	PASS	PASS	PASS	no itp	PASS	no itp
test 3	error	no itp	no itp	PASS	FAIL	FAIL	no itp	PASS	no itp

I would separately emphasize the third test's success with MATHSAT5 and CVC5, which makes it even harder to understand what's happening.

The reproduction test (junit5):

    public static Stream<Arguments> data() {
        return Arrays.stream(Solvers.values()).map(Arguments::of);
    }

    static SolverContext createSolver(Solvers solver) throws InvalidConfigurationException {
        Configuration config = Configuration.defaultConfiguration();
        LogManager logger = BasicLogManager.create(config);
        ShutdownManager shutdown = ShutdownManager.create();

        SolverContext context = SolverContextFactory.createSolverContext(
                config, logger, shutdown.getNotifier(), solver);
        return context;
    }

    @ParameterizedTest
    @MethodSource("data")
    void first(Solvers solver) throws InterruptedException, SolverException, InvalidConfigurationException {
        SolverContext context = createSolver(solver);
        InterpolatingProverEnvironment prover = context.newProverEnvironmentWithInterpolation(ProverOptions.GENERATE_MODELS);

        var ifm = context.getFormulaManager().getIntegerFormulaManager();
        var x = ifm.makeVariable("x");
        var one = ifm.makeNumber(1);

        var eqT = prover.addConstraint(ifm.equal(one, x));
        var ltT1 = prover.addConstraint(ifm.lessThan(one, x));
        var ltT2 = prover.addConstraint(ifm.lessThan(one, x));
        Assertions.assertTrue(prover.isUnsat());

        Assertions.assertDoesNotThrow(() -> prover.getSeqInterpolants0(ImmutableList.of(eqT, ltT1)));
    }

    @ParameterizedTest
    @MethodSource("data")
    void second(Solvers solver) throws InterruptedException, SolverException, InvalidConfigurationException {
        SolverContext context = createSolver(solver);
        InterpolatingProverEnvironment prover = context.newProverEnvironmentWithInterpolation(ProverOptions.GENERATE_MODELS);

        var ifm = context.getFormulaManager().getIntegerFormulaManager();
        var x = ifm.makeVariable("x");
        var one = ifm.makeNumber(1);

        var eqT = prover.addConstraint(ifm.equal(one, x));
        var ltT1 = prover.addConstraint(ifm.lessThan(one, x));
        var ltT2 = prover.addConstraint(ifm.lessThan(one, x));
        Assertions.assertTrue(prover.isUnsat());

        Assertions.assertDoesNotThrow(() -> prover.getSeqInterpolants0(ImmutableList.of(eqT, ltT2)));
    }

    @ParameterizedTest
    @MethodSource("data")
    void third(Solvers solver) throws InterruptedException, SolverException, InvalidConfigurationException {
        SolverContext context = createSolver(solver);
        InterpolatingProverEnvironment prover = context.newProverEnvironmentWithInterpolation(ProverOptions.GENERATE_MODELS);

        var ifm = context.getFormulaManager().getIntegerFormulaManager();
        var x = ifm.makeVariable("x");
        var one = ifm.makeNumber(1);

        var eqT = prover.addConstraint(ifm.equal(one, x));
        var ltT1 = prover.addConstraint(ifm.lessThan(one, x));
        var ltT2 = prover.addConstraint(ifm.lessThan(one, x));
        Assertions.assertTrue(prover.isUnsat());

        Assertions.assertDoesNotThrow(() -> prover.getInterpolant(ImmutableList.of(eqT)));
    }