From 794aafa6f84c7967cb7ef4a186f392727c4ae5a4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 23 Jan 2020 12:14:34 -0600
Subject: [PATCH] fix warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/extra_cmds/dbg_cmds.cpp | 2 +-
 src/qe/qe_term_graph.cpp                | 3 ++-
 src/sat/sat_aig_simplifier.cpp          | 2 +-
 src/smt/theory_fpa.cpp                  | 1 -
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index 47a2f65ee..3b6b2224c 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -398,7 +398,7 @@ public:
         ast_manager& m = ctx.m();
         qe::interpolator mbi(m);
         expr_ref itp(m);
-        lbool res = mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
+         mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
         ctx.regular_stream() << itp << "\n";
     }
 };
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index 33a0c02bb..1dc01678a 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -1267,11 +1267,12 @@ namespace qe {
         for (auto const& terms : partitions) {
             expr* a = nullptr;
             for (expr* b : terms) { 
-                if (is_uninterp(b)) 
+                if (is_uninterp(b)) { 
                     if (a) 
                         result.push_back(m.mk_eq(a, b));
                     else 
                         a = b;
+                }
             }
         }
         TRACE("qe", tout << result << "\n";);
diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp
index ba5b74b15..20d3735b4 100644
--- a/src/sat/sat_aig_simplifier.cpp
+++ b/src/sat/sat_aig_simplifier.cpp
@@ -426,7 +426,7 @@ namespace sat {
         // Assign higher cutset budgets to equality candidates that come from simulation
         // touch them to trigger recomputation of cutsets.
         u64_map<literal> val2lit;
-        unsigned i = 0, j = 0, num_eqs = 0;
+        unsigned i = 0, num_eqs = 0;
         for (cut_val val : var2val) {
             if (!s.was_eliminated(i) && s.value(i) == l_undef) {
                 literal u(i, false), v;
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index abad855c5..e103c8242 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -724,7 +724,6 @@ namespace smt {
     void theory_fpa::init_model(model_generator & mg) {
         TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout););
         ast_manager & m = get_manager();
-        context & ctx = get_context();
         m_factory = alloc(fpa_value_factory, m, get_family_id());
         mg.register_factory(m_factory);
     }