We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
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
For this formula, CVC4 without fmf-bound gives a result quickly, while CVC4 hangs using fmf-bound. It is likely a performance issue.
[581] % time cvc4 -q small.smt2 unsat real 0m0.087s user 0m0.053s sys 0m0.004s [582] % [582] % timeout -s 9 30 cvc4 --fmf-bound -q small.smt2 Killed [583] % [583] % cat small.smt2 (declare-fun a () Int) (declare-fun b () (Array Int Int)) (declare-fun c () Int) (declare-fun d () Int) (assert (> (select b 0) (select b 1))) (assert (forall ((e Int)) (=> (<= 0 e (- a d)) (forall ((f Int)) (=> (<= (+ d 1) f) (<= (select b e) (select b f))))))) (assert (exists ((h Int)) (and (<= 0 h c) (exists ((i Int)) (let ((g (store (store b 0 (select b 1)) 1 (select b 0)))) (and (<= (+ d 1) i) (> (select g h) (select g i)))))))) (assert (= a (+ d c))) (check-sat) [584] %
Commit: 36af095
The text was updated successfully, but these errors were encountered:
This is expected behavior, --fmf-bound is worse for "UNSAT" instances.
--fmf-bound
Internal note: --fmf-inst-engine also does not solve this.
--fmf-inst-engine
Transferring to cvc4-projects.
Sorry, something went wrong.
ajreynol
No branches or pull requests
For this formula, CVC4 without fmf-bound gives a result quickly, while CVC4 hangs using fmf-bound. It is likely a performance issue.
Commit: 36af095
The text was updated successfully, but these errors were encountered: