mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
134562162a
commit
574246ff7a
|
@ -150,9 +150,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
auto st = reduce_app_core(f, num, args, result, result_pr);
|
||||
CTRACE("model_evaluator", st != BR_FAILED,
|
||||
tout << f->get_name() << "\n";
|
||||
for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << "\n";
|
||||
tout << result << "\n";);
|
||||
tout << f->get_name() << " ";
|
||||
for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " ";
|
||||
tout << "\n--> " << result << "\n";);
|
||||
|
||||
return st;
|
||||
}
|
||||
|
|
|
@ -299,13 +299,12 @@ namespace q {
|
|||
auto* p = get_plugin(v);
|
||||
if (p && !fmls_extracted) {
|
||||
TRACE("q", tout << "domain eqs\n" << qb.domain_eqs << "\n";);
|
||||
|
||||
for (expr* e : qb.domain_eqs)
|
||||
if (!m_model->is_true(e))
|
||||
return expr_ref(nullptr, m);
|
||||
|
||||
|
||||
fmls.append(qb.domain_eqs);
|
||||
eliminate_nested_vars(fmls, qb);
|
||||
for (expr* e : fmls)
|
||||
if (!m_model->is_true(e))
|
||||
return expr_ref(nullptr, m);
|
||||
mbp::project_plugin proj(m);
|
||||
proj.extract_literals(*m_model, vars, fmls);
|
||||
fmls_extracted = true;
|
||||
|
|
Loading…
Reference in a new issue