From 5e034e495fdea9b44e945805b191faf7249711be Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Fri, 19 Feb 2021 10:33:41 +0000
Subject: [PATCH] fix compiler warnings

---
 src/api/api_opt.cpp              | 1 -
 src/ast/rewriter/seq_axioms.cpp  | 2 +-
 src/muz/rel/udoc_relation.cpp    | 1 -
 src/nlsat/nlsat_interval_set.cpp | 2 +-
 src/sat/smt/q_mbi.cpp            | 3 +--
 src/sat/smt/recfun_solver.cpp    | 1 -
 6 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 220e85241..8c2faec11 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -436,7 +436,6 @@ extern "C" {
     }
 
     static void optimize_on_model(opt::on_model_t& o, model_ref& m) {
-        Z3_context c = (Z3_context) o.c;
         auto model_eh = (void(*)(void*)) o.on_model;
         Z3_model_ref * m_ref = (Z3_model_ref*) o.m;
         m_ref->m_model = m.get();
diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 58a3cb34c..bcbee6274 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -26,8 +26,8 @@ Revision History:
 namespace seq {
 
     axioms::axioms(th_rewriter& r):
-        m_rewrite(r),
         m(r.m()),
+        m_rewrite(r),
         a(m),
         seq(m),
         m_sk(m, r),
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 9ecdcefdf..367475f77 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -262,7 +262,6 @@ namespace datalog {
             return true;
         }
         uint64_t n, sz;
-        ast_manager& m = get_ast_manager();
         if (dl.is_numeral(e, n) && dl.try_get_size(e->get_sort(), sz)) {
             num_bits = 0;
             while (sz > 0) ++num_bits, sz = sz/2;
diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp
index aa5053966..c50fcb5ea 100644
--- a/src/nlsat/nlsat_interval_set.cpp
+++ b/src/nlsat/nlsat_interval_set.cpp
@@ -80,7 +80,7 @@ namespace nlsat {
             TRACE("nlsat_interval", tout << "lower: "; am.display_decimal(tout, i.m_lower); tout << ", upper: "; am.display_decimal(tout, i.m_upper);
                   tout << "\ns: " << s << "\n";);
             SASSERT(s <= 0);
-            SASSERT(!is_zero(s) || !i.m_lower_open && !i.m_upper_open);            
+            SASSERT(!is_zero(s) || (!i.m_lower_open && !i.m_upper_open));
         }
         return true;
     }
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index bbaeb0ddf..582911222 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -513,8 +513,7 @@ namespace q {
 
     bool mbqi::first_offset(unsigned_vector& offsets, app_ref_vector const& vars) {
         offsets.reset();
-        for (app* _ : vars) 
-            offsets.push_back(0);
+        offsets.resize(vars.size(), 0);
         for (unsigned i = 0; i < vars.size(); ++i) 
             if (!next_offset(offsets, vars, i, 0))
                 return false;
diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp
index 40d5299c4..fbb96d9d6 100644
--- a/src/sat/smt/recfun_solver.cpp
+++ b/src/sat/smt/recfun_solver.cpp
@@ -269,7 +269,6 @@ namespace recfun {
 
     bool solver::post_visit(expr* e, bool sign, bool root) {
         euf::enode* n = expr2enode(e);
-        app* a = to_app(e);        
         SASSERT(!n || !n->is_attached_to(get_id()));
         if (!n) 
             n = mk_enode(e, false);