diff options
| author | Tim King <taking@cs.nyu.edu> | 2013-04-01 17:26:13 -0400 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2013-04-01 17:26:54 -0400 |
| commit | 7e011fd7ae1a95eb70a393d780e13c559cdce4a1 (patch) | |
| tree | a64a7e6e3d53699b2adab78140c614db8e6c63a1 /test | |
| parent | b6ad34343d0a09de37dc4e5ff57cd8625dca3fc4 (diff) | |
Adding tests for the previous commit.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/boolean-equality.cvc | 8 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/boolean-terms-rewrite.cvc | 8 |
3 files changed, 17 insertions, 0 deletions
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; |