mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 09:12:16 +00:00
Code Activity

more aggressive patching

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-26 14:56:13 -07:00
parent e5503cdc65
commit b84585beeb
5 changed files with 27 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/nla_core.cpp
View file

@ -1392,6 +1392,12 @@ void core::patch_monomials() {
if (m_to_refine.size() == 0)
break;
}
NOT_IMPLEMENTED_YET();
/*
If the tableau is not feasible we need to fix all non-linear
vars that do not satisfy var_breaks_correct_monic()
and find a feasible solution, fix the integral values too.
*/
TRACE("nla_solver", tout << "sz = " << m_to_refine.size() << "\n";);
SASSERT(m_lar_solver.ax_is_correct());
}