From 5ef0fdc9c86eafed39c518525387703ccc96e374 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Apr 2013 21:39:20 -0700 Subject: [PATCH] dealing with build warnings Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_quantifier_instantiation.cpp | 1 - src/muz_qe/fdd.cpp | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.cpp b/src/muz_qe/dl_mk_quantifier_instantiation.cpp index 993e5ada5..1d80d9b77 100644 --- a/src/muz_qe/dl_mk_quantifier_instantiation.cpp +++ b/src/muz_qe/dl_mk_quantifier_instantiation.cpp @@ -83,7 +83,6 @@ namespace datalog { void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs) { - unsigned sz = pat->get_num_args(); m_binding.reset(); m_binding.resize(q->get_num_decls()); term_pairs todo; diff --git a/src/muz_qe/fdd.cpp b/src/muz_qe/fdd.cpp index 6b23f3a3f..9ca5f758a 100644 --- a/src/muz_qe/fdd.cpp +++ b/src/muz_qe/fdd.cpp @@ -23,12 +23,12 @@ Revision History: #include "bit_vector.h" #include "trace.h" -#define OFFSET_OF(ty, field) (unsigned char*)(&((ty*)(0))->field) - (unsigned char*)(ty*)(0) +#define OFFSET_OF(th, ty, field) (unsigned char*)(&((ty*)(th))->field) - (unsigned char*)(ty*)(th) using namespace fdd; unsigned node::get_hash() const { - return string_hash((char*)this, OFFSET_OF(node, m_ref_count), 11); + return string_hash((char*)this, static_cast(OFFSET_OF(this, node, m_ref_count)), 11); } bool node::operator==(node const& other) const {