From ba7cda7a9cb02a38b1cf8fd9fbd85304a9056a5e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 Jul 2020 20:07:21 -0500 Subject: [PATCH] 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. --- src/theory/builtin/theory_builtin_rewriter.cpp | 13 ++++++++----- test/regress/CMakeLists.txt | 1 + .../regress1/quantifiers/issue4685-wrewrite.smt2 | 4 ++++ 3 files changed, 13 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue4685-wrewrite.smt2 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) -- 2.30.2