From c20b391cf78be4f29210ff7b08d3125a34113b3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 May 2016 14:32:51 -0700 Subject: [PATCH] reduce warnings Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.cpp | 1 - src/smt/theory_array.cpp | 2 +- src/smt/theory_datatype.cpp | 2 +- src/smt/theory_fpa.cpp | 2 -- 4 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 727832d70..2bacb3a4f 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -194,7 +194,6 @@ class mbp::impl { void filter_variables(model& model, app_ref_vector& vars, expr_ref_vector& lits, expr_ref_vector& unused_lits) { - ast_manager& m = vars.get_manager(); expr_mark lit_visited; project_plugin::mark_rec(lit_visited, lits); diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index ef6b0e776..5e0539787 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -75,7 +75,7 @@ namespace smt { ast_manager& m = get_manager(); context& ctx = get_context(); theory_var r = theory_array_base::mk_var(n); - VERIFY(r == m_find.mk_var()); + VERIFY(r == static_cast(m_find.mk_var())); SASSERT(r == static_cast(m_var_data.size())); m_var_data.push_back(alloc(var_data)); var_data * d = m_var_data[r]; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index e5c8b1313..8e140661b 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -198,7 +198,7 @@ namespace smt { theory_var theory_datatype::mk_var(enode * n) { theory_var r = theory::mk_var(n); - VERIFY(r == m_find.mk_var()); + VERIFY(r == static_cast(m_find.mk_var())); SASSERT(r == static_cast(m_var_data.size())); m_var_data.push_back(alloc(var_data)); var_data * d = m_var_data[r]; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index b97b35e24..552d23631 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -88,8 +88,6 @@ namespace smt { } expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_max_unspecified(func_decl * f, expr * x, expr * y) { - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); expr_ref a(m), wrapped(m), wu(m), wu_eq(m); a = m.mk_app(f, x, y);