Adding tests for the previous commit.

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 8e992c03e48e1300d53718b7af07bc87ab6ead8d..2db03ff1cd2470e92c0aa4764fba26c48962c4be 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -43,6 +43,7 @@ TESTS =       \
        boolean-terms-parametric-datatype-2.cvc \
        boolean-terms-tuple.cvc \
        boolean-terms-record.cvc \
+       boolean-terms-rewrite.cvc \
        some-boolean-tests.cvc \
        v10l40099.cvc \
        v2l40025.cvc \

diff --git a/test/regress/regress0/datatypes/boolean-equality.cvc b/test/regress/regress0/datatypes/boolean-equality.cvc
new file mode 100644 (file)
index 0000000..16b6218
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-equality.cvc
@@ -0,0 +1,8 @@
+% EXPECT: sat
+% EXIT: 10
+
+x : [# b:BOOLEAN #];
+
+ASSERT x = x;
+
+CHECKSAT;

diff --git a/test/regress/regress0/datatypes/boolean-terms-rewrite.cvc b/test/regress/regress0/datatypes/boolean-terms-rewrite.cvc
new file mode 100644 (file)
index 0000000..3887ab5
--- /dev/null
+++ b/test/regress/regress0/datatypes/boolean-terms-rewrite.cvc
@@ -0,0 +1,8 @@
+% EXPECT: sat
+% EXIT: 10
+
+x : [# b:BITVECTOR(1) #];
+
+ASSERT FALSE = ((x = (# b := 0bin0 #)) = (x = (# b := 0bin1 #)));
+
+CHECKSAT;