diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-09 20:07:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-09 20:07:21 -0500 |
commit | ba7cda7a9cb02a38b1cf8fd9fbd85304a9056a5e (patch) | |
tree | 3d7d957f19d6cda9de4022c93c9ea01fad4fe6b8 /src/theory/builtin | |
parent | 8ff3b306b7b35bc1040a6caee759929c4e497373 (diff) |
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.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 13 |
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]); + } } } } |