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).

1 files changed, 33 insertions, 35 deletions

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index e2a38b028..5b125b4b6 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -184,43 +184,41 @@ Node BVToInt::eliminationPass(Node n)
         (d_eliminationCache.find(current) != d_eliminationCache.end());
     bool inRebuildCache =
         (d_rebuildCache.find(current) != d_rebuildCache.end());
-    if (!inRebuildCache)
+    if (!inEliminationCache)
     {
-      // current is not the elimination of any previously-visited node
-      if (!inEliminationCache)
-      {
-        // current hasn't been eliminated yet.
-        // eliminate operators from it
-        Node currentEliminated =
-            FixpointRewriteStrategy<RewriteRule<UdivZero>,
-                                    RewriteRule<SdivEliminate>,
-                                    RewriteRule<SremEliminate>,
-                                    RewriteRule<SmodEliminate>,
-                                    RewriteRule<RepeatEliminate>,
-                                    RewriteRule<ZeroExtendEliminate>,
-                                    RewriteRule<SignExtendEliminate>,
-                                    RewriteRule<RotateRightEliminate>,
-                                    RewriteRule<RotateLeftEliminate>,
-                                    RewriteRule<CompEliminate>,
-                                    RewriteRule<SleEliminate>,
-                                    RewriteRule<SltEliminate>,
-                                    RewriteRule<SgtEliminate>,
-                                    RewriteRule<SgeEliminate>,
-                                    RewriteRule<ShlByConst>,
-                                    RewriteRule<LshrByConst> >::apply(current);
-        // save in the cache
-        d_eliminationCache[current] = currentEliminated;
-        // put the eliminated node in the rebuild cache, but mark that it hasn't
-        // yet been rebuilt by assigning null.
-        d_rebuildCache[currentEliminated] = Node();
-        // Push the eliminated node to the stack
-        toVisit.push_back(currentEliminated);
-        // Add the children to the stack for future processing.
-        toVisit.insert(
-            toVisit.end(), currentEliminated.begin(), currentEliminated.end());
-      }
+      // current hasn't been eliminated yet.
+      // eliminate operators from it
+      Node currentEliminated =
+          FixpointRewriteStrategy<RewriteRule<UdivZero>,
+                                  RewriteRule<SdivEliminate>,
+                                  RewriteRule<SremEliminate>,
+                                  RewriteRule<SmodEliminate>,
+                                  RewriteRule<RepeatEliminate>,
+                                  RewriteRule<ZeroExtendEliminate>,
+                                  RewriteRule<SignExtendEliminate>,
+                                  RewriteRule<RotateRightEliminate>,
+                                  RewriteRule<RotateLeftEliminate>,
+                                  RewriteRule<CompEliminate>,
+                                  RewriteRule<SleEliminate>,
+                                  RewriteRule<SltEliminate>,
+                                  RewriteRule<SgtEliminate>,
+                                  RewriteRule<SgeEliminate>,
+                                  RewriteRule<ShlByConst>,
+                                  RewriteRule<LshrByConst> >::apply(current);
+      // save in the cache
+      d_eliminationCache[current] = currentEliminated;
+      // also assign the eliminated now to itself to avoid revisiting.
+      d_eliminationCache[currentEliminated] = currentEliminated;
+      // put the eliminated node in the rebuild cache, but mark that it hasn't
+      // yet been rebuilt by assigning null.
+      d_rebuildCache[currentEliminated] = Node();
+      // Push the eliminated node to the stack
+      toVisit.push_back(currentEliminated);
+      // Add the children to the stack for future processing.
+      toVisit.insert(
+          toVisit.end(), currentEliminated.begin(), currentEliminated.end());
     }
-    else
+    if (inRebuildCache)
     {
       // current was already added to the rebuild cache.
       if (d_rebuildCache[current].isNull())