From ebe9db14d58ac3fc3f15009f56becbe69b36e56e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 21 Aug 2017 14:13:43 -0700
Subject: [PATCH] fix regression exposed by segfault2.smt2 crash

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_core.cpp            | 6 +++---
 src/smt/proto_model/proto_model.cpp | 6 +++---
 src/smt/theory_seq.cpp              | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index 684d1b3c2..2f6137172 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -90,18 +90,18 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
 void model_core::unregister_decl(func_decl * d) {
     decl2expr::obj_map_entry * ec = m_interp.find_core(d);
     if (ec && ec->get_data().m_value != 0) {
-        m_manager.dec_ref(ec->get_data().m_key);
-        m_manager.dec_ref(ec->get_data().m_value);
         m_interp.remove(d);
         m_const_decls.erase(d);
+        m_manager.dec_ref(ec->get_data().m_key);
+        m_manager.dec_ref(ec->get_data().m_value);
         return;
     }
     
     decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
     if (ef && ef->get_data().m_value != 0) {
-        m_manager.dec_ref(ef->get_data().m_key);
         dealloc(ef->get_data().m_value);
         m_finterp.remove(d);
         m_func_decls.erase(d);
+        m_manager.dec_ref(ef->get_data().m_key);
     }
 }
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 9a5f2a1ca..9b218037e 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -10,7 +10,7 @@ Abstract:
     <abstract>
 
 Author:
-
+ 
     Leonardo de Moura (leonardo) 2007-03-08.
 
 Revision History:
@@ -359,8 +359,8 @@ void proto_model::complete_partial_funcs() {
 
     // m_func_decls may be "expanded" when we invoke get_some_value.
     // So, we must not use iterators to traverse it.
-    for (func_decl* f : m_func_decls) {
-        complete_partial_func(f);
+    for (unsigned i = 0; i < m_func_decls.size(); i++) {
+        complete_partial_func(m_func_decls[i]);
     }
 }
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index d988da54f..c91882dad 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -427,7 +427,7 @@ bool theory_seq::branch_unit_variable() {
             break;
         }
     }
-    CTRACE("seq", result, "branch unit variable";);
+    CTRACE("seq", result, tout << "branch unit variable";);
     return result;
 }
 
@@ -3552,7 +3552,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
             }
         }
     }
-    CTRACE("seq", !val.is_int(), "length is not an integer\n";);
+    CTRACE("seq", !val.is_int(), tout << "length is not an integer\n";);
     return val.is_int();
 }