You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Set Yices as the backend for all abstract queries
Note that bt and m5 backends for abstract queries were only experimental (disabled)
Now flags BACKEND_* only configures bitvector solver
Refs: #15, #16
./avr.py --bmc --bin ./build/bin-mathsat5 --timeout 900 --memout 15000 counter_v.btor2.txt
./build/bin-mathsat5/
Copyright (c) 2016 - Present Aman Goel and Karem Sakallah, University of Michigan (output dir: output/work_test) (frontend: btor2) (property: all (1 assertions)) (problem size: 4 bits) (abstraction: sa+uf) 0s (bmc: safe till step 0) (bmc: abstract mode disabled at step 1) 0s (bmc: safe till step 5) 0s (bmc: safe till step 10) reach: reach_m5.cpp:1315: virtual int _m5::m5_API::s_check(long int, bool): Assertion `!MSAT_ERROR_MODEL(*m_model)' failed.
The text was updated successfully, but these errors were encountered: