From 6f273e7b8f8f595dea418cfe221e2a73e4cd582f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 11 Nov 2017 12:09:33 -0800
Subject: [PATCH] bug fixes in uninitialized variables

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_asymm_branch.cpp | 4 ++++
 src/sat/sat_asymm_branch.h   | 5 ++++-
 src/sat/sat_simplifier.cpp   | 3 ++-
 src/sat/sat_solver.cpp       | 1 +
 4 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 83574749e..abf1d95be 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -29,6 +29,7 @@ namespace sat {
         m_counter(0) {
         updt_params(p);
         reset_statistics();
+        m_calls = 0;
     }
 
     struct clause_size_lt {
@@ -57,6 +58,9 @@ namespace sat {
     };
     
     void asymm_branch::operator()(bool force) {
+        ++m_calls;
+        if (m_calls <= 1)
+            return;
         if (!m_asymm_branch && !m_asymm_branch_all)
             return;
         s.propagate(false); // must propagate, since it uses s.push()
diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h
index a11692a82..a6e44a4e2 100644
--- a/src/sat/sat_asymm_branch.h
+++ b/src/sat/sat_asymm_branch.h
@@ -33,7 +33,8 @@ namespace sat {
         solver & s;
         int64      m_counter;
         random_gen m_rand;
-
+        unsigned   m_calls;
+        
         // config
         bool                   m_asymm_branch;
         bool                   m_asymm_branch_all;
@@ -63,6 +64,8 @@ namespace sat {
         void collect_statistics(statistics & st) const;
         void reset_statistics();
 
+        void init_search() { m_calls = 0; }
+
         inline void dec(unsigned c) { m_counter -= c; }
     };
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 89b07ddd4..656bff104 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -104,7 +104,7 @@ namespace sat {
         return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); 
     }
     bool simplifier::abce_enabled() const { 
-        return !m_incremental_mode && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; 
+        return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; 
     }
     bool simplifier::bca_enabled()  const { 
         return !m_incremental_mode && !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded(); 
@@ -1868,6 +1868,7 @@ namespace sat {
         m_cce                     = p.cce();
         m_acce                    = p.acce();
         m_bca                     = p.bca();
+        m_abce                    = p.abce();
         m_bce_delay               = p.bce_delay();
         m_elim_blocked_clauses    = p.elim_blocked_clauses();
         m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 149d6feea..b0b5d8495 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1422,6 +1422,7 @@ namespace sat {
         m_next_simplify           = 0;
         m_min_d_tk                = 1.0;
         m_search_lvl              = 0;
+        m_asymm_branch.init_search();
         m_stopwatch.reset();
         m_stopwatch.start();
         m_core.reset();