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.

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 version 4.4.1 gives semingly incorrect model #2212

Closed
sdasgup3 opened this issue Mar 29, 2019 · 1 comment
Closed

Z3 version 4.4.1 gives semingly incorrect model #2212

sdasgup3 opened this issue Mar 29, 2019 · 1 comment

Comments

@sdasgup3
Copy link

sdasgup3 commented Mar 29, 2019

With the following Z3 query:

(declare-const A (_ BitVec 64))
(declare-const B (_ BitVec 64))
(push)  
(assert

(>= (+ (bv2int A) (bv2int B)) (^ 2 32))
)  
(check-sat)
(get-model)
(pop)

With Z3 version 4.4.1, I am getting a model like

sat
(model 
  (define-fun A () (_ BitVec 64)
    #x0000000000000000)
  (define-fun B () (_ BitVec 64)
    #x0000000000000000)
)

With version Z3 version 4.5.1 I am getting correct interpretation.
Is this fixed as per #250 ? Or there is something I am doing wrong.

@NikolajBjorner
Copy link
Contributor

There is no support for (very) old versions of Z3. Use newer versions where the models are correct.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants