mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
update solver only if there is a manager
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b03d4e4fc2
commit
6e05162df0
|
@ -627,7 +627,8 @@ void cmd_context::set_produce_proofs(bool f) {
|
|||
m_params.m_proof = f;
|
||||
if (has_manager()) {
|
||||
m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED);
|
||||
mk_solver();
|
||||
if (m_solver_factory)
|
||||
mk_solver();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue