summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f6616920a..448e3a8fa 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -212,7 +212,7 @@ void TheoryEngine::preRegister(TNode preprocessed) {
}
}
if (multipleTheories) {
- // Collect the shared terms if there are multipe theories
+ // Collect the shared terms if there are multiple theories
NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
}
}
@@ -1317,7 +1317,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
d_iteRemover.run(additionalLemmas, iteSkolemMap);
additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
- if(Trace.isOn("lemma-ites")) {
+ if(Debug.isOn("lemma-ites")) {
Debug("lemma-ites") << "removed ITEs from lemma: " << node << endl;
Debug("lemma-ites") << " + now have the following "
<< additionalLemmas.size() << " lemma(s):" << endl;
@@ -1417,7 +1417,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
- // If a treu constant or a negation of a false constant we can ignore it
+ // If a true constant or a negation of a false constant we can ignore it
if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
++ i;
continue;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback