mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
4d0bc8c8b3
commit
72400f1869
|
@ -1515,11 +1515,11 @@ namespace z3 {
|
|||
Z3_ast r;
|
||||
if (a.is_int()) {
|
||||
expr zero = a.ctx().int_val(0);
|
||||
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, zero);
|
||||
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
|
||||
}
|
||||
else if (a.is_real()) {
|
||||
expr zero = a.ctx().real_val(0);
|
||||
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, zero);
|
||||
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
|
||||
}
|
||||
else {
|
||||
r = Z3_mk_fpa_abs(a.ctx(), a);
|
||||
|
|
|
@ -1210,7 +1210,7 @@ expr_ref pred_transformer::get_origin_summary (model &mdl,
|
|||
if (!is_quantifier(s) && !mdl.is_true(s)) {
|
||||
TRACE("spacer", tout << "Summary not true in the model: "
|
||||
<< mk_pp(s, m) << "\n";);
|
||||
return expr_ref(m);
|
||||
// return expr_ref(m);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -77,6 +77,7 @@ namespace qe {
|
|||
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
|
||||
for (unsigned i = 0; i < acc.size(); ++i) {
|
||||
arg = m.mk_fresh_const(acc[i]->get_name().str().c_str(), acc[i]->get_range());
|
||||
vars.push_back(arg);
|
||||
model.register_decl(arg->get_decl(), m_val->get_arg(i));
|
||||
args.push_back(arg);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue