mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 07:33:24 +00:00
Code Activity

set proof mode by default to avoid crash on pop if we set it later in duality

Browse source
This commit is contained in:
Ken McMillan 2013-05-27 19:22:19 -07:00
parent 058c8d2083
commit b27abc501e
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/ast.cpp
View file

@ -1305,6 +1305,10 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs):
} }
void ast_manager::init() { void ast_manager::init() {
// TODO: the following is a HACK to enable proofs in the old smt solver
// When we stop using that solver, this hack can be removed
m_proof_mode = PGM_FINE;
m_int_real_coercions = true; m_int_real_coercions = true;
m_debug_ref_count = false; m_debug_ref_count = false;
m_fresh_id = 0; m_fresh_id = 0;