SRI-CSL / yices2

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

Assertion error at mcsat/solver.c:1132 #337

Closed rainoftime closed 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula yices2 238592b9

(set-logic ALL)
(declare-fun s0 () (Array Int Bool))
(declare-fun s1 () (Array Int Bool))
(declare-fun s2 () (Array Int Bool))
(define-fun s3 () Bool (distinct s0 s1 s2))
(assert s3)
(check-sat)

./yices_smt2 --mcsat xx.smt2 
yices_smt2: mcsat/solver.c:1132: mcsat_get_type_owners: Assertion `plugin_i != 10' failed
dddejan commented 3 years ago

The MCSAT solver doesn't support arrays. I'll fix this to report an error.