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

Invalid model for QF_LIA opt instance #3509

Closed
rainoftime opened this issue Mar 25, 2020 · 0 comments
Closed

Invalid model for QF_LIA opt instance #3509

rainoftime opened this issue Mar 25, 2020 · 0 comments

Comments

@rainoftime
Copy link
Contributor

Hi, for the following opt instance, z3 (Commit 41c68d6) gives an invalid model

(set-logic QF_LIA)
(set-option :model_validate true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v11 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i6 Int)
(declare-const i11 Int)
(declare-const v12 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const i14 Int)
(declare-const v27 Bool)
(declare-const v32 Bool)
(assert (or v32 (>= 905 i6) (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14)))
(assert (or (= i6 i1) (= i0 150) (>= 905 i6)))
(assert (or v32 (>= 905 i6) v7))
(assert (or (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14) (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14) (=> v8 (not v4))))
(assert (or (not v14) (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14) (= i1 i11)))
(assert (or v7 v32 (< 780 i14)))
(assert (or (not v14) v27 v2))
(assert (or (= i1 i11) v7 (= i0 150)))
(assert (or v32 v7 (not v14)))
(assert (or v7 (>= 905 i6) (=> v8 (not v4))))
(assert (or v15 (= i6 i1) (not v14)))
(assert (or (< 780 i14) (< 780 i14) v27))
(assert (or v2 (not v14) (>= 905 i6)))
(assert (or (or v9 v14 v6 (<= 205 98) v11 v6 v12 (distinct i1 i6) v14) v32 (= i6 i1)))
(assert (or v32 (< 780 i14) (>= 905 i6)))
(minimize i1)
(check-sat)
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

1 participant