ultimate-pa / smtinterpol

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

NullPointerException for incremental NIA instance #53

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance

(set-logic NIA)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v5 () Bool)
(declare-fun v11 () Bool)
(declare-fun v12 () Bool)
(declare-fun v17 () Bool)
(declare-fun v18 () Bool)
(declare-fun i2 () Int)
(declare-fun i3 () Int)
(declare-fun i4 () Int)
(push 1)
(assert (exists ((q0 Int) (q1 Bool) (q2 Bool) (q3 Int)) (=> (or v17 q1 q2 q2 v0) (< q3 q0))))
(declare-fun v20 () Bool)
(assert (not (exists ((q4 Bool) (q5 Bool)) (= (< 35 i4) v0 v12))))
(assert (or (forall ((q4 Bool) (q5 Bool)) v18) (exists ((q4 Bool) (q5 Bool)) (not (or v5 q5 q5 q4 q5)))))
(declare-fun v21 () Bool)
(assert (forall ((q6 Bool)) (not (xor q6 v0 q6 v11 q6 q6 (or v21 (> i4 29) v21 v12) (< 35 i4) q6))))
(push 1)
(assert (not (exists ((q7 Int)) (> i4 29))))
(pop 1)
(check-sat)

smtinterpol (commit 3f24148) throws a NullPointerException

Unexpected Exception: java.lang.NullPointerException
(error "java.lang.NullPointerException")

Not sure if the root cause is the same with https://github.com/ultimate-pa/smtinterpol/issues/50

rainoftime commented 4 years ago

Appended to https://github.com/ultimate-pa/smtinterpol/issues/50