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;
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index a642be9d6..4dc770056 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -49,13 +49,8 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
 
     dl_decl_util decl_util(m);
 
-<<<<<<< HEAD
-    context ctx_q(m, fparams);   
-    params.set_bool(":magic-sets-for-queries", use_magic_sets);
-=======
     context ctx_q(m, fparams);
     params.set_bool("magic_sets_for_queries", use_magic_sets);
->>>>>>> 3736c5ea3b97521dad85cdc6262151fae2875ec5
     ctx_q.updt_params(params);
     {
         parser* p = parser::create(ctx_q,m);