mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

fix missing removal of x in solve_mod

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-08-17 03:57:28 -07:00
parent b3f4d3fdc7
commit cb272bd7a8
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/simplex/model_based_opt.cpp
View file

@ -1256,6 +1256,8 @@ namespace opt {
for (unsigned ri : mod_rows) { for (unsigned ri : mod_rows) {
rational a = get_coefficient(ri, x); rational a = get_coefficient(ri, x);
replace_var(ri, x, rational::zero());
// add w = b mod K // add w = b mod K
vector<var> coeffs = m_rows[ri].m_vars; vector<var> coeffs = m_rows[ri].m_vars;
rational coeff = m_rows[ri].m_coeff; rational coeff = m_rows[ri].m_coeff;