Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)

This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.

1 files changed, 7 insertions, 3 deletions

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index d0579703d..476803c59 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -375,9 +375,13 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) {
 
 RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite)
 {
-  Node resultNode =
-      LinearRewriteStrategy<RewriteRule<EvalComp>, RewriteRule<BvComp> >::apply(
-          node);
+  Node resultNode = LinearRewriteStrategy<RewriteRule<EvalComp>>::apply(node);
+
+  if (node == resultNode && RewriteRule<BvComp>::applies(node))
+  {
+    resultNode = RewriteRule<BvComp>::run<false>(node);
+    return RewriteResponse(REWRITE_AGAIN, resultNode);
+  }
 
   return RewriteResponse(REWRITE_DONE, resultNode);
 }