mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

fix misc compiler warnings

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-02-15 11:53:24 +00:00
parent 614caaca62
commit d3fb5f2a4c
4 changed files with 6 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/rel/dl_base.cpp
View file

@ -189,8 +189,7 @@ namespace datalog {
union_find_default_ctx uf_ctx; union_find_default_ctx uf_ctx;
union_find<> uf(uf_ctx); //the numbers in uf correspond to column indexes after the join union_find<> uf(uf_ctx); //the numbers in uf correspond to column indexes after the join
for(unsigned i=0; i<join_sig_sz; i++) { for(unsigned i=0; i<join_sig_sz; i++) {
unsigned v = uf.mk_var(); VERIFY(uf.mk_var() == i);
SASSERT(v==i);
} }
for(unsigned i=0; i<joined_col_cnt; i++) { for(unsigned i=0; i<joined_col_cnt; i++) {

3
src/smt/smt_implied_equalities.cpp
View file

@ -166,11 +166,10 @@ namespace smt {
terms[i].term = m.mk_app(m_array_util.get_family_id(), OP_SELECT, 0, 0, args.size(), args.c_ptr()); terms[i].term = m.mk_app(m_array_util.get_family_id(), OP_SELECT, 0, 0, args.size(), args.c_ptr());
} }
assert_relevant(terms); assert_relevant(terms);
lbool is_sat = m_solver.check_sat(0,0); VERIFY(m_solver.check_sat(0,0) != l_false);
model_ref model1; model_ref model1;
m_solver.get_model(model1); m_solver.get_model(model1);
SASSERT(model1.get()); SASSERT(model1.get());
SASSERT(is_sat != l_false);
get_implied_equalities_model_based(model1, terms); get_implied_equalities_model_based(model1, terms);
m_solver.pop(1); m_solver.pop(1);
return; return;

9
src/smt/theory_arith_core.h
View file

@ -564,11 +564,9 @@ namespace smt {
template<typename Ext> template<typename Ext>
theory_var theory_arith<Ext>::internalize_numeral(app * n) { theory_var theory_arith<Ext>::internalize_numeral(app * n) {
rational _val; rational _val;
context & ctx = get_context(); VERIFY(m_util.is_numeral(n, _val));
bool flag = m_util.is_numeral(n, _val);
numeral val(_val); numeral val(_val);
SASSERT(flag); SASSERT(!get_context().e_internalized(n));
SASSERT(!ctx.e_internalized(n));
enode * e = mk_enode(n); enode * e = mk_enode(n);
// internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant. // internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
// e->mark_as_interpreted(); // e->mark_as_interpreted();
@ -3117,8 +3115,7 @@ namespace smt {
del_vars(get_old_num_vars(num_scopes)); del_vars(get_old_num_vars(num_scopes));
m_scopes.shrink(new_lvl); m_scopes.shrink(new_lvl);
theory::pop_scope_eh(num_scopes); theory::pop_scope_eh(num_scopes);
bool r = make_feasible(); VERIFY(make_feasible());
SASSERT(r);
SASSERT(m_to_patch.empty()); SASSERT(m_to_patch.empty());
m_to_check.reset(); m_to_check.reset();
m_in_to_check.reset(); m_in_to_check.reset();

3
src/smt/theory_array_base.cpp
View file

@ -645,11 +645,10 @@ namespace smt {
if (is_store(n)) { if (is_store(n)) {
theory_var w = n->get_arg(0)->get_th_var(get_id()); theory_var w = n->get_arg(0)->get_th_var(get_id());
SASSERT(w != null_theory_var); SASSERT(w != null_theory_var);
ast_manager& m = get_manager();
mg_merge(v, get_representative(w)); mg_merge(v, get_representative(w));
TRACE("array", tout << "merge: " << mk_pp(n->get_owner(), m) << " " << v << " " << w << "\n";); TRACE("array", tout << "merge: " << mk_pp(n->get_owner(), get_manager()) << " " << v << " " << w << "\n";);
} }
else if (is_const(n)) { else if (is_const(n)) {
set_default(v, n->get_arg(0)); set_default(v, n->get_arg(0));