From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 10 Jul 2020 01:07:21 +0000 (-0500)
Subject: Ensure legal elimination for witness rewrite (#4688)
X-Git-Tag: cvc5-1.0.0~3137
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba7cda7a9cb02a38b1cf8fd9fbd85304a9056a5e;p=cvc5.git

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 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]);
+          }
         }
       }
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5f82aedf1..00aa786ae 100644
--- 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
index 000000000..d88faa441
--- /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)