diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp
index d5dac0811..5bcda972a 100755
--- a/src/duality/duality_profiling.cpp
+++ b/src/duality/duality_profiling.cpp
@@ -125,8 +125,18 @@ namespace Duality {
 
   void timer_stop(const char *name){
     if(current->name != name || !current->parent){
+#if 0
       std::cerr << "imbalanced timer_start and timer_stop";
       exit(1);
+#endif
+      // in case we lost a timer stop due to an exception
+      while(current->name != name && current->parent)
+	current = current->parent;
+      if(current->parent){
+	current->time += (current_time() - current->start_time);
+	current = current->parent;
+      }
+      return;
     }
     current->time += (current_time() - current->start_time);
     current = current->parent;
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 49e591be2..bbd1ebe0a 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -2252,22 +2252,27 @@ namespace Duality {
 	      int update_count = 0;
 	      for(unsigned i = 0; i < expansions.size(); i++){
 		Node *node = expansions[i];
-		tree->SolveSingleNode(top,node);
-#ifdef NO_GENERALIZE
-		node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
-#else
 		try {
+		  tree->SolveSingleNode(top,node);
+#ifdef NO_GENERALIZE
+		  node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
+#else
 		  if(expansions.size() == 1 && NodeTooComplicated(node))
 		    SimplifyNode(node);
 		  else
 		    node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
 		  Generalize(node);
+#endif
 		}
 		catch(const RPFP::Bad &){
 		  // bad interpolants can get us here
 		  throw DoRestart();
 		}
-#endif
+		catch(char const *msg){
+		  // bad interpolants can get us here
+		  reporter->Message(std::string("interpolation failure:") + msg);
+		  throw DoRestart();
+		}
 		if(RecordUpdate(node)){
 		  update_count++;
 		  total_updates++;
@@ -2283,8 +2288,14 @@ namespace Duality {
 	      if(update_count == 0){
 		if(was_sat){
 		  update_failures++;
-		  if(update_failures > 10)
-		    throw Incompleteness();
+		  if(update_failures > 10){
+		    for(unsigned i = 0; i < expansions.size(); i++){
+		      Node *node = expansions[i];
+		      node->map->Annotation.SetFull();
+		      reporter->Message("incompleteness: cleared annotation");
+		    }
+		    throw DoRestart();
+		  }
 		}
 		reporter->Message("backtracked without learning");
 	      }