search

ultimate-pa / smtinterpol

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

AssertionError at ProofTermGenerator.java:161 #136

Closed daniel-larraz closed 1 year ago

daniel-larraz commented 1 year ago

For the following SMT script (smtinterpol_itp.txt), I get the following error:

(error "smtinterpol_itp.txt:302:23: java.lang.NullPointerException")

When I enable assertions (java -ea), I get this stacktrace:

Exception in thread "main" java.lang.AssertionError
    at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.ProofTermGenerator.convert(ProofTermGenerator.java:161)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getProof(SMTInterpol.java:761)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:773)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2937)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1321)
    at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:120)
    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)

SMTInterpol version: 2.5-1245-g74d3ff5c

jhoenicke commented 1 year ago

You need to set the option (set-option :produce-interpolants true) at the beginning of the script before set-logic. There was a better error message in the past but that error message was broken by some recent changes. I'll fix the error message, so that it's clear that the option is missing.