From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 5 Sep 2013 13:37:01 +0000 (-0400)
Subject: Fix bugs/issues with missed-t-prop dump output
X-Git-Tag: cvc5-1.0.0~7287^2~30
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f3976ab39799149ea4dce5a45f75cf98bb39887;p=cvc5.git

Fix bugs/issues with missed-t-prop dump output
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 380231cca..f6616920a 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -467,15 +467,19 @@ void TheoryEngine::propagate(Theory::Effort effort) {
   CVC4_FOR_EACH_THEORY;
 
   if(Dump.isOn("missed-t-propagations")) {
-    for(unsigned i = 0; i < d_possiblePropagations.size(); ++ i) {
+    for(unsigned i = 0; i < d_possiblePropagations.size(); ++i) {
       Node atom = d_possiblePropagations[i];
       bool value;
-      if (!d_propEngine->hasValue(atom, value)) continue;
+      if(d_propEngine->hasValue(atom, value)) {
+        continue;
+      }
       // Doesn't have a value, check it (and the negation)
       if(d_hasPropagated.find(atom) == d_hasPropagated.end()) {
         Dump("missed-t-propagations")
           << CommentCommand("Completeness check for T-propagations; expect invalid")
+          << EchoCommand(atom.toString())
           << QueryCommand(atom.toExpr())
+          << EchoCommand(atom.notNode().toString())
           << QueryCommand(atom.notNode().toExpr());
       }
     }