From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 10 Oct 2019 19:47:03 +0000 (-0500)
Subject: Warning instead of assertion for failing propagating instance (#3380)
X-Git-Tag: cvc5-1.0.0~3895
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c39dca48e7f0bff035cfff233c9d5224d9a0974;p=cvc5.git

Warning instead of assertion for failing propagating instance (#3380)
---

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