8000 Invalid model for String formula with str.++ and int.to.str (smt.arith.solver = 2, 5, 6) · Issue #4080 · Z3Prover/z3 · GitHub

More Web Proxy on the site http://driver.im/

Invalid model for String formula with str.++ and int.to.str (smt.arith.solver = 2, 5, 6) #4080

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.

Sign up for GitHub

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

Jump to bottom

Closed

rainoftime opened this issue Apr 24, 2020 · 0 comments

Contributor

rainoftime commented

Hi, for the following formula,
z3 (commit 04fec3f) gives an invalid model

(set-option :model_validate true)
(declare-const i3 Int)
(declare-const Str3 String)
(declare-const Str5 String)
(declare-const Str6 String)
(declare-const Str11 String)
(declare-const Str16 String)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(assert (or (and v17 (distinct (str.++ Str16 (int.to.str i3)) Str5 Str6 Str11 Str3)) v19 v18))
(check-sat)

The text was updated successfully, but these errors were encountered:

NikolajBjorner closed this as completed in

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

0