diff options
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 \ |