From bcf0f671b8d893b5937ce7f4d073b1f10b969524 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 30 Jul 2021 23:27:37 -0700
Subject: [PATCH] disable drat inside of quantifier elaboration

---
 src/sat/smt/q_mbi.cpp | 3 ++-
 src/sat/smt/q_mbi.h   | 2 ++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index c7ed4913a..ba6bc77b3 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -42,6 +42,7 @@ namespace q {
         add_plugin(ap);
         add_plugin(alloc(mbp::datatype_project_plugin, m));
         add_plugin(alloc(mbp::array_project_plugin, m));
+        
     }
 
     lbool mbqi::operator()() {
@@ -565,7 +566,7 @@ namespace q {
 
     void mbqi::init_solver() {
         if (!m_solver)
-            m_solver = mk_smt2_solver(m, ctx.s().params());
+            m_solver = mk_smt2_solver(m, m_no_drat_params);
     }
 
     void mbqi::init_search() {
diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h
index 174462ca4..1920baa52 100644
--- a/src/sat/smt/q_mbi.h
+++ b/src/sat/smt/q_mbi.h
@@ -20,6 +20,7 @@ Author:
 #include "qe/mbp/mbp_plugin.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/q_model_fixer.h"
+#include "sat/sat_solver.h"
 
 namespace euf {
     class solver;
@@ -60,6 +61,7 @@ namespace q {
         stats                                  m_stats;
         model_fixer                            m_model_fixer;
         model_ref                              m_model;
+        sat::no_drat_params                    m_no_drat_params;
         ref<::solver>                          m_solver;
         scoped_ptr_vector<obj_hashtable<expr>> m_values;
         scoped_ptr_vector<mbp::project_plugin> m_plugins;