From b27abc501ea31586337ce65cca54865533e3792c Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 27 May 2013 19:22:19 -0700 Subject: [PATCH] set proof mode by default to avoid crash on pop if we set it later in duality --- src/ast/ast.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 8ecaed172..da3c80f06 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1305,6 +1305,10 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs): } 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_debug_ref_count = false; m_fresh_id = 0;