Assertion failed when using MathSAT as backend solver

[nianzelee]

• Version: dbc3371
• Environment: Ubuntu 22.04 (Linux kernel 6.5.0-17-generic)
• Command line: ./avr.py --bmc --bin ./build/bin-mathsat5 --timeout 900 --memout 15000 counter_v.btor2.txt
  • AVR was compiled with MathSAT, and binaries are put under ./build/bin-mathsat5/
  • Input file counter_v.btor2.txt attached
• Result

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.

[aman-goel]

Same comments as #15

[nianzelee]

I still encountered the same error with --abstract sa.

• Version: f145cbc (recompiled with MathSAT 5.6.10)
• Command line: ./avr.py --bmc --bin ./build/bin-mathsat5/ --timeout 900 --memout 15000 counter_v.btor2.txt --abstract sa

Do you have an idea what may cause the problem?