diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index c3ea69e77..45f85e154 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -708,6 +708,7 @@ struct nnf::imp {
     }
 
     bool process_app(app * t, frame & fr) {
+        TRACE("nnf", tout << mk_ismt2_pp(t, m()) << "\n";);
         SASSERT(m().is_bool(t));
         if (t->get_family_id() == m().get_basic_family_id()) {
             switch (static_cast<basic_op_kind>(t->get_decl_kind())) {
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 26b35f0ed..26ff0136c 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -196,6 +196,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
     ptr_buffer<expr> args;
     expr * null = static_cast<expr*>(0);
     todo.push_back(std::make_pair(e, null));
+    
 
     expr * a;
     expr * expanded_a;
@@ -254,6 +255,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
                     if (new_t.get() == 0) {
                         // t is interpreted or model completion is disabled.
                         m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
+                        TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";);
                         trail.push_back(new_t);
                         if (!is_app(new_t) || to_app(new_t)->get_decl() != f) {
                             // if the result is not of the form (f ...), then assume we must simplify it.
@@ -302,6 +304,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
                         else {
                             SASSERT(r1);
                             trail.push_back(r1);
+                            TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";);
                             expr * r2 = 0;
                             if (!eval_cache.find(r1.get(), r2)) {
                                 todo.back().second = r1;
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 8a40f9d7a..8ebfa2d71 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -815,7 +815,7 @@ namespace smt {
     }
 
     void setup::setup_seq() {
-        m_context.register_plugin(alloc(theory_seq, m_manager));
+        m_context.register_plugin(alloc(theory_seq_empty, m_manager));
     }
 
     void setup::setup_card() {