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

Refutational soundness bug in QF_S #4875

Closed

wintered opened this issue Dec 8, 2020 · 0 comments

wintered commented Dec 8, 2020 •

edited

Loading

Hi,
the following trace shows a refutational soundness bug in Z3 (c49d39a).

[596] % z3release small.smt2
unsat
sat
[597] % cat small.smt2
(declare-const a String)
(assert (distinct (str.replace (str.replace a "B" a) a "AB") (str.replace (str.replace a "B" "AB") a "AB")))
(check-sat)
(reset)
(define-fun a () String "B")
(assert (distinct (str.replace (str.replace a "B" a) a "AB") (str.replace (str.replace a "B" "AB") a "AB")))
(check-sat)
[598] %

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

NikolajBjorner closed this as completed in

fae9481

# for free to join this conversation on GitHub. Already have an account? # to comment