diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-15 14:04:27 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-15 14:04:27 -0600 |
| commit | 002955063ecf1b4b190717a7a0b2aec79ac7b6d9 (patch) | |
| tree | 9a26231f484a76f8373541c67e3c1e7156b12a6a /test/regress/regress0 | |
| parent | aa1b0e19f9ccfc5338a1d056f03b36c0bec6b4b4 (diff) | |
Remove bv divide by zero option (#5672)
This is required to avoid failures in the planned refactoring of check-models.
This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem.
It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM.
FYI @barrettcw
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/bv/divtest_2_5.smt2 | 5 | ||||
| -rw-r--r-- | test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 | 6 |
3 files changed, 6 insertions, 7 deletions
diff --git a/test/regress/regress0/bv/divtest_2_5.smt2 b/test/regress/regress0/bv/divtest_2_5.smt2 index b2712e520..f45520044 100644 --- a/test/regress/regress0/bv/divtest_2_5.smt2 +++ b/test/regress/regress0/bv/divtest_2_5.smt2 @@ -1,7 +1,6 @@ -; EXPECT: sat -(set-info :smt-lib-version 2.5) +; EXPECT: unsat (set-logic QF_BV) -(set-info :status sat) +(set-info :status unsat) (declare-fun x () (_ BitVec 8)) (declare-fun y () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 index c6748b19e..b53f6f0cc 100644 --- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-div-zero-const --no-check-unsat-cores +; COMMAND-LINE: --no-check-unsat-cores (set-logic QF_BV) (set-info :status unsat) (declare-const x (_ BitVec 4)) diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 index 0888031d5..a514d8b09 100644 --- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --no-bv-div-zero-const --no-check-unsat-cores -; COMMAND-LINE: --bv-solver=simple --no-bv-div-zero-const --no-check-unsat-cores +; COMMAND-LINE: --no-check-unsat-cores +; COMMAND-LINE: --bv-solver=simple --no-check-unsat-cores (set-logic QF_BV) -(set-info :status sat) +(set-info :status unsat) (declare-const x (_ BitVec 4)) (declare-const y (_ BitVec 4)) (assert (not (= (bvugt (bvurem y x) x) (ite (= x #x0) (bvugt y #x0) false)))) |