From ea127c8ab93ecadb2a07f7dbe1bd2aec78b84614 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Thu, 27 Jun 2013 12:24:18 -0700
Subject: [PATCH] some confusion about proof generation

---
 src/tactic/goal.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 03a13aba5..51d7fedb0 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -255,7 +255,8 @@ void goal::get_formulas(ptr_vector<expr> & result) {
 }
 
 void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
-    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
+    // KLM: don't know why this assertion is no longer true 
+    // SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
     if (m_inconsistent)
         return;
     if (proofs_enabled()) {