mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix #6371
This commit is contained in:
parent
b9cba82531
commit
876ca2f1a5
|
@ -826,7 +826,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
result = elim_unused_vars(m(), q1, params_ref());
|
||||
|
||||
|
||||
TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << "\n";);
|
||||
|
||||
result_pr = nullptr;
|
||||
if (m().proofs_enabled()) {
|
||||
|
@ -835,6 +834,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
p2 = m().mk_elim_unused_vars(q1, result);
|
||||
result_pr = m().mk_transitivity(p1, p2);
|
||||
}
|
||||
|
||||
TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << " " << result_pr << "\n" ;);
|
||||
|
||||
SASSERT(old_q->get_sort() == result->get_sort());
|
||||
return true;
|
||||
}
|
||||
|
|
|
@ -621,10 +621,15 @@ void cmd_context::set_produce_unsat_cores(bool f) {
|
|||
}
|
||||
|
||||
void cmd_context::set_produce_proofs(bool f) {
|
||||
SASSERT(!has_assertions() || m_params.m_proof == f);
|
||||
if (has_manager())
|
||||
if (m_params.m_proof == f)
|
||||
return;
|
||||
SASSERT(!has_assertions());
|
||||
if (has_manager()) {
|
||||
m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED);
|
||||
std::cout << m_params.m_proof << " " << f << "\n";
|
||||
}
|
||||
m_params.m_proof = f;
|
||||
mk_solver();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -171,7 +171,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
|
|||
else
|
||||
pr = m.mk_modus_ponens(in_pr, pr);
|
||||
}
|
||||
TRACE("assert_expr_bug", tout << "after...\n" << r << "\n";);
|
||||
TRACE("assert_expr_bug", tout << "after...\n" << r << "\n" << pr << "\n";);
|
||||
}
|
||||
|
||||
m_has_quantifiers |= ::has_quantifiers(e);
|
||||
|
|
Loading…
Reference in a new issue