From d8a2e9d008791cab0e903ee62009e4f658316e8b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 15 Nov 2017 15:57:07 -0800
Subject: [PATCH] initialize glue in constructor to ensure it gets set

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp         | 13 ++++---------
 src/sat/sat_clause.cpp  |  4 +++-
 src/sat/sat_lookahead.h |  4 +++-
 src/sat/sat_solver.cpp  |  7 ++-----
 4 files changed, 12 insertions(+), 16 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index a6c4ab8fc..ba591083f 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1514,21 +1514,16 @@ void ast_manager::compress_ids() {
     ptr_vector<ast> asts;
     m_expr_id_gen.cleanup();
     m_decl_id_gen.cleanup(c_first_decl_id);
-    ast_table::iterator it  = m_ast_table.begin();
-    ast_table::iterator end = m_ast_table.end();
-    for (; it != end; ++it) {
-        ast * n = *it;
+    for (ast* n : m_ast_table) {
         if (is_decl(n))
             n->m_id = m_decl_id_gen.mk();
         else
             n->m_id = m_expr_id_gen.mk();
         asts.push_back(n);
-    }
+    }    
     m_ast_table.finalize();
-    ptr_vector<ast>::iterator it2  = asts.begin();
-    ptr_vector<ast>::iterator end2 = asts.end();
-    for (; it2 != end2; ++it2)
-        m_ast_table.insert(*it2);
+    for (ast* a : asts) 
+        m_ast_table.insert(a);
 }
 
 void ast_manager::raise_exception(char const * msg) {
diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index 90d542a14..8b7a4ca46 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -33,7 +33,9 @@ namespace sat {
         m_used(false),
         m_frozen(false),
         m_reinit_stack(false),
-        m_inact_rounds(0) {
+        m_inact_rounds(0),
+        m_glue(255),
+        m_psm(255) {
         memcpy(m_lits, lits, sizeof(literal) * sz);
         mark_strengthened();
         SASSERT(check_approx());
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 9f110b1a0..e65e7021a 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -84,9 +84,11 @@ namespace sat {
             double   m_cube_fraction;
 
             config() {
-                m_max_hlevel = 50;
+                memset(this, sizeof(*this), 0);
+                m_dl_success = 0.8;
                 m_alpha = 3.5;
                 m_max_score = 20.0;
+                m_max_hlevel = 50;
                 m_min_cutoff = 30;
                 m_preselect = false;
                 m_level_cand = 600;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 42b10d5c8..2980fffeb 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1762,11 +1762,8 @@ namespace sat {
        \brief Compute the psm of all learned clauses.
     */
     void solver::save_psm() {
-        clause_vector::iterator it  = m_learned.begin();
-        clause_vector::iterator end = m_learned.end();
-        for (; it != end; ++it) {
-            clause & c = *(*it);
-            c.set_psm(psm(c));
+        for (clause* cp : m_learned) {
+            cp->set_psm(psm(*cp));
         }
     }