bv-to-int: change order of passes (#5208)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 6 Oct 2020 20:47:58 +0000 (13:47 -0700)
committerGitHub <noreply@github.com>
Tue, 6 Oct 2020 20:47:58 +0000 (15:47 -0500)
commit5aa526ab1df69783d17750bfce8819a6e358e157
treec615abaee6f4bb492ed4d9256d806bbede77cb2e
parente10c381b821337c239479d86fbf1d2eb617c590a
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.
src/smt/process_assertions.cpp
test/regress/CMakeLists.txt
test/regress/regress2/bv_to_int_5095.smt2 [new file with mode: 0644]
test/regress/regress2/bv_to_int_5095_2.smt2 [new file with mode: 0644]