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

[cvc5.git] / src / theory / theory_engine.cpp

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 380231cca729e21e811c191afb88e2b5d79d260a..f6616920a72bd5edaa1a9ece4e8445a28b41f24b 100644 (file)
--- 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());
       }
     }