search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
371 stars 47 forks source link

Assertion error at exists_forall/ef_values.c:745 #366

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

950709adcb8e8ff26190

(set-logic UF)
(declare-const x Bool)
(declare-fun v () Bool)
(declare-sort S 0)
(assert (or v (and (not v) (forall ((q Bool)) (exists ((q S)) (forall ((q3 S)) (forall ((q5 Bool)) (and x (distinct q3 q)))))))))
(assert (or (forall ((q S)) (exists ((q3 S)) (exists ((q5 Bool)) (not (distinct q3 q)))))))
(check-sat)
yices_smt2 xx.smt2
yices_smt2: exists_forall/ef_values.c:745: ef_get_value_rep: Assertion `0' failed.
rainoftime commented 3 years ago

at exists_forall/ef_values.c:730:

(set-logic UF)
(declare-fun v () Bool)
(declare-sort S 0)
(assert (or (forall ((q Bool)) (exists ((q2 S)) (forall ((q S)) (distinct v (not (= q2 q))))))))
(assert (or (forall ((q2 S)) (exists ((q S)) (= q2 q)))))
(check-sat)