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

Soundness bug in horn tactic #3822

Closed

numairmansur opened this issue Apr 6, 2020 · 0 comments

numairmansur commented Apr 6, 2020

Hi,
On the following sat formula, i get unsat with (check-sat-using horn)

(set-logic BV)
(declare-fun W_S2_V3 () Bool)
(declare-fun R_S2_V1 () Bool)
(declare-fun W_S1_V1 () Bool)
(assert
 (let (($x10 (not W_S2_V3)))
 (not $x10)))
(assert
 (let (($x16 (and W_S1_V1 R_S2_V1)))
 (let (($x17 (not $x16)))
 (let (($x710 (not $x17)))
 (let (($x758 (not $x710)))
 (not $x758))))))
(check-sat-using horn)

commit: 16be6b9

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

NikolajBjorner closed this as completed in

6761bf1

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