diff options
| -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; } } |