From e47cd27c8d544178d13379d19c81927d582a6eb5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 20 Aug 2017 16:18:25 -0700
Subject: [PATCH] compiler warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/spacer/spacer_generalizers.cpp | 2 +-
 src/muz/spacer/spacer_qe_project.cpp   | 2 +-
 src/smt/mam.cpp                        | 3 +--
 src/smt/theory_fpa.cpp                 | 5 +++--
 src/smt/theory_str.cpp                 | 2 +-
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp
index f16fb10e1..94c419493 100644
--- a/src/muz/spacer/spacer_generalizers.cpp
+++ b/src/muz/spacer/spacer_generalizers.cpp
@@ -133,7 +133,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma)
 
     unsigned uses_level;
     expr_ref_vector core(m);
-    VERIFY(pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core));
+    VERIFY(pt.is_invariant(old_level, lemma->get_expr(), uses_level, &core));
 
     CTRACE("spacer", old_sz > core.size(),
            tout << "unsat core reduced lemma from: "
diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp
index c06854cb0..0eec500e9 100644
--- a/src/muz/spacer/spacer_qe_project.cpp
+++ b/src/muz/spacer/spacer_qe_project.cpp
@@ -98,7 +98,7 @@ peq::peq (app* p, ast_manager& m):
     m_eq (m),
     m_arr_u (m)
 {
-    SASSERT (is_partial_eq (p));
+    VERIFY (is_partial_eq (p));
     SASSERT (m_arr_u.is_array (m_lhs) &&
              m_arr_u.is_array (m_rhs) &&
              m_eq_proc (m.get_sort (m_lhs), m.get_sort (m_rhs)));
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 73ede7319..2aa9d6095 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2080,16 +2080,15 @@ namespace smt {
     */
     enode_vector * interpreter::mk_depth1_vector(enode * n, func_decl * f, unsigned i) {
         enode_vector * v = mk_enode_vector();
-        unsigned num_args = n->get_num_args();
         n = n->get_root();
         enode_vector::const_iterator it  = n->begin_parents();
         enode_vector::const_iterator end = n->end_parents();
         for (; it != end; ++it) {
             enode * p = *it;
             if (p->get_decl() == f  && 
+                i < p->get_num_args() && 
                 m_context.is_relevant(p)  &&
                 p->is_cgr() &&
-                i < p->get_num_args() &&
                 p->get_arg(i)->get_root() == n) {
                 v->push_back(p);
             }
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 17349ead6..e8edfc7ec 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -237,8 +237,9 @@ namespace smt {
 
         if (m_fpa_util.is_fp(e)) {
             expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
-            res = m_bv_util.mk_concat(3, cargs);
-            m_th_rw((expr_ref&)res);
+            expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);            
+            m_th_rw(tmp);
+            res = to_app(tmp);
         }
         else {
             sort * es = m.get_sort(e);
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 0d963f8b9..88b044a90 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8567,7 +8567,7 @@ namespace smt {
         } else {
             TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;);
             expr_ref is_zero(ctx.mk_eq_atom(a, m_autil.mk_int(0)), m);
-            literal is_zero_l = mk_literal(is_zero);
+            /* literal is_zero_l = */ mk_literal(is_zero);
             axiomAdd = true;
             TRACE("str", ctx.display(tout););
             // NOT_IMPLEMENTED_YET();