Merged my changes from experimental branch (new array decision procedure,

translation to bit-vectors for QF_NIA).

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0355256a3..2185f22ff 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -303,11 +303,11 @@ class TheoryEngine {
       return d_engine->propagate(literal, d_theory);
     }
 
-    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) {
+    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false, bool sendAtoms = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST);
+      return d_engine->lemma(lemma, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST);
     }
 
     theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {