search

SRI-CSL / sally

A model checker for infinite-state systems.
http://sri-csl.github.io/sally/
GNU General Public License v2.0
69 stars 12 forks source link

Assertion failure in Yices #23

Closed dddejan closed 9 years ago

dddejan commented 9 years ago

To run it use 

./builds/src/sally --engine ic3 --lsal-extensions -v 1 --solver y2m5 examples/tte_synchro/tte_synchro.mcmt examples/tte_synchro/tte_synchro.cm_clock_distance.mcmt -d ic3::generalization -d ic3 -d ic3::deadlock

The assertion fails

sally: solvers/simplex/simplex.c:6949: simplex_process_var_diseq: Assertion `arith_var_has_eterm(&solver->vtbl, x1) && arith_var_has_eterm(&solver->vtbl, x2) && x1 != x2' failed.
dddejan commented 9 years ago

Maybe a simpler problem to look at 

./src/sally -v 1 --engine ic3 ../examples/oral_messages/om1_with_relays_validity_two_faults.mcmt
dddejan commented 9 years ago

Fixed in Yices.