search

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:1133 #388

Closed rainoftime closed 1 year ago

rainoftime commented 2 years ago

yices f705557b7d33d866eb1

(set-logic ALL)
(declare-fun B () (Array (Array Int Bool) (Array Int Bool)))
(declare-fun C () (Array (Array (Array Int Bool) (Array Int Bool)) Bool))
(assert (C B))
yices_smt2: mcsat/solver.c:1133: mcsat_get_type_owners: Assertion `plugin_i != 10' failed.
ahmed-irfan commented 1 year ago

fixed!

mcsat now supports arrays.