diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index da05c6642..1b93e9828 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -764,7 +764,7 @@ public:
 
 
 #if 1
-    //    std::cout << "lemma: " << ++lemma_count << "\n";
+    std::cout << "lemma: " << ++lemma_count << std::endl;
     if(lemma_count == SHOW_LEMMA_COUNT){
       for(unsigned i = 0; i < lits.size(); i++)
         show_lit(lits[i]);
@@ -786,6 +786,8 @@ public:
     int sat = secondary->interpolate(preds,itps);
     profiling::timer_stop("foci");
 
+    std::cout << "lemma done" << std::endl;
+
     // if sat, lemma isn't valid, something is wrong
     if(sat){
 #if 1
@@ -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);
diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp
index 275d59f5d..016731e3a 100644
--- a/src/muz_qe/duality_dl_interface.cpp
+++ b/src/muz_qe/duality_dl_interface.cpp
@@ -373,7 +373,7 @@ void dl_interface::cancel() {
 #else
   // HACK: duality can't cancel at all times, we just exit here
   std::cout << "(error \"duality canceled\")\nunknown\n";
-  exit(0);
+  abort();
 #endif
 }