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
Hi, z3 gives unsat for the following instance.
unsat
$ cat test.smt (set-option :smt.phase_selection 1) (set-option :smt.arith.propagate_eqs false) (set-option :smt.arith.eager_eq_axioms false) (declare-fun i1 () Int) (declare-fun str1 () String) (assert (<= 32 (str.len str1))) (minimize i1) (check-sat) $ z3 test.smt unsat
However, z3 gives sat for the same instance without options.
sat
$ cat no-options.smt (declare-fun i1 () Int) (declare-fun str1 () String) (assert (<= 32 (str.len str1))) (minimize i1) (check-sat) $ z3 no-options.smt sat
Version: z3 4.13.0 3049f57
3049f57
The text was updated successfully, but these errors were encountered:
#7344
349ebd0
No branches or pull requests
Hi, z3 gives
unsat
for the following instance.However, z3 gives
sat
for the same instance without options.Version: z3 4.13.0
3049f57
The text was updated successfully, but these errors were encountered: