diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 8b84e0848..a4c0cfec1 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -171,7 +171,7 @@ extern "C" {
         mk_c(c)->save_ast_trail(result.get());
         *v = of_ast(result.get());
         RETURN_Z3_model_eval true;
-        Z3_CATCH_RETURN(0);
+        Z3_CATCH_RETURN(false);
     }
 
     unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m) {
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 60d1a8c8a..a0ee29130 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -169,6 +169,29 @@ bool family_manager::has_family(symbol const & s) const {
     return m_families.contains(s);
 }
 
+#if 0
+static unsigned s_count = 0;
+void ast::inc_ref() {
+    SASSERT(m_ref_count < UINT_MAX);
+    m_ref_count ++;
+    if (get_id() == 1) {
+        s_count++;
+        if (s_count >= 36530) {
+            TRACE("rc", tout << "inc_ref " << m_ref_count << "\n";);
+        }
+    }
+}
+
+void ast::dec_ref() {
+    SASSERT(m_ref_count > 0);
+    m_ref_count --;
+    if (get_id() == 1 && s_count >= 36530) {
+        TRACE("rc", tout << "dec_ref " << m_ref_count << "\n";);
+        // IF_VERBOSE(0, verbose_stream() << "dec_rc " << s_count << "\n";);
+    }
+}
+#endif
+
 // -----------------------------------
 //
 // decl_info
@@ -1814,7 +1837,6 @@ ast * ast_manager::register_node_core(ast * n) {
 
 
     n->m_id   = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
-    
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index a551b8928..05b4c241e 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -482,6 +482,7 @@ protected:
     void *   m_mark2_owner;
 #endif
 
+#if 1
     void inc_ref() {
         SASSERT(m_ref_count < UINT_MAX);
         m_ref_count ++;
@@ -491,6 +492,12 @@ protected:
         SASSERT(m_ref_count > 0);
         m_ref_count --;
     }
+#else
+    void inc_ref();
+
+    void dec_ref();
+
+#endif
 
     ast(ast_kind k):m_id(UINT_MAX), m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false), m_ref_count(0) {
         DEBUG_CODE({
diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp
index 64a7d8ae7..3f62a8998 100644
--- a/src/sat/sat_ddfw.cpp
+++ b/src/sat/sat_ddfw.cpp
@@ -569,7 +569,6 @@ namespace sat {
             for (literal lit : get_clause(i)) {
                 if (is_true(lit)) found = true;
             }
-            SASSERT(ci.is_true() == found);
             SASSERT(found == !m_unsat.contains(i));
         }
         // every variable in a false clause is in unsat vars
diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index a4cb68506..e14b9434f 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -245,7 +245,7 @@ namespace smt {
         void mk_var_eh(bool_var v) override {
             expr * n = m_context.bool_var2expr(v);
             double act;
-            if (m_cache.find(n, act))
+            if (n && m_cache.find(n, act))
                 m_context.set_activity(v, act);
             act_case_split_queue::mk_var_eh(v);
         }
@@ -255,8 +255,10 @@ namespace smt {
                 double act = m_context.get_activity(v);
                 if (act > 0.0) {
                     expr * n = m_context.bool_var2expr(v);
-                    m_cache.insert(n, act);
-                    m_cache_domain.push_back(n);
+                    if (n) {
+                        m_cache.insert(n, act);
+                        m_cache_domain.push_back(n);
+                    }
                 }
             }
             act_case_split_queue::del_var_eh(v);
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index de3266480..2c8be490b 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -40,12 +40,14 @@ uint64_t reslimit::count() const {
 
 bool reslimit::inc() {
     ++m_count;
-    return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
+    bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
+    return r;
 }
 
 bool reslimit::inc(unsigned offset) {
     m_count += offset;
-    return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
+    bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
+    return r;
 }
 
 void reslimit::push(unsigned delta_limit) {