diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 5579660b2..28df07d02 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -636,7 +636,6 @@ goal * goal::translate(ast_translation & translator) const {
     return res;
 }
 
-
 bool goal::sat_preserved() const {
     return prec() == PRECISE || prec() == UNDER;
 }
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 98df761c8..ba4e7e661 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -814,7 +814,7 @@ class repeat_tactical : public unary_tactical {
             if (r1[0]->is_decided()) {
                 result.push_back(r1[0]);  
                 return;                                                                                     
-            }                                                                                               
+            }                          
             goal_ref r1_0 = r1[0];                                                                          
             operator()(depth+1, r1_0, result); 
         }                                                                                                   
diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp
index 09b2bd00c..c79834518 100644
--- a/src/tactic/ufbv/ufbv_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_tactic.cpp
@@ -32,7 +32,7 @@ Notes:
 
 
 static tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) {
-    return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p)));
+    return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p)), 5);
 }
 
 static tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {