From d100ff88e449dc57098089e86b1de7b8ea8ff751 Mon Sep 17 00:00:00 2001
From: Dejan Jovanovic <dejan.jovanovic@sri.com>
Date: Tue, 25 Aug 2015 16:15:49 -0700
Subject: another test case

---
 test/regress/regress0/bool/test01.smt2 | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 test/regress/regress0/bool/test01.smt2

diff --git a/test/regress/regress0/bool/test01.smt2 b/test/regress/regress0/bool/test01.smt2
new file mode 100644
index 000000000..0436766aa
--- /dev/null
+++ b/test/regress/regress0/bool/test01.smt2
@@ -0,0 +1,25 @@
+(set-logic QF_UF)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(declare-fun x0 () Bool)
+(declare-fun y0 () Bool)
+(declare-fun z0 () Bool)
+
+(assert (or x0 y0))
+(assert (or (not y0) z0))
+
+(declare-fun x1 () Bool)
+(declare-fun y1 () Bool)
+
+(assert x1)
+(assert y1)
+
+(declare-fun f (Bool) Bool)
+
+(assert (not (= (f (or x0 z0)) (f (and x1 y1)))))
+
+(check-sat)
+
+(exit)
-- 
cgit v1.2.3