Merge branch '1.2.x'

3 files changed, 18 insertions, 1 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 1c275add7..370bdfcf0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -42,6 +42,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
   d_input(input),
   d_symtabAllocated(),
   d_symtab(&d_symtabAllocated),
+  d_assertionLevel(0),
   d_anonymousFunctionCount(0),
   d_done(false),
   d_checksEnabled(true),
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ee37f331e..53f5d10f3 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1311,6 +1311,18 @@ 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")) {
+    Debug("lemma-ites") << "removed ITEs from lemma: " << node << std::endl;
+    Debug("lemma-ites") << " + now have the following "
+                        << additionalLemmas.size() << " lemma(s):" << std::endl;
+    for(std::vector<Node>::const_iterator i = additionalLemmas.begin();
+        i != additionalLemmas.end();
+        ++i) {
+      Debug("lemma-ites") << " + " << *i << std::endl;
+    }
+    Debug("lemma-ites") << std::endl;
+  }
+
   // assert to prop engine
   d_propEngine->assertLemma(additionalLemmas[0], negated, removable);
   for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index f26bbe0aa..7d4948251 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -30,7 +30,11 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
 {
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
     std::vector<Node> quantVar;
-    output[i] = run(output[i], output, iteSkolemMap, quantVar);
+    // Do this in two steps to avoid Node problems(?)
+    // Appears related to bug 512, splitting this into two lines
+    // fixes the bug on clang on Mac OS
+    Node itesRemoved = run(output[i], output, iteSkolemMap, quantVar);
+    output[i] = itesRemoved;
   }
 }