From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Fri, 14 May 2010 22:50:13 +0000 (+0000)
Subject: Adding ITE tests
X-Git-Tag: cvc5-1.0.0~9058
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=06b5f38e17a1275e966e50c2d74274ef4d4d4697;p=cvc5.git

Adding ITE tests
---

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 521fd7feb..58f9c6a4e 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -14,6 +14,8 @@ TESTS =	\
 	simple-uf.smt \
 	ite.smt2 \
 	ite2.smt2 \
+	ite3.smt2 \
+	ite4.smt2 \
 	bug32.cvc \
 	hole6.cvc \
 	logops.01.cvc \
diff --git a/test/regress/regress0/ite3.smt2 b/test/regress/regress0/ite3.smt2
new file mode 100644
index 000000000..b3c4f3e84
--- /dev/null
+++ b/test/regress/regress0/ite3.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(declare-fun a () Bool)
+(assert (not (= x (ite a (ite a x y) (ite (not a) x y)))))
+(check-sat)
diff --git a/test/regress/regress0/ite4.smt2 b/test/regress/regress0/ite4.smt2
new file mode 100644
index 000000000..c1c41f4b5
--- /dev/null
+++ b/test/regress/regress0/ite4.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_UF)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(declare-fun a () Bool)
+(assert (not (= x (ite a (ite a x y) (ite (not a) y x)))))
+(check-sat)