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 | |
| parent | 89081ba6a8a62a117cbfef99aa7c8e4bf0bf1b39 (diff) | |
added support for division by zero for bit-vector division operators
Diffstat (limited to 'test/regress/regress0/unconstrained')
| -rw-r--r-- | test/regress/regress0/unconstrained/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/unconstrained/bvdiv2.smt2 | 8 |
2 files changed, 6 insertions, 6 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 \ diff --git a/test/regress/regress0/unconstrained/bvdiv2.smt2 b/test/regress/regress0/unconstrained/bvdiv2.smt2 index 6314701b3..7a8fc3753 100644 --- a/test/regress/regress0/unconstrained/bvdiv2.smt2 +++ b/test/regress/regress0/unconstrained/bvdiv2.smt2 @@ -18,9 +18,9 @@ (declare-fun v4 () (_ BitVec 1024)) (declare-fun v5 () (_ BitVec 1024)) (assert - (not - (= (bvudiv x0 x0) (_ bv1 10)) - ) -) + (and + (not (= x0 (_ bv0 10))) + (not (= (bvudiv x0 x0) (_ bv1 10))) +)) (check-sat) (exit) |