bv-to-int: Expand definitions of bvudiv and bvurem during bv-to-int preprocessing...
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 8 Dec 2020 12:51:06 +0000 (04:51 -0800)
committerGitHub <noreply@github.com>
Tue, 8 Dec 2020 12:51:06 +0000 (06:51 -0600)
commitc23652b991f064ada72427e2ab4098a105587bef
tree509b56117d90efda6d26f0865f016da8b8723ba8
parent384ab75e8637e872b568b6f493612d308f3f15ee
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.
src/preprocessing/passes/bv_to_int.cpp
test/regress/CMakeLists.txt