From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 8 Dec 2009 19:00:53 +0000 (+0000)
Subject: broken formula
X-Git-Tag: cvc5-1.0.0~9387
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a85aa996535fb86009c1869f0daa1c27c980a566;p=cvc5.git

broken formula
---

diff --git a/test/regress/simple2.smt b/test/regress/simple2.smt
new file mode 100644
index 000000000..c8db8c13f
--- /dev/null
+++ b/test/regress/simple2.smt
@@ -0,0 +1,13 @@
+(benchmark b
+:status unknown
+:logic QF_UF
+:extrapreds ((x0))
+:extrapreds ((x1))
+:extrapreds ((x2))
+:extrapreds ((x3))
+:assumption (or x1 (not x0))
+:formula
+(and (or x0 (not x3))
+     (or x3 x2)
+     (not x1))
+)