search

usi-verification-and-security / opensmt

The opensmt solver
Other
76 stars 18 forks source link

Assertion violation Theory.cc:103 (incomplete fix) #99

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Related and fixed: https://github.com/usi-verification-and-security/opensmt/issues/89

Hi, for the following formula,

(set-logic QF_LIA)
(declare-fun i3 () Int)
(push 1)
(push 1)
(assert false)
(check-sat)
(pop 1)
(check-sat)
(assert (= (* 53 (* (/ 901 211) (- i3 (- 901 53)))) 176))
(push 1)
(push 1)
(push 1)
(push 1)
(push 1)
(check-sat)
(pop 1)
(check-sat)
(check-sat)
(push 1)
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(push 1)
(push 1)
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(check-sat)
(push 1)
(check-sat)
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(check-sat)
(check-sat)
(check-sat)
(pop 1)
(assert (= (+ 0.0 (- i3 (- 901 53))) 0.0))
(check-sat)
(pop 1)
(check-sat)
(check-sat)
(push 1)
(assert false)
(check-sat)
(check-sat)
(pop 1)
(check-sat)

opensmt (commits 492c61689b2) throws an assertion violation

opensmt: /home/rainoftime/Work/tofuzz/opensmt/src/smtsolvers/Theory.cc:103: TPropRes CoreSMTSolver::handleSat(): Assertion `safeValue(l1) != l_True' failed.
Aborted (core dumped)

(Perhaps the root cause is the same with https://github.com/usi-verification-and-security/opensmt/issues/92

blishko commented 4 years ago

This one also works now, after #111. Note that operator "/" should not really be used in QF_LIA: http://smtlib.cs.uiowa.edu/theories-Ints.shtml In theories with integers you should be using operator "div" instead. Also zero should be just "0", not "0.0".