diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 9847e4264..a307df4bb 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -518,6 +518,12 @@ namespace z3 {
         sort(context & c, Z3_ast a):ast(c, a) {}
         sort(sort const & s):ast(s) {}
         operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
+
+        /**
+           \brief retrieve unique identifier for func_decl.
+         */
+        unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
+
         /**
            \brief Return true if this sort and \c s are equal.
         */
@@ -615,6 +621,11 @@ namespace z3 {
         operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
         func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
 
+        /**
+           \brief retrieve unique identifier for func_decl.
+         */
+        unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
+
         unsigned arity() const { return Z3_get_arity(ctx(), *this); }
         sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
         sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
@@ -771,6 +782,11 @@ namespace z3 {
             return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
         }
 
+        /**
+           \brief retrieve unique identifier for expression.
+         */
+        unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
+
         /**
            \brief Return int value of numeral, throw if result cannot fit in
            machine int
diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp
index 1aa923f1f..833c83820 100644
--- a/src/sat/sat_big.cpp
+++ b/src/sat/sat_big.cpp
@@ -172,6 +172,7 @@ namespace sat {
 
     void big::add_del(literal u, literal v) {
         if (u.index() > v.index()) std::swap(u, v);
+		
         m_del_bin[u.index()].push_back(v);
     }
 
@@ -210,7 +211,6 @@ namespace sat {
             }
             wlist.set_end(itprev);
         }        
-
         s.propagate(false);
         return elim;
     }
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index e2d05385b..52641736a 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -244,10 +244,10 @@ namespace sat {
     }
 
     void scc::reduce_tr() {
-        unsigned quota = 0, num_reduced = 0;
-        while ((num_reduced = reduce_tr(false)) > quota) { quota = std::max(100u, num_reduced / 2); }
-        quota = 0;
-        while ((num_reduced = reduce_tr(true))  > quota) { quota = std::max(100u, num_reduced / 2); }
+        unsigned quota = 0, num_reduced = 0, count = 0;
+        while ((num_reduced = reduce_tr(false)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); }
+        quota = 0; count = 0;
+        while ((num_reduced = reduce_tr(true))  > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); }
     }
 
     void scc::collect_statistics(statistics & st) const {