From f7036fc10ccdebfc1ca7fffe692cd26dd5eb50fe Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 18 Jun 2020 23:42:59 -0700 Subject: 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). --- test/regress/regress0/bv/bv_to_int_elim_err.smt2 | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test/regress/regress0/bv/bv_to_int_elim_err.smt2 (limited to 'test/regress/regress0/bv') 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) -- cgit v1.2.3