diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-12-08 04:51:06 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-08 06:51:06 -0600 |
| commit | c23652b991f064ada72427e2ab4098a105587bef (patch) | |
| tree | 509b56117d90efda6d26f0865f016da8b8723ba8 /test/regress | |
| parent | 384ab75e8637e872b568b6f493612d308f3f15ee (diff) | |
bv-to-int: Expand definitions of bvudiv and bvurem during bv-to-int preprocessing pass (#5620)
#5544 enforces expandDefinition not to run before preprocessing.
The bv-to-int preprocessing pass used to rely on expandDefinition to replace BITVECTOR_UDIV and BITVECTOR_UREM with their _TOTAL versions.
This PR performs the replacement in the preprocessing pass itself.
A regression that timed out is now fixed and is brought back to the regressions.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7b3f94c1a..56780278b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2166,6 +2166,7 @@ set(regress_2_tests regress2/bv_to_int_ashr.smt2 regress2/bv_to_int_bitwise.smt2 regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 + regress2/bv_to_int_bvmul1.smt2 regress2/bv_to_int_inc1.smt2 regress2/bv_to_int_mask_array_1.smt2 regress2/bv_to_int_mask_array_2.smt2 @@ -2628,7 +2629,6 @@ set(regression_disabled_tests regress2/arith/real2int-test.smt2 regress2/bug396.smt2 # due to bv2int not handling unsigned/signed division - regress2/bv_to_int_bvmul1.smt2 regress2/nl/dumortier-050317.smt2 regress2/nl/nt-lemmas-bad.smt2 regress2/quantifiers/ForElimination-scala-9.smt2 |