Ensure legal elimination for witness rewrite (#4688)

Fixes #4685.

A recent commit #4661 added assertions for checking whether a witness rewrite corresponded to a legal elimination. #4685 demonstrates that these assertions can be violated and hence should be checked to ensure the rewrite is sound.

1 files changed, 8 insertions, 5 deletions

diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 47986c966..245e7cb8a 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -103,11 +103,14 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
         {
           Trace("builtin-rewrite") << "Witness rewrite: " << node << " --> "
                                    << node[1][1 - i] << std::endl;
-          // based on the witness terms we construct, this should be a legal
-          // elimination, since t should not contain x and be a subtype of x.
-          Assert(!expr::hasSubterm(node[1][1 - i], node[0][0]));
-          Assert(node[1][i].getType().isSubtypeOf(node[0][0].getType()));
-          return RewriteResponse(REWRITE_DONE, node[1][1 - i]);
+          // also must be a legal elimination: the other side of the equality
+          // cannot contain the variable, and it must be a subtype of the
+          // variable
+          if (!expr::hasSubterm(node[1][1 - i], node[0][0]) &&
+              node[1][i].getType().isSubtypeOf(node[0][0].getType()))
+          {
+            return RewriteResponse(REWRITE_DONE, node[1][1 - i]);
+          }
         }
       }
     }