8000 Completeness issue on simple string formula · Issue #7446 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Completeness issue on simple string formula #7446

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
merlinsun opened this issue Nov 7, 2024 · 0 comments
Closed

Completeness issue on simple string formula #7446

merlinsun opened this issue Nov 7, 2024 · 0 comments

Comments

@merlinsun
Copy link
merlinsun commented Nov 7, 2024 •
edited
Loading

Hello,

Z3 abd1674 returns unknown for the following formula. However, the term like (str.<= "" s) within it could be directly simplified to true.

Here’s a minimal example:

$ z3 small.smt2 
unknown
$ cat small.smt2 
(declare-fun v () String)
(assert (str.<= "" (str.replace_all v "i" v)))
(check-sat)

Thank you for your attention!
NikolajBjorner added a commit that referenced this issue Nov 12, 2024
@NikolajBjorner
fix #7446, by adding rewrite simplification
c0e748a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix Z3Prover#7446, by adding rewrite simplification
52bdfc5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix Z3Prover#7446, by adding rewrite simplification