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

cryptic yices error #33

Closed xapantu closed 8 years ago

xapantu commented 8 years ago
> src/sally mutex.mcmt --engine ic3
Yices error (push): the context state does not allow operation

mutex.mcmt.txt

dddejan commented 8 years ago

This is most likely due to a deadlocked model.

dddejan commented 8 years ago

In the aiger branch you can use the --ic3-check-deadlock option to check for deadlocks.