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

Z3/smt2_eval_CVC4 inconsistency: QF_BV/spear/wget_v1.10.2/src_wget_vc18197.smt2 #35

Open
hriener opened this issue Apr 26, 2015 · 2 comments
Open

Z3/smt2_eval_CVC4 inconsistency: QF_BV/spear/wget_v1.10.2/src_wget_vc18197.smt2 #35

hriener opened this issue Apr 26, 2015 · 2 comments
Assignees
@finnhaedicke

Comments

@hriener
Copy link
Contributor

hriener commented Apr 26, 2015

QF_BV/spear/wget_v1.10.2/src_wget_vc18197.smt2 smt2_eval_CVC4 FAIL
QF_BV/spear/wget_v1.10.2/src_wget_vc18755.smt2 smt2_eval_CVC4 FAIL
QF_BV/spear/wget_v1.10.2/src_wget_vc18756.smt2 smt2_eval_CVC4 FAIL
QF_BV/spear/wget_v1.10.2/src_wget_vc18196.smt2 smt2_eval_CVC4 FAIL
@hriener
Copy link
Contributor Author

hriener commented Apr 26, 2015

After minimization:
$ cat out.smt2
(set-logic QF_BV)
(assert (= (_ bv0 64) (bvsdiv (_ bv0 64) (_ bv0 64))))
(exit)

$ smt2_eval_CVC4 out.smt2
[metaSMT] Instance is SAT
[z3] Instance is UNSAT

@hriener
Copy link
Contributor Author

hriener commented Apr 26, 2015

@finnhaedicke: Could look into the CVC4 backend?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@finnhaedicke finnhaedicke

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@finnhaedicke @hriener