smtinterpol
smtinterpol copied to clipboard
ultimate-pa
SMTInterpol interpolating SMT solver
Hi @jhoenicke, while playing around with SMTInterpol and quantifiers, I found the following funny example: ``` (set-logic UF) (declare-sort Unit 0) (assert (forall ((u0 Unit) (u1 Unit)) (= u0 u1)))...
We have found a simple and long SMT query ([smt_278.zip](https://github.com/ultimate-pa/smtinterpol/files/9847438/smt_278.zip)) where SMTInterpol needs more time than expected. *What would one 'expect' from SMT solving, which is by definition a computationally...
Running SMTInterpol on this SMT script ([bmc.txt](https://github.com/ultimate-pa/smtinterpol/files/9758421/bmc.txt)) triggers the following error: ``` Unexpected Exception: java.lang.NullPointerException Exception in thread "main" de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: java.lang.NullPointerException at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:123) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:99) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:35) at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:178) Caused...
Using the following (already reduced) test file, SMTInterpol 2.1-335-g4c543a5 produces an AssertionError: (set-logic QF_UFLIA) (declare-fun g0 () Bool) (declare-fun a (Int Int) Bool) (define-fun b ((t Int)) Int (+ (+...
Hello, Our static analyses found a following potential NPE: 1. Return null to caller https://github.com/ultimate-pa/smtinterpol/blob/828ec76df5a88e07883a616002688ad6f2d8a184/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Theory.java#L1579 2. Return the return value of function term to caller https://github.com/ultimate-pa/smtinterpol/blob/828ec76df5a88e07883a616002688ad6f2d8a184/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/dpll/Clause.java#L292 3. Function toTerm executes...
Hi, for the following formula, smtinterpol https://github.com/ultimate-pa/smtinterpol/commit/47ca37869cd94298f7e3fa3f0c642e854d73c24b [292.txt](https://github.com/ultimate-pa/smtinterpol/files/5616872/292.txt) ~~~~ sat Exception in thread "main" java.lang.AssertionError at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm.unshare(CCTerm.java:292) at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.pop(Clausifier.java:2047) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.pop(SMTInterpol.java:443) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2806) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1317) at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:119)...
Hi, for the following formula, [1022.txt](https://github.com/ultimate-pa/smtinterpol/files/4888957/1022.txt) smtinterpol commit 4e106c2bb ~~~~ Exception in thread "main" java.lang.AssertionError [7/1996] at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.shareCCTerm(Clausifier.java:1022) at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier$CCTermBuilder$SaveCCTerm.perform(Clausifier.java:147) at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier$CCTermBuilder.convert(Clausifier.java:182) at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.addTermAxioms(Clausifier.java:1038) at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createLinVar(Clausifier.java:1124) at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createMutableAffinTerm(Clausifier.java:1140) at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.createLeq0(Clausifier.java:2066)...
Hi, for the following formula, [arr.txt](https://github.com/ultimate-pa/smtinterpol/files/4882941/arr.txt) smtinterpol commit cb90e74 ~~~~ Unexpected Exception: java.lang.ArrayIndexOutOfBoundsException: 4 Exception in thread "main" de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: java.lang.ArrayIndexOutOfBoundsException: 4 at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:122) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:98) at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:35) at de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:165) Caused...