smtinterpol
smtinterpol copied to clipboard
ultimate-pa
SMTInterpol interpolating SMT solver
Hi, for the following formula ~~~~ (set-logic LRA) (declare-fun y2 () Real) (declare-fun y3 () Real) (declare-fun y4 () Real) (declare-fun x1 () Real) (declare-fun y1 () Real) (assert (or...
Hi, for the following formula ~~~~ (set-logic HORN) (declare-fun ULTIMATE.start_L7 (Int Int Int Int Int Int Int Int Bool) Bool) (declare-fun ULTIMATE.start_L23 (Int Int Int Int Int Int Int Int...
Hi, for the following formula, [927.txt](https://github.com/ultimate-pa/smtinterpol/files/5273581/927.txt) smtinterpol d208e931d9 ~~~~ Exception in thread "main" java.lang.AssertionError: Unknown proof rule @assumption. at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.FixResolutionProof.walk(FixResolutionProof.java:227) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.FixResolutionProof$ProofWalker.walk(FixResolutionProof.java:70) at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:115) at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:106) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.FixResolutionProof.fix(FixResolutionProof.java:189) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.ProofTermGenerator.convert(ProofTermGenerator.java:150)...
While running the tests testMusEnumerationScriptSet2" or "testMusEnumerationScriptSet5" in MusesTest.java, an error occurred in the SmtInterpol(SmtInterpol other, , final Map options, final OptionMap.CopyMode mode) constructor: java.lang.AssertionError at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.ProofTracker.buildProof(ProofTracker.java:54) at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.ProofTracker.auxAxiom(ProofTracker.java:206) at...
Hi, for the following formula, [1904.txt](https://github.com/ultimate-pa/smtinterpol/files/4883215/1904.txt) smtinterpol commit cb90e74 ~~~~ Exception in thread "main" java.lang.AssertionError: Not an assumption in unsat clause at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.checkValidUnsatClause(DPLLEngine.java:1904) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.getProof(DPLLEngine.java:1491) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.retrieveProof(SMTInterpol.java:1159) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getProof(SMTInterpol.java:791) at...
Hi, for the following formula, [693.txt](https://github.com/ultimate-pa/smtinterpol/files/4883057/693.txt) smtinterpol commit cb90e74 ~~~~ Exception in thread "main" java.lang.AssertionError at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explainConflict(DPLLEngine.java:693) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explain(DPLLEngine.java:854) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.access$100(DPLLEngine.java:56) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine$AllSatIterator.hasNext(DPLLEngine.java:1791) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SExpression.convertSexp(SExpression.java:58) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SExpression.toString(SExpression.java:82) at java.lang.String.valueOf(String.java:2994) at...
Hi, for the following formula, [147.txt](https://github.com/ultimate-pa/smtinterpol/files/4882976/147.txt) smtinterpol commit cb90e74 ~~~~ sat ( (IP_18 IP_4 IP_27 IP_10 IP_15) ) () () () () Exception in thread "main" java.lang.AssertionError at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.ProofTermGenerator.convert(ProofTermGenerator.java:147) at...
Hi, for the following formula, [704.txt](https://github.com/ultimate-pa/smtinterpol/files/4882962/704.txt) smtinterpol commit cb90e74 ~~~~ sat Exception in thread "main" java.lang.AssertionError at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explainConflict(DPLLEngine.java:704) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.explain(DPLLEngine.java:854) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine.access$100(DPLLEngine.java:56) at de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.DPLLEngine$AllSatIterator.hasNext(DPLLEngine.java:1791) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SExpression.convertSexp(SExpression.java:58) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SExpression.toString(SExpression.java:82) at java.lang.String.valueOf(String.java:2994)...
Hi, for the following formula, ~~~~ (set-logic ALL) (set-info :status sat) (declare-datatypes ((t1 1)) ((par (T1) ((mkt1 (p1 T1)))))) (declare-datatypes ((t2 1)) ((par (T1) ((mkt2 (p1 T1)))))) (define-fun s1 ()...
Hi, for the following formulas, [NPD.txt](https://github.com/ultimate-pa/smtinterpol/files/4494010/NPD.txt) [NPD2.txt](https://github.com/ultimate-pa/smtinterpol/files/4494011/NPD2.txt) smtinterpol commit 0610d35 throws a NPD