Merge branch 'master' of https://github.com/Z3Prover/z3

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

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;
     }
 

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);

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();