diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 63a17e0ea..ba3ed2e3a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -283,7 +283,7 @@ namespace sat {
         m_stats.m_mk_var++;
         bool_var v = m_justification.size();
         
-        if (!m_free_vars.empty() && false) {
+        if (!m_free_vars.empty()) {
             v = m_free_vars.back();
             m_free_vars.pop_back();
             m_active_vars.push_back(v);