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

Solution soundness bug on QF_S formula #4791

Closed

wintered opened this issue Nov 12, 2020 · 0 comments

wintered commented Nov 12, 2020

[637] % cvc4 small.smt2
unsat
[638] % z3release small.smt2
sat
[639] % 
[639] % cat small.smt2
(set-logic QF_S)
(assert (str.in_re "A" (re.diff (re.* re.allchar) re.allchar (re.* re.allchar))))
(check-sat)
[640]

OS: Ubuntu 18.04
Commit: dd3e6c

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

NikolajBjorner closed this as completed in

5d10cb7

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