diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp
index 56bada7c1..239fd9008 100644
--- a/src/ast/normal_forms/pull_quant.cpp
+++ b/src/ast/normal_forms/pull_quant.cpp
@@ -244,7 +244,7 @@ struct pull_quant::imp {
                     quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
                     proof * p1 = 0;
                     if (n != q1) {
-                        proof * p0 = m_manager.mk_pull_quant(to_quantifier(n)->get_expr(), to_quantifier(new_expr));
+                        proof * p0 = m_manager.mk_pull_quant(n, to_quantifier(new_expr));
                         p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0);
                     }
                     proof * p2 = q1 == r ? 0 : m_manager.mk_pull_quant(q1, to_quantifier(r));
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index 1aace7716..dd08ac9db 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -37,6 +37,7 @@ struct check_logic::imp {
     datatype_util m_dt_util;
     pb_util       m_pb_util;
     bool          m_uf;        // true if the logic supports uninterpreted functions
+    bool          m_dt;        // true if the lgoic supports dattypes
     bool          m_arrays;    // true if the logic supports arbitrary arrays
     bool          m_bv_arrays; // true if the logic supports only bv arrays
     bool          m_reals;     // true if the logic supports reals
@@ -53,6 +54,7 @@ struct check_logic::imp {
 
     void reset() {
         m_uf          = false;
+        m_dt          = false;
         m_arrays      = false;
         m_bv_arrays   = false;
         m_reals       = false;
@@ -105,6 +107,10 @@ struct check_logic::imp {
             m_uf        = true;
             m_bvs       = true;
         }
+        else if (logic == "QF_DT") {
+            m_uf        = true;            
+            m_dt        = true;
+        }
         else if (logic == "QF_AUFLIA") {
             m_uf     = true;
             m_arrays = true;
@@ -187,6 +193,7 @@ struct check_logic::imp {
             m_bvs         = true;
             m_uf          = true;
             m_ints        = true;
+            m_dt          = true;
             m_nonlinear   = true; // non-linear 0-1 variables may get eliminated
         }
         else {
@@ -443,7 +450,7 @@ struct check_logic::imp {
         else if (fid == m_seq_util.get_family_id()) {
             // nothing to check
         }
-        else if (fid == m_dt_util.get_family_id() && m_logic == "QF_FD") {
+        else if (fid == m_dt_util.get_family_id() && m_dt) {
             // nothing to check
         }
         else if (fid == m_pb_util.get_family_id() && m_logic == "QF_FD") {
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 50b49f3b8..56b5d541a 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -125,6 +125,8 @@ namespace smt {
             setup_QF_FPBV();
         else if (m_logic == "QF_S")
             setup_QF_S();
+        else if (m_logic == "QF_DT")
+            setup_QF_DT();
         else
             setup_unknown();
     }
@@ -190,6 +192,8 @@ namespace smt {
                 setup_AUFLIRA();
             else if (m_logic == "UFNIA")
                 setup_UFNIA();
+            else if (m_logic == "QF_DT")
+                setup_QF_DT();
             else if (m_logic == "LRA")
                 setup_LRA();
             else 
@@ -210,6 +214,10 @@ namespace smt {
         m_params.m_random_initial_activity = IA_RANDOM;
     }
 
+    void setup::setup_QF_DT() {
+        setup_QF_UF();
+    }
+
     void setup::setup_QF_BVRE() {
         setup_QF_BV();
         setup_QF_LIA();
diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h
index a3bb29195..924c2caec 100644
--- a/src/smt/smt_setup.h
+++ b/src/smt/smt_setup.h
@@ -54,6 +54,7 @@ namespace smt {
         // setup_<logic>(static_features & st) can only be used if the logical context will perform a single 
         // check.
         // 
+        void setup_QF_DT();
         void setup_QF_UF();
         void setup_QF_UF(static_features const & st);
         void setup_QF_RDL();
diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index 75cd0f2bb..874f1cfcc 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -141,7 +141,7 @@ bool smt_logics::logic_has_fpa(symbol const & s) {
 }
 
 bool smt_logics::logic_has_uf(symbol const & s) {
-    return s == "QF_UF" || s == "UF";
+    return s == "QF_UF" || s == "UF" || s == "QF_DT";
 }
 
 bool smt_logics::logic_has_horn(symbol const& s) {
@@ -153,5 +153,5 @@ bool smt_logics::logic_has_pb(symbol const& s) {
 }
 
 bool smt_logics::logic_has_datatype(symbol const& s) {
-    return s == "QF_FD" || s == "ALL";
+    return s == "QF_FD" || s == "ALL" || s == "QF_DT";
 }