diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 4bde7b90b..5dc768206 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -2707,6 +2707,8 @@ namespace sls {
     void arith_base<num_t>::update_unchecked(var_t v, num_t const& new_value) {
         auto& vi = m_vars[v];
         auto old_value = value(v);
+        if (old_value == new_value)
+            return;
         IF_VERBOSE(5, verbose_stream() << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n");
         TRACE(arith, tout << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n");
         vi.set_value(new_value);