From c85113acdbd2394dc40d545a514b4bad12da1ea4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 12 Apr 2020 15:25:08 -0700
Subject: [PATCH] fix #3928

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp | 24 ------------------------
 src/cmd_context/cmd_context.h   |  1 -
 src/sat/sat_config.cpp          |  3 +++
 3 files changed, 3 insertions(+), 25 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 2aba7c89f..dcabeacbd 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -902,30 +902,6 @@ recfun::promise_def cmd_context::decl_rec_fun(const symbol &name, unsigned int a
     return get_recfun_plugin().mk_def(name, arity, domain, range);
 }
 
-// insert a recursive function as a regular quantified axiom
-void cmd_context::insert_rec_fun_as_axiom(func_decl *f, expr_ref_vector const& binding, svector<symbol> const &ids, expr* e) {
-    expr_ref eq(m());
-    app_ref lhs(m());
-    lhs = m().mk_app(f, binding.size(), binding.c_ptr());
-    eq  = m().mk_eq(lhs, e);
-    if (!ids.empty()) {
-        if (is_var(e)) {
-            ptr_vector<sort> domain;
-            for (expr* b : binding) domain.push_back(m().get_sort(b));
-            insert_macro(f->get_name(), domain.size(), domain.c_ptr(), e);
-            return;
-        }
-        if (!is_app(e)) {
-            throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)");
-        }
-        expr* pats[2] = { m().mk_pattern(lhs), m().mk_pattern(to_app(e)) };
-        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 2, pats);
-    }
-
-    assert_expr(eq);
-}
-
-
 void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* rhs) {
 
     TRACE("recfun", tout<< "define recfun " << f->get_name()  << " = " << mk_pp(rhs, m()) << "\n";);
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 8f0d8dbed..0f471179a 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -388,7 +388,6 @@ public:
     void model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t);
     void model_del(func_decl* f);
     void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
-    void insert_rec_fun_as_axiom(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
     func_decl * find_func_decl(symbol const & s) const;
     func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
                                unsigned arity, sort * const * domain, sort * range) const;
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 0adb8c94a..3b3bc43bf 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -248,6 +248,9 @@ namespace sat {
 
         sat_simplifier_params sp(_p);
         m_elim_vars = sp.elim_vars();
+
+        if (m_drat && (m_xor_solver || m_card_solver)) 
+            throw sat_param_exception("DRAT checking only works for pure CNF");
     }
 
     void config::collect_param_descrs(param_descrs & r) {