mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
10145366b2
commit
2fa156eaf4
|
@ -176,6 +176,7 @@ namespace array {
|
|||
TRACE("array", tout << "v" << v_child << " - " << ctx.bpp(select) << " " << ctx.bpp(child) << " prop: " << should_prop_upward(get_var_data(v_child)) << "\n";);
|
||||
if (can_beta_reduce(child))
|
||||
push_axiom(select_axiom(select, child));
|
||||
propagate_parent_select_axioms(v_child);
|
||||
}
|
||||
|
||||
void solver::add_lambda(theory_var v, euf::enode* lambda) {
|
||||
|
|
|
@ -93,7 +93,10 @@ namespace fpa {
|
|||
SASSERT(m.is_bool(e));
|
||||
if (!visit_rec(m, e, sign, root, redundant))
|
||||
return sat::null_literal;
|
||||
return expr2literal(e);
|
||||
sat::literal lit = expr2literal(e);
|
||||
if (sign)
|
||||
lit.neg();
|
||||
return lit;
|
||||
}
|
||||
|
||||
void solver::internalize(expr* e, bool redundant) {
|
||||
|
|
Loading…
Reference in a new issue