From d64bc795f0f2a5e6ecdca17c1f5143a348a5d5be Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 30 Oct 2020 10:10:54 -0700
Subject: [PATCH] wrong assert, compiler warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp     | 1 -
 src/sat/smt/arith_solver.cpp    | 1 -
 src/sat/smt/bv_internalize.cpp  | 2 +-
 src/sat/smt/euf_internalize.cpp | 1 -
 src/sat/smt/euf_solver.cpp      | 1 -
 src/sat/smt/q_mbi.cpp           | 2 --
 6 files changed, 1 insertion(+), 7 deletions(-)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 27e5b3db9..5c3202e8a 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1679,7 +1679,6 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
     lbool nullable(l_false);
     unsigned min_length(0), lower_bound(0), upper_bound(UINT_MAX);
     bool is_value(false);
-    bool normalized(false);
     if (e->get_family_id() == u.get_family_id()) {
         switch (e->get_decl()->get_decl_kind()) {
         case OP_RE_EMPTY_SET:
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 0b0359530..489ff66c9 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -911,7 +911,6 @@ namespace arith {
             theory_var v = (i + start) % sz;
             if (is_bool(v))
                 continue;
-            enode* n1 = var2enode(v);
             ensure_column(v);
             if (!can_get_ivalue(v))
                 continue;
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 9e39a1ffa..bce5e1118 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -139,7 +139,7 @@ namespace bv {
             n = mk_enode(e, suppress_args);
 
         SASSERT(!n->is_attached_to(get_id()));
-        theory_var v = mk_var(n);
+        mk_var(n);
         SASSERT(n->is_attached_to(get_id()));
         if (internalize_mode::no_delay_i != get_internalize_mode(a)) 
             mk_bits(n->get_th_var(get_id()));
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index b52b58f83..b31a7090e 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -21,7 +21,6 @@ Author:
 namespace euf {
 
     void solver::internalize(expr* e, bool redundant) {
-        SASSERT(!get_enode(e) || get_enode(e)->bool_var() < UINT_MAX);
         if (get_enode(e))
             return;
         if (si.is_bool_op(e))
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index b103df9d3..302e1edd0 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -276,7 +276,6 @@ namespace euf {
             return;
         bool sign = l.sign();                
         m_egraph.set_value(n, sign ? l_false : l_true);
-        auto const & j = s().get_justification(l);
         for (auto th : enode_th_vars(n))
             m_id2solver[th.get_id()]->asserted(l);
 
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index bf6db5dd9..db6baef9e 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -166,7 +166,6 @@ namespace q {
             flatten_and(fml, result->vbody);
         }
         expr_ref& mbody = result->mbody;
-        unsigned sz = q->get_num_decls();
         if (!m_model->eval_expr(q->get_expr(), mbody, true))
             return nullptr;
 
@@ -187,7 +186,6 @@ namespace q {
     */
     expr_ref mbqi::basic_project(model& mdl, quantifier* q, app_ref_vector& vars) {
         unsigned sz = q->get_num_decls();
-        unsigned max_generation = 0;
         expr_ref_vector vals(m);
         vals.resize(sz, nullptr);
         for (unsigned i = 0; i < sz; ++i) {