diff --git a/lib/ast_smt_pp.cpp b/lib/ast_smt_pp.cpp
index 0dcd78101..aa3a9c76d 100644
--- a/lib/ast_smt_pp.cpp
+++ b/lib/ast_smt_pp.cpp
@@ -602,12 +602,22 @@ class smt_printer {
                 }
             }
 
-            m_out << " :pat { ";
+            if (m_is_smt2) {
+                m_out << " :pattern ( ";
+            }
+            else {
+                m_out << " :pat { ";
+            }
             for (unsigned j = 0; j < pat->get_num_args(); ++j) {
                 print_no_lets(pat->get_arg(j));
                 m_out << " ";
             }
-            m_out << "}";
+            if (m_is_smt2) {
+                m_out << ")";
+            }
+            else {
+                m_out << "}";
+            }
         }
         if (m_is_smt2 && q->get_num_patterns() > 0) {
             m_out << ")";
diff --git a/lib/dl_bmc_engine.cpp b/lib/dl_bmc_engine.cpp
index 99512f89a..f1071d106 100644
--- a/lib/dl_bmc_engine.cpp
+++ b/lib/dl_bmc_engine.cpp
@@ -27,6 +27,7 @@ Revision History:
 #include "dl_decl_plugin.h"
 #include "bool_rewriter.h"
 #include "model_smt2_pp.h"
+#include "ast_smt_pp.h"
 
 namespace datalog {
     bmc::bmc(context& ctx): 
@@ -711,7 +712,11 @@ namespace datalog {
             md->eval(trace, trace);
             md->eval(path, path);
             IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n";);
-            IF_VERBOSE(2, m_solver.display(verbose_stream()); verbose_stream() << "\n";);
+            ast_smt_pp pp(m);
+            for (unsigned i = 0; i < m_solver.size(); ++i) {
+                pp.add_assumption(m_solver.get_formulas()[i]);
+            }
+            IF_VERBOSE(2, pp.display_smt2(verbose_stream(), m.mk_true()); verbose_stream() << "\n";);
             m_answer = get_proof(md, to_app(trace), to_app(path));
             is_sat = l_true;
         }
diff --git a/lib/dl_check_table.cpp b/lib/dl_check_table.cpp
index 1b1dd4974..d7dfbe1ae 100644
--- a/lib/dl_check_table.cpp
+++ b/lib/dl_check_table.cpp
@@ -96,6 +96,9 @@ namespace datalog {
             (*m_tocheck)(tocheck(tgt), tocheck(src), tocheck(delta));
             (*m_checker)(checker(tgt), checker(src), checker(delta));
             get(tgt).well_formed();
+            if (delta) {
+                get(*delta).well_formed();
+            }
         }
     };
 
diff --git a/lib/pdr_farkas_learner.cpp b/lib/pdr_farkas_learner.cpp
index a9a6956c3..5a5352207 100644
--- a/lib/pdr_farkas_learner.cpp
+++ b/lib/pdr_farkas_learner.cpp
@@ -329,7 +329,7 @@ namespace pdr {
         m_ctx->pop(1);
 
         IF_VERBOSE(3, {
-                for (unsigned i = 0; i < lemmas.size(); ++i) {
+                for (unsigned i = 0; i < ilemmas.size(); ++i) {
                     verbose_stream() << "B': " << mk_pp(ilemmas[i].get(), m) << "\n";
                 }
             });