diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-10 14:47:03 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-10 14:47:03 -0500 |
commit | 9c39dca48e7f0bff035cfff233c9d5224d9a0974 (patch) | |
tree | ec9f73f6d585fb004b9b855bfe198f38d287fbb0 /src/theory/quantifiers/quant_conflict_find.cpp | |
parent | 2c77abd838c55269d78fcfb2ec44be0fdb089214 (diff) |
Warning instead of assertion for failing propagating instance (#3380)
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 2044fe22a..4b055f71c 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -602,7 +602,23 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, Trace("qcf-instance-check") << "...spurious." << std::endl; return true; }else{ - Assert(p->isPropagatingInstance(inst_eval)); + if (Configuration::isDebugBuild()) + { + if (!p->isPropagatingInstance(inst_eval)) + { + // Notice that this can happen in cases where: + // (1) x = -1*y is rewritten to y = -1*x, and + // (2) -1*y is a term in the master equality engine but -1*x is not. + // In other words, we determined that x = -1*y is a relevant + // equality to propagate since it involves two known terms, but + // after rewriting, the equality y = -1*x involves an unknown term + // -1*x. In this case, the equality is still relevant to propagate, + // despite the above function not being precise enough to realize + // it. We output a warning in debug for this. See #2993. + Trace("qcf-instance-check") + << "WARNING: not propagating." << std::endl; + } + } Trace("qcf-instance-check") << "...not spurious." << std::endl; } } @@ -2301,7 +2317,8 @@ bool QuantConflictFind::isPropagatingInstance(Node n) const else if (!getEqualityEngine()->hasTerm(cur)) { Trace("qcf-instance-check-debug") - << "...not propagating instance because of " << n << std::endl; + << "...not propagating instance because of " << cur << " " << ck + << std::endl; return false; } } |