diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp
index f15c241f2..bd7b0d26c 100644
--- a/src/sat/sat_ddfw.cpp
+++ b/src/sat/sat_ddfw.cpp
@@ -317,7 +317,7 @@ namespace sat {
             // cls becomes false: flip any variable in clause to receive reward w
             switch (ci.m_num_trues) {
             case 0: {
-                m_unsat.insert(cls_idx);
+                m_unsat.insert_fresh(cls_idx);
                 clause const& c = get_clause(cls_idx);
                 for (literal l : c) {
                     inc_reward(l, w);
@@ -406,7 +406,7 @@ namespace sat {
                     inc_reward(lit, ci.m_weight);
                     inc_make(lit);
                 }
-                m_unsat.insert(i);
+                m_unsat.insert_fresh(i);
                 break;
             case 1:
                 dec_reward(to_literal(ci.m_trues), ci.m_weight);
diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h
index 988365285..ff86e9b8c 100644
--- a/src/sat/sat_ddfw.h
+++ b/src/sat/sat_ddfw.h
@@ -178,7 +178,7 @@ namespace sat {
 
         inline void inc_make(literal lit) { 
             bool_var v = lit.var(); 
-            if (make_count(v)++ == 0) m_unsat_vars.insert(v); 
+            if (make_count(v)++ == 0) m_unsat_vars.insert_fresh(v); 
         }
 
         inline void dec_make(literal lit) { 
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 2fa7ed040..2f3fc91b2 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -990,7 +990,7 @@ namespace sat {
         m_rating.push_back(0);
         m_vprefix.push_back(prefix());
         if (!m_s.was_eliminated(v)) 
-            m_freevars.insert(v);
+            m_freevars.insert_fresh(v);
     }
 
     void lookahead::init(bool learned) {
@@ -1096,7 +1096,7 @@ namespace sat {
             literal l = m_trail[i];
             set_undef(l);
             TRACE("sat", tout << "inserting free var v" << l.var() << "\n";);
-            m_freevars.insert(l.var());
+            m_freevars.insert_fresh(l.var());
         }
             
         m_num_tc1 = m_num_tc1_lim.back();
diff --git a/src/sat/sat_prob.cpp b/src/sat/sat_prob.cpp
index 46a098ba8..824ec4fc6 100644
--- a/src/sat/sat_prob.cpp
+++ b/src/sat/sat_prob.cpp
@@ -80,7 +80,7 @@ namespace sat {
             ci.del(lit);
             switch (ci.m_num_trues) {
             case 0:
-                m_unsat.insert(cls_idx);
+                m_unsat.insert_fresh(cls_idx);
                 dec_break(lit);
                 break;
             case 1:
@@ -184,7 +184,7 @@ namespace sat {
             }
             switch (ci.m_num_trues) {
             case 0:
-                m_unsat.insert(i);
+                m_unsat.insert_fresh(i);
                 break;
             case 1:
                 inc_break(to_literal(ci.m_trues));
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index 6e64cc7ae..b04c67a07 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -318,7 +318,7 @@ public:
         m_size(0)
     {}
 
-    void insert(unsigned x) {
+    void insert_fresh(unsigned x) {
         SASSERT(!contains(x));
         m_index.reserve(x + 1, UINT_MAX);
         m_elems.reserve(m_size + 1);
@@ -327,6 +327,11 @@ public:
         m_size++;
         SASSERT(contains(x));
     }
+
+    void insert(unsigned x) {
+        if (!contains(x))
+            insert_fresh(x);
+    }
     
     void remove(unsigned x) {
         SASSERT(contains(x));