diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-06-18 23:42:59 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-18 23:42:59 -0700 |
commit | f7036fc10ccdebfc1ca7fffe692cd26dd5eb50fe (patch) | |
tree | 660b6877dd4aec0f2d60fe3a1558ded8e0db498b /test/regress/regress0/bv | |
parent | e8884b9b8ba86ce71807887cab87a5188cce4003 (diff) |
Bv to int elimination bugfix (#4435)
fix 1:
------
The wrong flag was checked in the traversal, causing an assertion error [here](https://github.com/CVC4/CVC4/blob/8236d7f9bff3aef4f7b37a15d509b8a11551401f/src/preprocessing/passes/bv_to_int.cpp#L247)
This is fixed in this PR. A test was added as well.
fix 2:
------
It is desirable that bv-to-bool runs before bv-to-int, but this was not the case, and is fixed in this PR.
Do not merge until after competition release (label added).
Diffstat (limited to 'test/regress/regress0/bv')
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_elim_err.smt2 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 new file mode 100644 index 000000000..16731b01e --- /dev/null +++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models +; EXPECT: sat +(set-logic QF_BV) +(declare-fun _substvar_183_ () (_ BitVec 32)) +(assert (let ((?x15 ((_ sign_extend 0) _substvar_183_))) (bvsle ((_ zero_extend 24) ((_ extract 15 8) (bvadd ?x15 (_ bv4294966758 32)))) (bvadd ?x15 ?x15)))) +(check-sat) +(exit) |