From 16ad33bf399d1b9aa1e333bbb89b560ffc868632 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Jun 2016 18:15:51 -0700
Subject: [PATCH 1/2] add collection of statistics #652

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 contrib/cmake/src/tactic/core/CMakeLists.txt |  1 +
 src/tactic/probe.cpp                         | 16 ++++++++--------
 2 files changed, 9 insertions(+), 8 deletions(-)

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

From b11f9050e370376e43bd76f70ce5abb11da3ff6e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Jun 2016 18:20:25 -0700
Subject: [PATCH 2/2] fix bugs exposed from bad indentation warnings, #650

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/pdr/pdr_reachable_cache.cpp | 7 ++++++-
 src/smt/theory_fpa.cpp              | 5 ++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

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