From 0cd406ca0baf3df353681751dcb65229734d736e Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 30 Jul 2015 09:09:13 +0100
Subject: [PATCH] Fixed initialization order and unused variable warnings.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/muz/base/dl_rule_set.cpp  | 2 +-
 src/smt/smt_model_checker.cpp | 4 ++--
 src/smt/smt_model_finder.cpp  | 8 ++++----
 src/smt/theory_array_full.cpp | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index 555b592ef..7d02bfdd6 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -457,7 +457,7 @@ namespace datalog {
             rule * r = *it;
             app * head = r->get_head();
             func_decl * head_decl = head->get_decl();
-            unsigned head_strat = get_predicate_strat(head_decl);
+            // unsigned head_strat = get_predicate_strat(head_decl);
             unsigned n = r->get_tail_size();
             for (unsigned i = 0; i < n; i++) {
                 func_decl * tail_decl = r->get_tail(i)->get_decl();
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 4a1d9c6e6..9c20c5deb 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -40,8 +40,8 @@ namespace smt {
         m_max_cexs(1),
         m_iteration_idx(0),
         m_curr_model(0),
-        m_new_instances_bindings(m),
-        m_cancel(false) {
+        m_cancel(false),
+        m_new_instances_bindings(m) {
     }
 
     model_checker::~model_checker() {
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 80851bac7..d8f18a123 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -2431,8 +2431,8 @@ namespace smt {
                 m_array_util(m), 
                 m_arith_util(m),
                 m_bv_util(m),
-                m_info(0),
-                m_cancel(false) {
+                m_cancel(false),
+                m_info(0) {
             }
             
                 
@@ -3285,8 +3285,8 @@ namespace smt {
         m_sm_solver(alloc(simple_macro_solver, m, m_q2info)),
         m_hint_solver(alloc(hint_solver, m, m_q2info)),
         m_nm_solver(alloc(non_auf_macro_solver, m, m_q2info, m_dependencies)),
-        m_new_constraints(m),
-        m_cancel(false) {
+        m_cancel(false),
+        m_new_constraints(m) {
     }
     
     model_finder::~model_finder() {
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 4e169a8be..91f5b68ec 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -778,7 +778,7 @@ namespace smt {
         TRACE("array", 
               tout << mk_bounded_pp(v1, get_manager()) << "\n==\n" 
               << mk_bounded_pp(v2, get_manager()) << "\n";);
-        context& ctx = get_context();
+        
         if (m_eqs.contains(v1, v2)) {
             return false;
         }