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

Jump to bottom

(rewriter.flat=false) Invalid model on QF_LIA formula #4951

Closed
muchang opened this issue Jan 14, 2021 · 0 comments
Closed

(rewriter.flat=false) Invalid model on QF_LIA formula #4951

muchang opened this issue Jan 14, 2021 · 0 comments

Comments

@muchang
Copy link

muchang commented Jan 14, 2021

z3_invalid_model.smt2.zip

[621] % z3release model_validate=true z3_invalid_model.smt2 
sat
[622] % z3release model_validate=true rewriter.flat=false z3_invalid_model.smt2 
sat
(error "line 366 column 10: an invalid model was generated")
[623] %

Commit: 8abb644
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@muchang