broken formula

diff --git a/test/regress/simple2.smt b/test/regress/simple2.smt
new file mode 100644 (file)
index 0000000..c8db8c1
--- /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))
+)