search

ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver
GNU Lesser General Public License v3.0
60 stars 17 forks source link

Another AssertionError with check-sat-assuming #40

Open kfriedberger opened 5 years ago

kfriedberger commented 5 years ago

The following snipped causes SMTInterpol (453d36e342e90aae7b5942e519ea73ce3c93219a) to fail with an AssertionError:

SMTInterpol env = new SMTInterpol(new DefaultLogger(), () -> false);
env.setLogic(Logics.QF_AUFLIRA);
env.declareFun("A", new Sort[] {}, env.getTheory().getBooleanSort());
Term[] terms = new Term[] {env.term("A")};
env.checkSatAssuming(terms);
env.checkSat();
env.checkSatAssuming(terms);

Stacktrace:

Exception in thread "main" java.lang.AssertionError
at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.assume(DPLLEngine.java:1877)
at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:492)

Strangely, the corresponding SMTlib-input does not trigger the problem:

(set-logic QF_AUFLIRA)
(declare-fun A () Bool)
(check-sat-assuming (A))
(check-sat)
(check-sat-assuming (A))

This issue might be related to #29.

kfriedberger commented 4 years ago

This issue seems to not be fixed until today. Is there any progress?