search

ultimate-pa / smtinterpol

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

NullPointerException at ParseEnvironment.java:122 (produce-models, model-check-mode) #103

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance, 122npe.txt

smtinterpol 7020e26 throws a NPE

Unexpected Exception: java.lang.NullPointerException                                                                                                                                                [3/1882]
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: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:153)
Caused by: java.lang.NullPointerException
        at de.uni_freiburg.informatik.ultimate.logic.Theory.term(Theory.java:1576)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ArrayTheory.fillInModel(ArrayTheory.java:974)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ModelBuilder.<init>(ModelBuilder.java:47)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure.fillInModel(CClosure.java:1312)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.model.Model.<init>(Model.java:120)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSatAssuming(SMTInterpol.java:489)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.checkSat(SMTInterpol.java:435)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2870)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1317)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)