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

[consolidated] Issues about string formulas #6054

Closed

merlinsun opened this issue May 26, 2022 · 1 comment

merlinsun commented May 26, 2022

Hi,
For this instance, z3 f77037e gives an invalid model.

$ z3 model_validate=true delta.smt2
sat
(error "line 4 column 10: an invalid model was generated")
$ cat delta.smt2
(declare-fun v () Int)
(declare-fun a () Int)
(assert (distinct true (= "" (str.replace (str.substr "A" 0 a) "" (str.substr "A" 0 v)))))
(check-sat)

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

merlinsun changed the title ~~Invalid model on string formula~~ [consolidated] Issues about string formulas

Author

merlinsun commented May 26, 2022

Refutational soundness

$ cat case1.smt2
(set-logic ALL)
(declare-fun v () Int)
(declare-fun a () Int)
(assert (= "" (str.replace (str.substr "A" 0 v) "" (str.substr "A" 0 a))))
(check-sat)
$ z3 case1.smt2
unsat
$ cat case2.smt2
(set-logic ALL)
(declare-fun v () Int)
(declare-fun a () Int)
(assert (= "" (str.replace (str.substr "A" 0 0) "" (str.substr "A" 0 0))))
(check-sat)
$ z3 case2.smt2
sat

NikolajBjorner closed this as completed in

de892ed

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