diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 782713d5c..cca0c5c1b 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -96,7 +96,6 @@ namespace sat {
                 if (!process(c))
                     continue; // clause was removed
                 *it2 = *it;
-                // throw exception to test bug fix: if (it2 != it) throw solver_exception("trigger bug");
                 ++it2;
             }
             s.m_clauses.set_end(it2);
@@ -129,14 +128,14 @@ namespace sat {
         // check if the clause is already satisfied
         for (i = 0; i < sz; i++) {
             if (s.value(c[i]) == l_true) {
-                s.dettach_clause(c);
+                s.detach_clause(c);
                 s.del_clause(c);
                 return false;
             }
         }
         // try asymmetric branching
         // clause must not be used for propagation
-        s.dettach_clause(c);
+        solver::scoped_detach scoped_d(s, c);
         s.push();
         for (i = 0; i < sz - 1; i++) {
             literal l = c[i];
@@ -154,7 +153,6 @@ namespace sat {
         SASSERT(s.m_qhead == s.m_trail.size());
         if (i == sz - 1) {
             // clause size can't be reduced.
-            s.attach_clause(c);
             return true;
         }
         // clause can be reduced 
@@ -189,18 +187,17 @@ namespace sat {
             TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";);
             s.assign(c[0], justification());
             s.propagate_core(false); 
-            s.del_clause(c);
+            scoped_d.del_clause();
             SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size());
             return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
         case 2:
             SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
             s.mk_bin_clause(c[0], c[1], false);
-            s.del_clause(c);
+            scoped_d.del_clause();
             SASSERT(s.m_qhead == s.m_trail.size());
             return false;
         default:
             c.shrink(new_sz);
-            s.attach_clause(c);
             SASSERT(s.m_qhead == s.m_trail.size());
             return true;
         }
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 6a7ca6280..b7f83df6c 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -94,7 +94,7 @@ namespace sat {
                 continue;
             }
             if (!c.frozen())
-                m_solver.dettach_clause(c);
+                m_solver.detach_clause(c);
             // apply substitution
             for (i = 0; i < sz; i++) {
                 SASSERT(!m_solver.was_eliminated(c[i].var()));
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 57cdc2fb4..a66f82486 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -462,25 +462,25 @@ namespace sat {
             return simplify_clause_core<false>(num_lits, lits);
     }
 
-    void solver::dettach_bin_clause(literal l1, literal l2, bool learned) {
+    void solver::detach_bin_clause(literal l1, literal l2, bool learned) {
         get_wlist(~l1).erase(watched(l2, learned));
         get_wlist(~l2).erase(watched(l1, learned));
     }
 
-    void solver::dettach_clause(clause & c) {
+    void solver::detach_clause(clause & c) {
         if (c.size() == 3)
-            dettach_ter_clause(c);
+            detach_ter_clause(c);
         else
-            dettach_nary_clause(c);
+            detach_nary_clause(c);
     }
 
-    void solver::dettach_nary_clause(clause & c) {
+    void solver::detach_nary_clause(clause & c) {
         clause_offset cls_off = get_offset(c);
         erase_clause_watch(get_wlist(~c[0]), cls_off);
         erase_clause_watch(get_wlist(~c[1]), cls_off);
     }
 
-    void solver::dettach_ter_clause(clause & c) {
+    void solver::detach_ter_clause(clause & c) {
         erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
         erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
         erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]);
@@ -1493,7 +1493,7 @@ namespace sat {
         for (unsigned i = new_sz; i < sz; i++) {
             clause & c = *(m_learned[i]);
             if (can_delete(c)) {
-                dettach_clause(c);
+                detach_clause(c);
                 del_clause(c);
             }
             else {
@@ -1551,7 +1551,7 @@ namespace sat {
                     else {
                         c.inc_inact_rounds();
                         if (c.inact_rounds() > m_config.m_gc_k) {
-                            dettach_clause(c);
+                            detach_clause(c);
                             del_clause(c);
                             m_stats.m_gc_clause++;
                             deleted++;
@@ -1562,7 +1562,7 @@ namespace sat {
                     if (psm(c) > static_cast<unsigned>(c.size() * m_min_d_tk)) {
                         // move to frozen;
                         TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";);
-                        dettach_clause(c);
+                        detach_clause(c);
                         c.reset_inact_rounds();
                         c.freeze();
                         m_num_frozen++;
@@ -2595,7 +2595,7 @@ namespace sat {
             }
             else {
                 clause & c = *(cw.get_clause());
-                dettach_clause(c);
+                detach_clause(c);
                 attach_clause(c, reinit);
                 if (scope_lvl() > 0 && reinit) {
                     // clause propagated literal, must keep it in the reinit stack.
@@ -2628,7 +2628,7 @@ namespace sat {
         for (unsigned i = 0; i < clauses.size(); ++i) {
             clause & c = *(clauses[i]);
             if (c.contains(lit)) {
-                dettach_clause(c);
+                detach_clause(c);
                 del_clause(c);
             }
             else {
@@ -2646,7 +2646,7 @@ namespace sat {
             literal l1 = m_user_bin_clauses[i].first;
             literal l2 = m_user_bin_clauses[i].second;
             if (nlit == l1 || nlit == l2) {
-                dettach_bin_clause(l1, l2, learned);
+                detach_bin_clause(l1, l2, learned);
             }
         }
     }
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index f910e374f..6c91565aa 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -195,15 +195,34 @@ namespace sat {
         bool attach_nary_clause(clause & c);
         void attach_clause(clause & c, bool & reinit);
         void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
+        class scoped_detach {
+            solver& s;
+            clause& c;
+            bool m_deleted;
+        public:
+            scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
+                s.detach_clause(c);
+            }            
+            ~scoped_detach() {
+                if (!m_deleted) s.attach_clause(c);
+            }
+
+            void del_clause() {
+                if (!m_deleted) {
+                    s.del_clause(c);
+                    m_deleted = true;
+                }
+            }
+        };
         unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;
         unsigned select_learned_watch_lit(clause const & cls) const;
         bool simplify_clause(unsigned & num_lits, literal * lits) const;
         template<bool lvl0>
         bool simplify_clause_core(unsigned & num_lits, literal * lits) const;
-        void dettach_bin_clause(literal l1, literal l2, bool learned);
-        void dettach_clause(clause & c);
-        void dettach_nary_clause(clause & c);
-        void dettach_ter_clause(clause & c);
+        void detach_bin_clause(literal l1, literal l2, bool learned);
+        void detach_clause(clause & c);
+        void detach_nary_clause(clause & c);
+        void detach_ter_clause(clause & c);
         void push_reinit_stack(clause & c);
 
         // -----------------------
diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp
index aee84c1f0..60c85b660 100644
--- a/src/util/small_object_allocator.cpp
+++ b/src/util/small_object_allocator.cpp
@@ -70,6 +70,7 @@ void small_object_allocator::reset() {
 
 void small_object_allocator::deallocate(size_t size, void * p) {
     if (size == 0) return;
+
 #if defined(Z3DEBUG) && !defined(_WINDOWS)
     // Valgrind friendly
     memory::deallocate(p);
@@ -93,6 +94,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
 
 void * small_object_allocator::allocate(size_t size) {
     if (size == 0) return 0;
+
 #if defined(Z3DEBUG) && !defined(_WINDOWS)
     // Valgrind friendly
     return memory::allocate(size);