Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Assertion failed when using MathSAT as backend solver #16

Open
nianzelee opened this issue Feb 9, 2024 · 2 comments
Open

Assertion failed when using MathSAT as backend solver #16

nianzelee opened this issue Feb 9, 2024 · 2 comments

Comments

@nianzelee
Copy link

  • 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 added a commit that referenced this issue Feb 24, 2024
@aman-goel
Use Y2 backend for all abstract queries
f5238a3 
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
@aman-goel
Copy link
Owner

aman-goel commented Feb 24, 2024 •
edited

Same comments as #15

@nianzelee
Copy link
Author

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?

@aman-goel aman-goel reopened this Apr 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@nianzelee @aman-goel