fix #3957

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/tactic/tactical.cpp

@@ -792,76 +792,79 @@ class repeat_tactical : public unary_tactical {
     void operator()(unsigned depth,
                     goal_ref const & in, 
                     goal_ref_buffer& result) {
-        // TODO: implement a non-recursive version.
-        if (depth > m_max_depth) {
-            result.push_back(in.get());
-            return;
-        }
 
         bool models_enabled = in->models_enabled();
         bool proofs_enabled = in->proofs_enabled();
         bool cores_enabled  = in->unsat_core_enabled();
 
         ast_manager & m = in->m();                                                                          
         goal_ref_buffer      r1;  
-        result.reset();          
+        goal_ref g = in;
+        unsigned r1_size = 0;
+        result.reset();      
+    try_goal:
+        r1.reset();
+        if (depth > m_max_depth) {
+            result.push_back(g.get());
+            return;
+        }
         {
-            goal orig_in(in->m(), proofs_enabled, models_enabled, cores_enabled);
-            orig_in.copy_from(*(in.get()));
-            m_t->operator()(in, r1);                                                            
+            goal orig_in(g->m(), proofs_enabled, models_enabled, cores_enabled);
+            orig_in.copy_from(*(g.get()));
+            m_t->operator()(g, r1);                                                            
             if (r1.size() == 1 && is_equal(orig_in, *(r1[0]))) {
                 result.push_back(r1[0]);
                 return;                                                                                     
             }
         }
-        unsigned r1_size = r1.size();                                                                       
-        SASSERT(r1_size > 0);                                                                               
+        r1_size = r1.size();                                                                       
+        SASSERT(r1_size > 0);    
         if (r1_size == 1) {                                                                                 
             if (r1[0]->is_decided()) {
                 result.push_back(r1[0]);  
                 return;                                                                                     
             }                          
-            goal_ref r1_0 = r1[0];                                                                          
-            operator()(depth+1, r1_0, result); 
-        }                                                                                                   
-        else {
-            goal_ref_buffer            r2;                                                                  
-            for (unsigned i = 0; i < r1_size; i++) {                                                        
-                goal_ref g = r1[i];                                                                         
-                r2.reset();                   
-                operator()(depth+1, g, r2);                                              
-                if (is_decided(r2)) {
-                    SASSERT(r2.size() == 1);
-                    if (is_decided_sat(r2)) {                                                          
-                        // found solution...                                                                
-                        result.push_back(r2[0]);
-                        return;                                                                             
-                    }                                                                                       
-                    else {                                                                                  
-                        SASSERT(is_decided_unsat(r2));
-                    }                                                                                       
-                }                                                                                           
-                else {                                                                                      
-                    result.append(r2.size(), r2.c_ptr());                                                           
-                }                                                                                           
-            }    
-                                                                                           
-            if (result.empty()) {                                                                           
-                // all subgoals were shown to be unsat.                                                     
-                // create an decided_unsat goal with the proof
-                in->reset_all();
-                proof_ref pr(m);
-                expr_dependency_ref core(m);
-                if (proofs_enabled) {
-                    apply(m, in->pc(), pr);                    
-                }
-                if (cores_enabled && in->dc()) {
-                    core = (*in->dc())();
-                }
-                in->assert_expr(m.mk_false(), pr, core);
-                result.push_back(in.get());
-            }
-        }
+            g = r1[0];   
+            depth++;
+            goto try_goal;
+        }                      
+
+		goal_ref_buffer            r2;
+		for (unsigned i = 0; i < r1_size; i++) {
+			goal_ref g = r1[i];
+			r2.reset();
+			operator()(depth + 1, g, r2);
+			if (is_decided(r2)) {
+				SASSERT(r2.size() == 1);
+				if (is_decided_sat(r2)) {
+					// found solution...                                                                
+					result.push_back(r2[0]);
+					return;
+				}
+				else {
+					SASSERT(is_decided_unsat(r2));
+				}
+			}
+			else {
+				result.append(r2.size(), r2.c_ptr());
+			}
+		}
+
+		if (result.empty()) {
+			// all subgoals were shown to be unsat.                                                     
+			// create an decided_unsat goal with the proof
+			g->reset_all();
+			proof_ref pr(m);
+			expr_dependency_ref core(m);
+			if (proofs_enabled) {
+				apply(m, g->pc(), pr);
+			}
+			if (cores_enabled && g->dc()) {
+				core = (*g->dc())();
+			}
+			g->assert_expr(m.mk_false(), pr, core);
+			result.push_back(g.get());
+		}
     }
 
 public: