Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Invalid model for integer formula #4871

Closed
rainoftime opened this issue Dec 8, 2020 · 0 comments
Closed

Invalid model for integer formula #4871

rainoftime opened this issue Dec 8, 2020 · 0 comments

Comments

@rainoftime
Copy link
Contributor

rainoftime commented Dec 8, 2020

Hi, for the following formula,
z3 9f6a0a8

(set-option :model_validate true)
(declare-fun i6 () Int)
(assert (= 1 (mod i6 0)))
(assert (= 0 (mod (mod i6 25) 2)))
(check-sat-using (then solve-eqs qfnia))
(get-model)
./z3 delta.out.smt2                                                                                                         
sat
(error "line 5 column 39: an invalid model was generated")
(
  (define-fun i6 () Int
    76)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    1)
)
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant