diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-05 09:37:01 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-05 15:17:37 -0400 |
commit | 2f3976ab39799149ea4dce5a45f75cf98bb39887 (patch) | |
tree | 97c037df8ad6afde56daabaf14056a794d18663c | |
parent | b3a4670710d3ffdc99879a1d27f37cf775af18eb (diff) |
Fix bugs/issues with missed-t-prop dump output
-rw-r--r-- | src/theory/theory_engine.cpp | 8 |
1 files 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()); } } |