From 7e011fd7ae1a95eb70a393d780e13c559cdce4a1 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 1 Apr 2013 17:26:13 -0400 Subject: [PATCH] Adding tests for the previous commit. --- test/regress/regress0/datatypes/Makefile.am | 1 + test/regress/regress0/datatypes/boolean-equality.cvc | 8 ++++++++ test/regress/regress0/datatypes/boolean-terms-rewrite.cvc | 8 ++++++++ 3 files changed, 17 insertions(+) create mode 100644 test/regress/regress0/datatypes/boolean-equality.cvc create mode 100644 test/regress/regress0/datatypes/boolean-terms-rewrite.cvc 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; -- 2.30.2