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
hermanventer@Hermans-MacBook-Pro MIRAI % z3 --version Z3 version 4.10.1 - 64 bit hermanventer@Hermans-MacBook-Pro MIRAI % which z3 /opt/homebrew/bin/z3 hermanventer@Hermans-MacBook-Pro MIRAI % cat z3.bug (declare-fun param_1 () Int) (assert (= 0 (rem param_1 2))) (assert (let ((a!1 (not (= 0 (rem (- 255 param_1) 2))))) (not a!1))) (check-sat) (get-model) hermanventer@Hermans-MacBook-Pro MIRAI % z3 z3.bug sat ( (define-fun param_1 () Int 0) )
Needless to say, this used to be unsatisfiable and still is on https://jfmc.github.io/z3-play/
Confirmed that this works as expected (non sat) using 4.9.1
The text was updated successfully, but these errors were encountered:
it has to be a regression, not specific to M1
Sorry, something went wrong.
8551b21
No branches or pull requests
hermanventer@Hermans-MacBook-Pro MIRAI % z3 --version
Z3 version 4.10.1 - 64 bit
hermanventer@Hermans-MacBook-Pro MIRAI % which z3
/opt/homebrew/bin/z3
hermanventer@Hermans-MacBook-Pro MIRAI % cat z3.bug
(declare-fun param_1 () Int)
(assert (= 0 (rem param_1 2)))
(assert (let ((a!1 (not (= 0 (rem (- 255 param_1) 2)))))
(not a!1)))
(check-sat)
(get-model)
hermanventer@Hermans-MacBook-Pro MIRAI % z3 z3.bug
sat
(
(define-fun param_1 () Int
0)
)
Needless to say, this used to be unsatisfiable and still is on https://jfmc.github.io/z3-play/
Confirmed that this works as expected (non sat) using 4.9.1
The text was updated successfully, but these errors were encountered: