diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-11-13 04:49:34 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-11-13 04:49:34 +0000 |
commit | 2cf12a56cb9c5eb539d50a39b2764a292d6fd13f (patch) | |
tree | 3578ca6339a97e4b85c83d1a9f2219aea569aca7 /test/regress/regress0/unconstrained/Makefile.am | |
parent | 89081ba6a8a62a117cbfef99aa7c8e4bf0bf1b39 (diff) |
added support for division by zero for bit-vector division operators
Diffstat (limited to 'test/regress/regress0/unconstrained/Makefile.am')
-rw-r--r-- | test/regress/regress0/unconstrained/Makefile.am | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index 05c66d60c..7e5bcba8c 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -16,6 +16,8 @@ export CVC4_REGRESSION_ARGS # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" # dejan: disable arith2.smt2, arith7.smt2 it's mixed arithmetic and it doesn't go well when changing theoryof +# lianah: disabled bvdiv.smt2, bvconcat.smt2 as the unconstrained terms are no longer recognized after implementing +# the divide-by-zero semantics for bv division. TESTS = \ arith3.smt2 \ arith4.smt2 \ @@ -28,9 +30,7 @@ TESTS = \ bvbool.smt2 \ bvcmp.smt2 \ bvconcat2.smt2 \ - bvconcat.smt2 \ bvdiv2.smt2 \ - bvdiv.smt2 \ bvext.smt2 \ bvite.smt2 \ bvmul2.smt2 \ |