diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 5a2b4457b0..82caa8fa12 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -270,6 +270,22 @@ namespace opt {
                     // to_int, prevent the LP from seeing the full feasible region.
                     if (m_lower[obj_index].is_finite() && m_lower[obj_index] > obj)
                         bound = m_s->mk_ge(obj_index, m_lower[obj_index]);
+                    if (bound == last_bound && obj.get_infinitesimal().is_pos()) {
+                        // The objective sits infinitesimally above the strict
+                        // bound asserted in the previous round: r + k*delta with
+                        // k > 0.  Such a value is not a proven optimum, it only
+                        // says the arithmetic solver could not move off the
+                        // bound it was just given.  Its blocker is built from
+                        // the rational part alone, so it collapses onto the
+                        // previous blocker and the search would stop here and
+                        // report the stalled value as the optimum.  Force a
+                        // strictly larger rational step instead; if the step is
+                        // infeasible the loop terminates through the l_false
+                        // branch below with the best proven bound.
+                        m_s->push();
+                        ++num_scopes;
+                        bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));
+                    }
                     if (bound == last_bound)
                         break;
                 }
diff --git a/src/test/api.cpp b/src/test/api.cpp
index 7b1bf1303f..e1d337cf9a 100644
--- a/src/test/api.cpp
+++ b/src/test/api.cpp
@@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/util.h"
 #include "util/trace.h"
 #include <map>
+#include <string>
 #include "util/trace.h"
 
 void test_apps() {
@@ -423,8 +424,39 @@ void test_scaled_minimize_unbounded() {
     std::cout << "scaled minimize unbounded test done" << std::endl;
 }
 
+// Sets a global parameter for the duration of the scope and restores the
+// previous value on exit.
+class scoped_global_param {
+    std::string m_id;
+    std::string m_old;
+    bool m_had = false;
+public:
+    scoped_global_param(char const* id, char const* value) : m_id(id) {
+        Z3_string v = nullptr;
+        m_had = Z3_global_param_get(id, &v);
+        if (m_had && v)
+            m_old = v;
+        Z3_global_param_set(id, value);
+    }
+    ~scoped_global_param() {
+        if (m_had)
+            Z3_global_param_set(m_id.c_str(), m_old.c_str());
+    }
+};
+
 void tst_scaled_min() {
     test_scaled_minimize_unbounded();
+
+    // The same objectives must stay unbounded when the integer cut/cube
+    // heuristics run less often.  At these periods the LRA optimizer stalls at
+    // a delta-rational value r + k*delta, whose blocker degenerates to the same
+    // 'objective > r' literal in consecutive rounds; the search used to stop
+    // there and report a finite value for an unbounded objective.
+    for (unsigned period : {16u, 32u, 64u, 128u}) {
+        std::cout << "lp.int_hammer_period=" << period << std::endl;
+        scoped_global_param _period("lp.int_hammer_period", std::to_string(period).c_str());
+        test_scaled_minimize_unbounded();
+    }
 }
 
 void tst_max_rev() {