mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

dealing with build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-04 21:39:20 -07:00
parent 65dff93e93
commit 5ef0fdc9c8
2 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz_qe/dl_mk_quantifier_instantiation.cpp
View file

@ -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;

4
src/muz_qe/fdd.cpp
View file

@ -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<unsigned>(OFFSET_OF(this, node, m_ref_count)), 11);
}
bool node::operator==(node const& other) const {