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 violation at solvers/funs/fun_solver.c:2661 #252

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-logic QF_ALIA)
(declare-fun _substvar_237_ () (Array (Array (Array Bool Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)))
(declare-fun _substvar_249_ () (Array (Array (Array Bool Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)))
(declare-fun _substvar_289_ () (Array (Array (Array Bool Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)))
(declare-fun _substvar_385_ () (Array Bool Bool))
(declare-fun _substvar_547_ () (Array Bool Bool))
(declare-fun _substvar_569_ () (Array (Array (Array Bool Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)))
(declare-fun _substvar_600_ () (Array (Array (Array Bool Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)))
(declare-fun _substvar_619_ () (Array (Array Bool Bool) (Array Bool Bool)))
(declare-fun _substvar_622_ () (Array Bool Bool))
(declare-const arr-3410093864546416904_3410093864546416904-0 (Array (Array Bool Bool) (Array Bool Bool)))
(declare-const arr-3410093864546416904_5084294929380604898-0 (Array (Array Bool Bool) Bool))
(assert (= _substvar_289_ _substvar_249_ _substvar_237_ (store _substvar_600_ arr-3410093864546416904_3410093864546416904-0 (store arr-3410093864546416904_5084294929380604898-0 _substvar_547_ true)) (store (store (store _substvar_569_ arr-3410093864546416904_3410093864546416904-0 (store arr-3410093864546416904_5084294929380604898-0 _substvar_385_ true)) _substvar_619_ arr-3410093864546416904_5084294929380604898-0) arr-3410093864546416904_3410093864546416904-0 (store arr-3410093864546416904_5084294929380604898-0 (select arr-3410093864546416904_3410093864546416904-0 _substvar_622_) true))))
(check-sat)

yices d89f5f7e77

yices_smt2: solvers/funs/fun_solver.c:2661: equal_mappings: Assertion `n <= card && m <= card && dv != (2147483647) && dw != (2147483647)' failed.
BrunoDutertre commented 4 years ago

Same as #255. Fixed in d0dc837dc578158ec956b6c7000f6ed126f524ec.