From 9c39dca48e7f0bff035cfff233c9d5224d9a0974 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Oct 2019 14:47:03 -0500 Subject: Warning instead of assertion for failing propagating instance (#3380) --- src/theory/quantifiers/quant_conflict_find.cpp | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/quant_conflict_find.cpp') 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; } } -- cgit v1.2.3