Merged bit-vector and uf proof branch.

1 files changed, 7 insertions, 2 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 9767ac7c7..593c522a8 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -99,7 +99,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
-  PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); );
+  PROOF (
+         ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
+         );
 }
 
 PropEngine::~PropEngine() {
@@ -117,7 +119,10 @@ void PropEngine::assertFormula(TNode node) {
   d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN);
 }
 
-void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) {
+void PropEngine::assertLemma(TNode node, bool negated,
+                             bool removable,
+                             ProofRule rule,
+                             TNode from) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;