From 8dde1bf86df40d11ecabd2dc96bf4d94fb3162a1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Apr 2020 16:02:32 -0700
Subject: [PATCH] compiler warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/mam.cpp                   | 15 ++++++++-------
 src/smt/smt_quantifier.cpp        |  1 +
 src/tactic/ufbv/ufbv_rewriter.cpp |  4 ++--
 3 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index abf2e8ac8..93a189edf 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -386,12 +386,6 @@ namespace {
     //
     // ------------------------------------
 
-    inline enode * get_enode(context & ctx, app * n) {
-        SASSERT(ctx.e_internalized(n));
-        enode * e = ctx.get_enode(n);
-        SASSERT(e);
-        return e;
-    }
     inline enode * mk_enode(context & ctx, quantifier * qa, app * n) {
         ctx.internalize(n, false, ctx.get_generation(qa));
         enode * e = ctx.get_enode(n);
@@ -446,6 +440,13 @@ namespace {
         }
 
 #ifdef Z3DEBUG
+        inline enode * get_enode(context & ctx, app * n) const {
+            SASSERT(ctx.e_internalized(n));
+            enode * e = ctx.get_enode(n);
+            SASSERT(e);
+            return e;
+        }
+
         void display_label_hashes_core(std::ostream & out, app * p) const {
             if (p->is_ground()) {
                 enode * e = get_enode(*m_context, p);
@@ -587,7 +588,7 @@ namespace {
         }
     };
 
-    inline std::ostream & operator<<(std::ostream & out, code_tree const & tree) {
+    std::ostream & operator<<(std::ostream & out, code_tree const & tree) {
         tree.display(out);
         return out;
     }
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 974828501..521a28c01 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -622,6 +622,7 @@ namespace smt {
         void assign_eh(quantifier * q) override {
             m_active = true;
             ast_manager& m = m_context->get_manager();
+            (void)m;
             if (!m_fparams->m_ematching) {
                 return;
             }
diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp
index 2411b9340..59bfe5a86 100644
--- a/src/tactic/ufbv/ufbv_rewriter.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter.cpp
@@ -34,8 +34,8 @@ ufbv_rewriter::ufbv_rewriter(ast_manager & m):
     m_new_args(m), 
     m_rewrite_todo(m),
     m_rewrite_cache(m),
-    m_new_exprs(m),
-    m_in_processed(m) {
+    m_in_processed(m),
+    m_new_exprs(m) {
     params_ref p;
     p.set_bool("elim_and", true);
     m_bsimp.updt_params(p);