diff --git a/contrib/cmake/src/tactic/core/CMakeLists.txt b/contrib/cmake/src/tactic/core/CMakeLists.txt
index ed3a84edf..fcd26bd84 100644
--- a/contrib/cmake/src/tactic/core/CMakeLists.txt
+++ b/contrib/cmake/src/tactic/core/CMakeLists.txt
@@ -3,6 +3,7 @@ z3_add_component(core_tactics
     blast_term_ite_tactic.cpp
     cofactor_elim_term_ite.cpp
     cofactor_term_ite_tactic.cpp
+    collect_statistics_tactic.cpp  
     ctx_simplify_tactic.cpp
     der_tactic.cpp
     distribute_forall_tactic.cpp
diff --git a/src/muz/pdr/pdr_reachable_cache.cpp b/src/muz/pdr/pdr_reachable_cache.cpp
index 85100c19f..2bedc1393 100644
--- a/src/muz/pdr/pdr_reachable_cache.cpp
+++ b/src/muz/pdr/pdr_reachable_cache.cpp
@@ -109,7 +109,12 @@ namespace pdr {
             UNREACHABLE();
             break;
         }
-        if (found) m_stats.m_hits++; m_stats.m_miss++;
+        if (found) {
+            m_stats.m_hits++; 
+        }
+        else {
+            m_stats.m_miss++;
+        }
         return found;
     }
 
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 8e96c925d..ee7559500 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -691,7 +691,10 @@ namespace smt {
         m_rw.reset();
         m_th_rw.reset();        
         m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());        
-        if (m_factory) dealloc(m_factory); m_factory = 0;
+        if (m_factory) {
+            dealloc(m_factory); 
+            m_factory = 0;
+        }
         ast_manager & m = get_manager();
         dec_ref_map_key_values(m, m_conversions);
         dec_ref_collection_values(m, m_is_added_to_model);
diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp
index ecc27eccf..677438cdf 100644
--- a/src/tactic/probe.cpp
+++ b/src/tactic/probe.cpp
@@ -287,14 +287,14 @@ struct is_non_qfbv_predicate {
         if (fid == m.get_basic_family_id())
             return;
         if (fid == u.get_family_id()) {
-			if (n->get_decl_kind() == OP_BSDIV0 ||
-				n->get_decl_kind() == OP_BUDIV0 ||
-				n->get_decl_kind() == OP_BSREM0 ||
-				n->get_decl_kind() == OP_BUREM0 ||
-				n->get_decl_kind() == OP_BSMOD0)
-				throw found();
-			return;
-		}
+            if (n->get_decl_kind() == OP_BSDIV0 ||
+                n->get_decl_kind() == OP_BUDIV0 ||
+                n->get_decl_kind() == OP_BSREM0 ||
+                n->get_decl_kind() == OP_BUREM0 ||
+                n->get_decl_kind() == OP_BSMOD0)
+                throw found();
+            return;
+        }
         if (is_uninterp_const(n))
             return;
         throw found();