search

ultimate-pa / smtinterpol

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

Triggered NPE in ParseEnvironment.java:122 #125

Closed ErrReporter closed 3 years ago

ErrReporter commented 3 years ago

Hi,

for this formula:

(set-option :print-success false)
(set-option :produce-interpolants true)
(set-logic QF_UFLIA)
(declare-const lock Bool) (declare-const lock1 Bool)
(declare-const lock2 Bool) (declare-const lock3 Bool)
(declare-const old Int) (declare-const old1 Int)
(declare-const new Int) (declare-const new1 Int)
(declare-const new2 Int)
(assert (! (= lock true) :named L1))
(assert (! (= old new) :named L2))
(assert (! (= lock1 false) :named L3))
(assert (! (= new1 (+ new 1)) :named L4))
(assert (! (not (= old new1)) :named L5))
(assert (! (= lock2 true) :named L11))
(assert (! (= old1 new1) :named L21))
(assert (! (= lock3 false) :named L31))
(assert (! (= new2 (+ new1 1)) :named L41))
(assert (! (= new2 old1) :named L51))
(assert (! (not lock3) :named L6))
(check-sat)
(get-interpolants L1 L2 L3 L4 L5 L11 L21 L31 L41 L51 L6)

It generates an NPE exception:

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: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 by: java.lang.NullPointerException
    at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.colorTermsInAssertions(Interpolator.java:603)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:220)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:876)
    at de.uni_freiburg.informatik.ultimate.logic.NoopScript.getInterpolants(NoopScript.java:392)
    at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2933)
    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)

Commit: eab6c41e4af2ca7cff922da33e3e2a95c8e36c70