From cb272bd7a876c4eabe7f9d31a7b07ac61e1df679 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Aug 2022 03:57:28 -0700
Subject: [PATCH] fix missing removal of x in solve_mod

---
 src/math/simplex/model_based_opt.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 2f0058bd336..62a6b5129fe 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1256,6 +1256,8 @@ namespace opt {
 
         for (unsigned ri : mod_rows) {
             rational a = get_coefficient(ri, x);
+            replace_var(ri, x, rational::zero());
+
             // add w = b mod K
             vector<var> coeffs = m_rows[ri].m_vars;
             rational coeff = m_rows[ri].m_coeff;