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/regress1/ho | |
| 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/regress1/ho')
| -rw-r--r-- | test/regress/regress1/ho/issue4065-no-rep.smt2 | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2 index 25662d6eb..9852150d9 100644 --- a/test/regress/regress1/ho/issue4065-no-rep.smt2 +++ b/test/regress/regress1/ho/issue4065-no-rep.smt2 @@ -1,8 +1,5 @@ -; COMMAND-LINE: -q -; EXPECT: sat (set-logic AUFBV) -(set-info :status sat) -(set-option :bv-div-zero-const false) +(set-info :status unsat) (set-option :fmf-bound-int true) (set-option :uf-ho true) (declare-fun _substvar_20_ () Bool) |