mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
update solver only if there is a manager
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5b71f7cf9e
commit
b03d4e4fc2
|
@ -624,10 +624,11 @@ void cmd_context::set_produce_proofs(bool f) {
|
|||
if (m_params.m_proof == f)
|
||||
return;
|
||||
SASSERT(!has_assertions());
|
||||
if (has_manager())
|
||||
m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED);
|
||||
m_params.m_proof = f;
|
||||
mk_solver();
|
||||
if (has_manager()) {
|
||||
m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED);
|
||||
mk_solver();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue