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 on QF_S formula #4794

Closed

rainoftime opened this issue Nov 14, 2020 · 0 comments

Contributor

rainoftime commented Nov 14, 2020 •

edited

Loading

Hi, for the following formula

(declare-fun str12 () String)
(declare-fun str13 () String)
(assert (str.in_re str13 (re.inter (re.union (str.to_re "hcoyHvwKX") (str.to_re str13) (str.to_re str12)) (re.* (str.to_re "")))))
(check-sat)

Z3 49a0266 yields unsat, but CVC4 answers sat.
Below is a model given by CVC4 and passed the check of Z3

(define-fun str12 () String "")
(define-fun str13 () String "")

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

NikolajBjorner closed this as completed in

12198d1

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