From 2f3976ab39799149ea4dce5a45f75cf98bb39887 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 5 Sep 2013 09:37:01 -0400 Subject: [PATCH] Fix bugs/issues with missed-t-prop dump output --- src/theory/theory_engine.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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()); } } -- 2.30.2