diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 5a789a610..5148dedc0 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -22,7 +22,7 @@
 #include "math/lp/lar_solver.h"
 #include "math/lp/lp_utils.h"
 
-#define SMALL_CUTS 0
+#define SMALL_CUTS 1
 namespace lp {
 
 class gomory::imp {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 432f7e11d..234b58b42 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2045,7 +2045,15 @@ public:
 
         case lp::lia_move::branch: {
             TRACE("arith", tout << "branch\n";);
-            app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
+            app_ref b(m);
+            bool u = m_lia->is_upper();
+            auto const & k = m_lia->get_offset();
+            if (0 == ctx().get_random_value() % 2) {
+                b = mk_bound(m_lia->get_term(), k, !u);
+            }
+            else {
+                b = mk_bound(m_lia->get_term(), u ? k - 1 : k + 1, u);
+            }
             if (m.has_trace_stream()) {
                 app_ref body(m);
                 body = m.mk_or(b, m.mk_not(b));