diff --git a/src/math/polysat/fixed_bits.cpp b/src/math/polysat/fixed_bits.cpp
index 63643dfc4..d697f3312 100644
--- a/src/math/polysat/fixed_bits.cpp
+++ b/src/math/polysat/fixed_bits.cpp
@@ -607,10 +607,13 @@ namespace polysat {
     }
     
     void fixed_bits::push() {
+#if 0
         m_trail_size.push_back(m_trail.size());
+#endif
     }
     
     void fixed_bits::pop(unsigned pop_cnt) {
+#if 0
         SASSERT(!m_consistent); // Why do we backtrack if this is true? We might remove this for (random) restarts
         SASSERT(pop_cnt > 0);
         
@@ -642,6 +645,7 @@ namespace polysat {
             m_trail.resize(prev_cnt);
         else 
             m_trail.resize(last_to_keep);
+#endif
     }
 
 #define COUNT(DOWN, TO_COUNT) \