diff options
Diffstat (limited to 'test')
| -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) |