Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

4 files changed, 17 insertions, 2 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 4e813d646..b7ed0b2ec 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -636,6 +636,10 @@ void ArithProof::registerTerm(Expr term) {
     d_realMode = true;
   }
 
+  if (term.isVariable() && !ProofManager::getSkolemizationManager()->isSkolem(term)) {
+    d_declarations.insert(term);
+  }
+
   // recursively declare all other terms
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
     // could belong to other theories
@@ -824,6 +828,14 @@ void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren
 }
 
 void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
+  for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
+    Expr term = *it;
+    Assert(term.isVariable());
+    os << "(% " << ProofManager::sanitize(term) << " ";
+    os << "(term ";
+    os << term.getType() << ")\n";
+    paren << ")";
+  }
 }
 
 void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 126e89ed2..08985487d 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -53,7 +53,7 @@ protected:
   // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations
 
   //   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
-  // ExprSet d_declarations; // all the variable/function declarations
+  ExprSet d_declarations; // all the variable/function declarations
 
   bool d_realMode;
 
diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp
index 3a962f987..fb7df4576 100644
--- a/src/proof/lemma_proof.cpp
+++ b/src/proof/lemma_proof.cpp
@@ -34,7 +34,6 @@ std::set<Node> LemmaProofRecipe::ProofStep::getAssertions() const {
 }
 
 void LemmaProofRecipe::addStep(ProofStep& proofStep) {
-  std::list<ProofStep>::iterator existingFirstStep = d_proofSteps.begin();
   d_proofSteps.push_front(proofStep);
 }
 
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 1c9bb0ff0..5ce615366 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -272,6 +272,10 @@ void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) {
   } else {
     Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
     if(d_deps.find(n) == d_deps.end()) {
+      if (options::allowEmptyDependencies()) {
+        Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl;
+        return;
+      }
       InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
     }
     Assert(d_deps.find(n) != d_deps.end());