diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 0b25a250b..fcff20afc 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -290,6 +290,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
 
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
+        TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << "\n";);
         if (a == b) {
             result = m.mk_true();
             return BR_DONE;
@@ -315,6 +316,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 conj.push_back(m.mk_eq(else1, else2));
             }
             if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
+                TRACE("model_evalator", tout << "argss are unique";);
                 return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
             }
 
@@ -329,7 +331,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 expr_ref s2(m_ar.mk_select(args2.size(), args2.c_ptr()), m);
                 conj.push_back(m.mk_eq(s1, s2));
             }
-            result = m.mk_and(conj.size(), conj.c_ptr());
+            result = mk_and(conj);
+            TRACE("model_evaluator", tout << mk_pp(a, m) << " == " << mk_pp(b, m) << " -> " << conj << "\n";
+                  for (auto& s : stores1) tout << "store: " << s << "\n";
+                  );
             return BR_REWRITE_FULL;
         }
         return BR_FAILED;
@@ -454,7 +459,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
         func_interp* g = m_model.get_func_interp(f);
-		if (!g) return false;
+        if (!g) return false;
         unsigned sz = g->num_entries();
         unsigned arity = f->get_arity();
         unsigned base_sz = stores.size();
diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h
index fbbbd12f8..43a967729 100644
--- a/src/muz/rel/dl_sparse_table.h
+++ b/src/muz/rel/dl_sparse_table.h
@@ -326,29 +326,29 @@ namespace datalog {
         public:
             unsigned m_offset; //!< in bits
             unsigned m_length; //!< in bits
-
-            column_info(unsigned offset, unsigned length) \
-                    : m_big_offset(offset/8), 
-                    m_small_offset(offset%8),
-                    m_mask( length==64 ? ULLONG_MAX : (static_cast<uint64_t>(1)<<length)-1 ),
-                    m_write_mask( ~(m_mask<<m_small_offset) ),
-                    m_offset(offset), 
-                    m_length(length) {
-                SASSERT(length<=64);
-                SASSERT(length+m_small_offset<=64);
+            
+            column_info(unsigned offset, unsigned length) 
+                : m_big_offset(offset / 8), 
+                  m_small_offset(offset % 8),
+                  m_mask( length == 64 ? ULLONG_MAX : (static_cast<uint64_t>(1)<<length)-1 ),
+                  m_write_mask( ~(m_mask << m_small_offset) ),
+                  m_offset(offset), 
+                  m_length(length) {
+                SASSERT(length <= 64);
+                SASSERT(length + m_small_offset <= 64);
             }
             table_element get(const char * rec) const {
-                const uint64_t * ptr = reinterpret_cast<const uint64_t*>(rec+m_big_offset);
+                const uint64_t * ptr = reinterpret_cast<const uint64_t*>(rec + m_big_offset);
                 uint64_t res = *ptr;
-                res>>=m_small_offset;
-                res&=m_mask;
+                res >>= m_small_offset;
+                res &= m_mask;
                 return res;
             }
             void set(char * rec, table_element val) const {
                 SASSERT( (val&~m_mask)==0 ); //the value fits into the column
-                uint64_t * ptr = reinterpret_cast<uint64_t*>(rec+m_big_offset);
-                *ptr&=m_write_mask;
-                *ptr|=val<<m_small_offset;
+                uint64_t * ptr = reinterpret_cast<uint64_t*>(rec + m_big_offset);
+                *ptr &= m_write_mask;
+                *ptr |= val << m_small_offset;
             }
             unsigned next_ofs() const { return m_offset+m_length; }
         };
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 765cc87f5..5ab52b57c 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -438,7 +438,7 @@ namespace smt {
                 }
                 else if (!check(q)) {
                     if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
-                        verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
+                        IF_VERBOSE(0, verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n");
                     }
                     TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
                     num_failures++;
diff --git a/src/util/util.h b/src/util/util.h
index 6e7ee5ce5..77204977e 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -193,8 +193,10 @@ bool is_threaded();
 
 #ifdef _MSC_VER
 #define DO_PRAGMA(x) __pragma(x)
+#define PRAGMA_LOCK __pragma(omp critical (verbose_lock))
 #else
 #define DO_PRAGMA(x) _Pragma(#x)
+#define PRAGMA_LOCK _Pragma("omp critical (verbose_lock){)
 #endif
 
 #ifdef _NO_OMP_
@@ -202,7 +204,7 @@ bool is_threaded();
 #else
 #define LOCK_CODE(CODE)                         \
     {                                           \
-        DO_PRAGMA(omp critical (verbose_lock))   \
+        PRAGMA_LOCK   \
             {                                   \
                 CODE;                           \
             }                                   \