Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)

`TheoryBVRewriter::RewriteITEBv()` is currently always returning the
status `REWRITE_DONE`. This can result in a situation where a rewritten
node can be rewritten again (which breaks the contract of our rewriter).
The unit test in this commit illustrates the issue. The commit fixes the
issue by returning `REWRITE_AGAIN` or `REWRITE_AGAIN_FULL` if a node
changed. `REWRITE_AGAIN_FULL` is needed if the resulting node may have a
child that is not a subterm of the original expression.

1 files changed, 10 insertions, 3 deletions

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 8f9e6614c..0f7629c5f 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -173,12 +173,19 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
                             RewriteRule<BvIteConstCond>,
                             RewriteRule<BvIteEqualChildren>,
                             RewriteRule<BvIteConstChildren>,
-                            RewriteRule<BvIteEqualCond>,
-                            RewriteRule<BvIteMergeThenIf>,
+                            RewriteRule<BvIteEqualCond>>::apply(node);
+  if (resultNode != node)
+  {
+    return RewriteResponse(REWRITE_AGAIN, resultNode);
+  }
+
+  resultNode =
+      LinearRewriteStrategy<RewriteRule<BvIteMergeThenIf>,
                             RewriteRule<BvIteMergeElseIf>,
                             RewriteRule<BvIteMergeThenElse>,
                             RewriteRule<BvIteMergeElseElse>>::apply(node);
-  return RewriteResponse(REWRITE_DONE, resultNode);
+  return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN_FULL,
+                         resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){