From dbde71c2905db352dbb83d8b5e177aa68e6762ea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 5 Dec 2012 12:05:07 -0800
Subject: [PATCH] fixing unit tests

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_model_checker.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index cefdacef5..53f3af961 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -283,7 +283,6 @@ namespace smt {
         if (!m_fparams) {
             m_fparams = alloc(smt_params, m_context->get_fparams());
             m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
-            m_fparams->m_proof_mode = m_manager.proof_mode();            
         }
         if (!m_aux_context) {
             symbol logic;