search

ultimate-pa / smtinterpol

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

IndexOutOfBoundsException for incremental LIA instance #58

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-logic LIA) 
(declare-fun v4 () Bool)
(declare-fun v7 () Bool)
(declare-fun v10 () Bool)
(assert (not (exists ((q0 Bool) (q1 Int) (q2 Bool) (q3 Int)) (not (>= 6 q3)))))
(push 1)
(assert (xor v7 v10 (= v4 v7 ) v4 (not v10)))
(pop 1)
(check-sat)

smtinterpol (commit 3f24148) throws an IndexOutOfBoundsException

Unexpected Exception: java.lang.IndexOutOfBoundsException: Index: 0, Size: 0
(error "java.lang.IndexOutOfBoundsException: Index: 0, Size: 0")
rainoftime commented 4 years ago

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