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.

diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 47986c9663d18dffafe901396b162e31ec17ae1e..245e7cb8a5660075ff73ddd9f66f6ffe2d84ac05 100644 (file)
--- 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]);
+          }
         }
       }
     }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5f82aedf1657a4d6712f6c14e392eeb6509d5b28..00aa786ae6fe23468321c5ea9ef76cbe8e9aaa98 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1568,6 +1568,7 @@ set(regress_1_tests
   regress1/quantifiers/issue4243-prereg-inc.smt2
   regress1/quantifiers/issue4290-cegqi-r.smt2
   regress1/quantifiers/issue4620-erq-witness-unsound.smt2
+  regress1/quantifiers/issue4685-wrewrite.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2

diff --git a/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2 b/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2
new file mode 100644 (file)
index 0000000..d88faa4
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue4685-wrewrite.smt2
@@ -0,0 +1,4 @@
+(set-logic NIRA)
+(set-info :status sat)
+(assert (forall ((a Int) (b Int)) (or (> a 0) (<= a (/ 0 (+ 0.5 b))))))
+(check-sat)