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 1/2] 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()) {

From d8b31773b80965ae7bf7bf9e1766aef86f44b2ed Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Thu, 27 Jun 2013 17:27:36 -0700
Subject: [PATCH 2/2] some debugging stuff

---
 src/interp/iz3interp.cpp           | 15 ++++++++++++++-
 src/interp/iz3translate_direct.cpp | 10 ++++++----
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index aac8648ba..ac6970231 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -190,6 +190,16 @@ public:
     return true;
   }
 
+  void test_secondary(const std::vector<ast> &cnsts,
+			     const std::vector<int> &parents,
+			     std::vector<ast> &interps
+			     ){
+    int num = cnsts.size();
+    iz3secondary *sp = iz3foci::create(this,num,(int *)(parents.empty()?0:&parents[0]));
+    int res = sp->interpolate(cnsts, interps);
+    if(res != 0)
+      throw "secondary failed";
+  }                         
 
   void proof_to_interpolant(z3pf proof,
 			    const std::vector<ast> &cnsts,
@@ -198,7 +208,10 @@ public:
 			    const std::vector<ast> &theory,
 			    interpolation_options_struct *options = 0
 			    ){
-    
+#if 0
+    test_secondary(cnsts,parents,interps);
+    return;
+#endif
     profiling::timer_start("Interpolation prep");
 
     // get rid of frames not used in proof
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index da05c6642..58ebb67f7 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -39,6 +39,7 @@ using namespace stl_ext;
 
 
 static int lemma_count = 0;
+static int nll_lemma_count = 0;
 #define SHOW_LEMMA_COUNT -1
 
 // One half of a resolution. We need this to distinguish
@@ -764,7 +765,8 @@ public:
 
 
 #if 1
-    //    std::cout << "lemma: " << ++lemma_count << "\n";
+    ++lemma_count;
+    //    std::cout << "lemma: " << lemma_count << "\n";
     if(lemma_count == SHOW_LEMMA_COUNT){
       for(unsigned i = 0; i < lits.size(); i++)
         show_lit(lits[i]);
@@ -1337,7 +1339,7 @@ public:
     return res;
   }
 
-// #define NEW_EXTRACT_TH_LEMMA
+  //#define NEW_EXTRACT_TH_LEMMA
 
   void get_local_hyps(const ast &proof, std::set<ast> &res){
     std::set<ast> hyps = get_hyps(proof);
@@ -1372,7 +1374,7 @@ public:
       }
     }
 #ifdef NEW_EXTRACT_TH_LEMMA
-    bool lemma_nll = nargs > 1;
+    bool lemma_nll = nprems > 1;
     if(nll && !lemma_nll){
       lemma_nll = false;
       // std::cout << "lemma count = " << nll_lemma_count << "\n";
@@ -1394,7 +1396,7 @@ public:
     try {
       res = extract_th_lemma_common(lits,nll,lemma_nll);
     }
-#if 0
+#if 1
     catch (const invalid_lemma &) {
       std::cout << "\n\nlemma: " << my_count;
       std::cout << "\n\nproof node: \n";