From: Tim King <taking@cs.nyu.edu>
Date: Mon, 1 Apr 2013 21:26:13 +0000 (-0400)
Subject: Adding tests for the previous commit.
X-Git-Tag: cvc5-1.0.0~7351
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e011fd7ae1a95eb70a393d780e13c559cdce4a1;p=cvc5.git

Adding tests for the previous commit.
---

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 8e992c03e..2db03ff1c 100644
--- 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
index 000000000..16b6218e9
--- /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
index 000000000..3887ab5a5
--- /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;