mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 23:43:15 +00:00
Code Activity

fix #7725 - proofs are only possible if context was created with proofs enabled

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-07-12 09:14:12 +02:00
parent e575919657
commit fd5455422e
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/goal.cpp
View file

@ -57,11 +57,10 @@ goal::goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_
m_ref_count(0), m_ref_count(0),
m_depth(0), m_depth(0),
m_models_enabled(models_enabled), m_models_enabled(models_enabled),
m_proofs_enabled(proofs_enabled), m_proofs_enabled(proofs_enabled && m.proofs_enabled()),
m_core_enabled(core_enabled), m_core_enabled(core_enabled),
m_inconsistent(false), m_inconsistent(false),
m_precision(PRECISE) { m_precision(PRECISE) {
SASSERT(!proofs_enabled || m.proofs_enabled());
} }
goal::goal(goal const & src): goal::goal(goal const & src):