mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
359ee818a5
commit
e47cd27c8d
|
@ -133,7 +133,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma)
|
|||
|
||||
unsigned uses_level;
|
||||
expr_ref_vector core(m);
|
||||
VERIFY(pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core));
|
||||
VERIFY(pt.is_invariant(old_level, lemma->get_expr(), uses_level, &core));
|
||||
|
||||
CTRACE("spacer", old_sz > core.size(),
|
||||
tout << "unsat core reduced lemma from: "
|
||||
|
|
|
@ -98,7 +98,7 @@ peq::peq (app* p, ast_manager& m):
|
|||
m_eq (m),
|
||||
m_arr_u (m)
|
||||
{
|
||||
SASSERT (is_partial_eq (p));
|
||||
VERIFY (is_partial_eq (p));
|
||||
SASSERT (m_arr_u.is_array (m_lhs) &&
|
||||
m_arr_u.is_array (m_rhs) &&
|
||||
m_eq_proc (m.get_sort (m_lhs), m.get_sort (m_rhs)));
|
||||
|
|
|
@ -2080,16 +2080,15 @@ namespace smt {
|
|||
*/
|
||||
enode_vector * interpreter::mk_depth1_vector(enode * n, func_decl * f, unsigned i) {
|
||||
enode_vector * v = mk_enode_vector();
|
||||
unsigned num_args = n->get_num_args();
|
||||
n = n->get_root();
|
||||
enode_vector::const_iterator it = n->begin_parents();
|
||||
enode_vector::const_iterator end = n->end_parents();
|
||||
for (; it != end; ++it) {
|
||||
enode * p = *it;
|
||||
if (p->get_decl() == f &&
|
||||
i < p->get_num_args() &&
|
||||
m_context.is_relevant(p) &&
|
||||
p->is_cgr() &&
|
||||
i < p->get_num_args() &&
|
||||
p->get_arg(i)->get_root() == n) {
|
||||
v->push_back(p);
|
||||
}
|
||||
|
|
|
@ -237,8 +237,9 @@ namespace smt {
|
|||
|
||||
if (m_fpa_util.is_fp(e)) {
|
||||
expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
|
||||
res = m_bv_util.mk_concat(3, cargs);
|
||||
m_th_rw((expr_ref&)res);
|
||||
expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);
|
||||
m_th_rw(tmp);
|
||||
res = to_app(tmp);
|
||||
}
|
||||
else {
|
||||
sort * es = m.get_sort(e);
|
||||
|
|
|
@ -8567,7 +8567,7 @@ namespace smt {
|
|||
} else {
|
||||
TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;);
|
||||
expr_ref is_zero(ctx.mk_eq_atom(a, m_autil.mk_int(0)), m);
|
||||
literal is_zero_l = mk_literal(is_zero);
|
||||
/* literal is_zero_l = */ mk_literal(is_zero);
|
||||
axiomAdd = true;
|
||||
TRACE("str", ctx.display(tout););
|
||||
// NOT_IMPLEMENTED_YET();
|
||||
|
|
Loading…
Reference in a new issue