diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index af07c4482e..31475fc6d4 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -462,12 +462,23 @@ namespace lp {
         column_cell& cs = m_columns[row_el_iv.var()][column_offset];
         unsigned row_offset = cs.offset();
         if (column_offset != column_vals.size() - 1) {
-            auto & cc = column_vals[column_offset] = column_vals.back(); // copy from the tail
+            auto & cc = column_vals[column_offset] = column_vals.back(); // column cells are tiny, a plain copy is optimal
             m_rows[cc.var()][cc.offset()].offset() = column_offset;
         }
     
         if (row_offset != row_vals.size() - 1) {
-            auto & rc = row_vals[row_offset] = row_vals.back(); // copy from the tail
+            row_cell<T> & rc   = row_vals[row_offset];
+            row_cell<T> & tail = row_vals.back();
+            rc.var()    = tail.var();
+            rc.offset() = tail.offset();
+            // Relocating the tail coefficient: a copy allocates a fresh bignum only when the
+            // source (tail) is big, so swap to steal the tail's storage exactly in that case.
+            // When the tail is small the copy never allocates and is cheaper than a swap. See
+            // Z3Prover/bench#3143.
+            if (tail.coeff().is_big())
+                rc.coeff().swap(tail.coeff());
+            else
+                rc.coeff() = tail.coeff();
             m_columns[rc.var()][rc.offset()].offset() = row_offset;
         }