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
Z3 (master 6384080) reports sat instead of unsat for the following formula:
sat
unsat
(declare-const A0 (Array Int Int)) (declare-const A1 (Array Int Int)) (assert (= A0 ((as const (Array Int Int)) 0))) (assert (= A1 ((as const (Array Int Int)) 1))) (assert (= (store A0 2 3) (store A1 2 3))) (check-sat)
The model Z3 reports is:
sat (model (define-fun A0 () (Array Int Int) ((as const (Array Int Int)) 0)) (define-fun A1 () (Array Int Int) ((as const (Array Int Int)) 1)) )
Does Z3 fully support equalities over constant arrays?
The text was updated successfully, but these errors were encountered:
fffc539
No branches or pull requests
Z3 (master 6384080) reports
sat
instead ofunsat
for the following formula:The model Z3 reports is:
Does Z3 fully support equalities over constant arrays?
The text was updated successfully, but these errors were encountered: