diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 940b286d9..a4c00ced4 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1426,6 +1426,7 @@ namespace polysat {
 
     void solver::push() {
         LOG_H3("Push user scope");
+        propagate();
         push_level();
         m_base_levels.push_back(m_level);
         m_base_index.push_back(m_search.size());