mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

fix the build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-05-08 17:28:34 -07:00
parent 7da06df64f
commit 0108a86490
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/lar_solver.cpp
View file

@ -395,11 +395,11 @@ namespace lp {
mpq lar_solver::from_model_in_impq_to_mpq(const impq& v) const { return v.x + m_imp->m_delta * v.y; } mpq lar_solver::from_model_in_impq_to_mpq(const impq& v) const { return v.x + m_imp->m_delta * v.y; }
inline const impq& lar_solver::get_upper_bound(lpvar j) const { const impq& lar_solver::get_upper_bound(lpvar j) const {
return get_core_solver().m_r_solver.m_upper_bounds[j]; return get_core_solver().m_r_solver.m_upper_bounds[j];
} }
inline const impq& lar_solver::get_lower_bound(lpvar j) const { const impq& lar_solver::get_lower_bound(lpvar j) const {
return get_core_solver().m_r_solver.m_lower_bounds[j]; return get_core_solver().m_r_solver.m_lower_bounds[j];
} }