smtinterpol

smtinterpol copied to clipboard

AssertionError at Interpolator.java:757 (incomplete fix)

1

Related: https://github.com/ultimate-pa/smtinterpol/issues/74 --- Hi, for the following formula, [757.txt](https://github.com/ultimate-pa/smtinterpol/files/4584631/757.txt) smtinterpol commit f15aa2170 throws an assertion error ~~~~ unsat Exception in thread "main" java.lang.AssertionError: Mixed Literal with only one subterm: r1...

rainoftime

Hi, for the following formula, [cast.txt](https://github.com/ultimate-pa/smtinterpol/files/4496726/cast.txt) smtinterpol commit 0610d35 throws a ClassCastException ~~~~ Unexpected Exception: java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.logic.QuantifiedFormula cannot be cast to de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm ~~~~

rainoftime

ClassCastException on UF formula (get-proof)

1

Hi, for the following formula, ~~~~ (set-option :produce-proofs true) (set-logic UF) (declare-const v2 Bool) (assert (! (forall ((q0 Bool) (q1 Bool) (q2 Bool)) v2) :named IP_1)) (assert (! (not (forall...

rainoftime

Related and fixed https://github.com/ultimate-pa/smtinterpol/issues/76 ---- Hi, for the following formulas, [xx.txt](https://github.com/ultimate-pa/smtinterpol/files/4533410/xx.txt) [1514.txt](https://github.com/ultimate-pa/smtinterpol/files/4533345/1514.txt) SMTInterpol (commit 7625fe26c8f2) throws an AssertionError ~~~~ Exception in thread "main" java.lang.AssertionError at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.generateLevel0Proof(DPLLEngine.java:1514) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.setLiteral(DPLLEngine.java:457) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateClauses(DPLLEngine.java:402)...

rainoftime

AssertionError at DPLLEngine.java:1567

1

Hi, for the following formula, [1567.txt](https://github.com/ultimate-pa/smtinterpol/files/4534595/1567.txt) SMTInterpol 7625fe26c8f throws an assertion error ~~~~ Exception in thread "main" java.lang.AssertionError at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.getLevel0(DPLLEngine.java:1567) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explainConflict(DPLLEngine.java:810) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explain(DPLLEngine.java:854) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.solve(DPLLEngine.java:1201) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol$CheckType$1.check(SMTInterpol.java:113) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:476)...

rainoftime

AssertionError at DPLLEngine.java:1558

1

Hi, for the following formula, [1558.txt](https://github.com/ultimate-pa/smtinterpol/files/4534619/1558.txt) SMTInterpol 7625fe2 throws an assertion error ~~~~ Exception in thread "main" java.lang.AssertionError [6/1935] at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkLevel0Clause(DPLLEngine.java:1558) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.getLevel0(DPLLEngine.java:1568) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.generateLevel0Proof(DPLLEngine.java:1527) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.setLiteral(DPLLEngine.java:457) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.propagateClauses(DPLLEngine.java:402) at...

rainoftime

Hi, for the following formula, [105.txt](https://github.com/ultimate-pa/smtinterpol/files/4533444/105.txt) SMTInterpol (commit 7625fe2) throws an AssertionError ~~~~ sat Exception in thread "main" java.lang.AssertionError at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.EqualityProxy.createCCEquality(EqualityProxy.java:105) at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure.createEquality(CClosure.java:1015) at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.WeakCongruencePath.generateClause(WeakCongruencePath.java:368) at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.WeakCongruencePath.computeWeakeqExt(WeakCongruencePath.java:146) at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ArrayTheory.computeWeakeqExt(ArrayTheory.java:1419) at...

rainoftime

Another AssertionError with check-sat-assuming

1

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...

kfriedberger

C API

1

Not a bug, more of a feature request. Is there any plans of providing a C API to the solver? For integration into tools implemented in other languages C would...

dddejan

Performance of FunctionSymbol.checkSort

2

In our application, we construct huge formulas where already the construction process takes thousands of seconds. The function [FunctionSymbol.checkSort](https://github.com/ultimate-pa/smtinterpol/blob/master/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/FunctionSymbol.java#L177) is a huge bottleneck in this case. Is the .toString() for...

stahlbauer