diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp
index aad7fae6e..d28a79be6 100644
--- a/src/math/lp/int_cube.cpp
+++ b/src/math/lp/int_cube.cpp
@@ -45,7 +45,11 @@ namespace lp {
             lra.pop();
             lra.move_non_basic_columns_to_bounds();
             // it can happen that we found an integer solution here
-            return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
+            if (!lra.r_basis_has_inf_int()) {
+                lia.settings().stats().m_cube_success_bail_sat++;
+                return lia_move::sat;
+            }
+            return lia_move::undef;
         }
         lra.pop();
         lra.round_to_integer_solution();
diff --git a/src/math/lp/int_cube_lll.cpp b/src/math/lp/int_cube_lll.cpp
index 28e2e988a..e7acec087 100644
--- a/src/math/lp/int_cube_lll.cpp
+++ b/src/math/lp/int_cube_lll.cpp
@@ -429,7 +429,11 @@ namespace lp {
             TRACE(lll_cube, tout << "cannot find a feasible solution\n";);
             lra.pop();
             lra.move_non_basic_columns_to_bounds();
-            return !lra.r_basis_has_inf_int() ? lia_move::sat : lia_move::undef;
+            if (!lra.r_basis_has_inf_int()) {
+                lia.settings().stats().m_lll_cube_success_bail_sat++;
+                return lia_move::sat;
+            }
+            return lia_move::undef;
         }
         save_x_J();
         lra.pop();
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 58c9fb476..cdcf9f87c 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -112,8 +112,10 @@ struct statistics {
     unsigned m_gcd_conflicts = 0;
     unsigned m_cube_calls = 0;
     unsigned m_cube_success = 0;
+    unsigned m_cube_success_bail_sat = 0;
     unsigned m_lll_cube_calls = 0;
     unsigned m_lll_cube_success = 0;
+    unsigned m_lll_cube_success_bail_sat = 0;
     unsigned m_lll_cube_bail_collect = 0;
     unsigned m_lll_cube_bail_build = 0;
     unsigned m_lll_cube_bail_basis = 0;
@@ -160,8 +162,10 @@ struct statistics {
         st.update("arith-gcd-conflict", m_gcd_conflicts);
         st.update("arith-cube-calls", m_cube_calls);
         st.update("arith-cube-success", m_cube_success);
+        st.update("arith-cube-success-bail-sat", m_cube_success_bail_sat);
         st.update("arith-lll-cube-calls", m_lll_cube_calls);
         st.update("arith-lll-cube-success", m_lll_cube_success);
+        st.update("arith-lll-cube-success-bail-sat", m_lll_cube_success_bail_sat);
         st.update("arith-lll-cube-bail-collect", m_lll_cube_bail_collect);
         st.update("arith-lll-cube-bail-build", m_lll_cube_bail_build);
         st.update("arith-lll-cube-bail-basis", m_lll_cube_bail_basis);