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 2044fe22af7229253f53c41ab7492a0f45d60e89..4b055f71c967a04378e58290056cdce5eab60289 100644 (file)
--- 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;
       }
     }