diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-10-06 13:47:58 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-06 15:47:58 -0500 |
| commit | 5aa526ab1df69783d17750bfce8819a6e358e157 (patch) | |
| tree | c615abaee6f4bb492ed4d9256d806bbede77cb2e /test/regress/regress2 | |
| parent | e10c381b821337c239479d86fbf1d2eb617c590a (diff) | |
bv-to-int: change order of passes (#5208)
Closes #5095 and replaces #5110.
There are two tests in #5095 that produce two different assertion failures when using bv-to-int.
The first happens because the substitution map wasn't applied after the pass.
The second happens because div (that is introduced in the pass) is not rewritten using witness.
Both problems are solved by making sure that apply-substs, theory-preprocess and ite-removal are executed after bv-to-int.
The two tests from #5095 are included as regressions.
Diffstat (limited to 'test/regress/regress2')
| -rw-r--r-- | test/regress/regress2/bv_to_int_5095.smt2 | 10 | ||||
| -rw-r--r-- | test/regress/regress2/bv_to_int_5095_2.smt2 | 6 |
2 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress2/bv_to_int_5095.smt2 b/test/regress/regress2/bv_to_int_5095.smt2 new file mode 100644 index 000000000..bec97618d --- /dev/null +++ b/test/regress/regress2/bv_to_int_5095.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic QF_BV) +(set-option :solve-bv-as-int sum) +(set-option :incremental true) +(declare-fun _substvar_27_ () Bool) +(declare-const bv_40-3 (_ BitVec 40)) +(assert (= bv_40-3 (_ bv0 40))) +(push 1) +(assert _substvar_27_) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress2/bv_to_int_5095_2.smt2 b/test/regress/regress2/bv_to_int_5095_2.smt2 new file mode 100644 index 000000000..54dfa0946 --- /dev/null +++ b/test/regress/regress2/bv_to_int_5095_2.smt2 @@ -0,0 +1,6 @@ +; EXPECT: sat +; COMMAND --solve-bv-as-int=sum +(set-logic BV) +(declare-const bv_42-0 (_ BitVec 42)) +(assert (exists ((q28 (_ BitVec 42))) (distinct (bvudiv bv_42-0 bv_42-0) q28))) +(check-sat)
\ No newline at end of file |