diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index b45f9ba51..3834fa61b 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1252,6 +1252,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
 
 void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
     lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
+    variable_values.clear();
     mpq delta = mpq(1, 2); // start from 0.5 to have less clashes
     unsigned i;
     unsigned n = m_mpq_lar_core_solver.m_r_x.size();