Adding ITE tests

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 521fd7feb58e5a6aa29d8eafd7fc3c80b5e71afe..58f9c6a4e3d5983a2a2c3d3350ed1699177df35e 100644 (file)
--- 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 (file)
index 0000000..b3c4f3e
--- /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 (file)
index 0000000..c1c41f4
--- /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)