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

fix the factorization sign to be equal to the monomial sign

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-10 13:41:10 -07:00
parent 375027d195
commit 5352a5fb85
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/int_solver.cpp
View file

@ -269,7 +269,7 @@ lia_move int_solver::find_cube() {
m_lar_solver->pop(); m_lar_solver->pop();
m_lar_solver->round_to_integer_solution(); m_lar_solver->round_to_integer_solution();
m_lar_solver->set_status(lp_status::FEASIBLE); m_lar_solver->set_status(lp_status::FEASIBLE);
lp_assert(is_feasible()); lp_assert(settings().get_cancel_flag() || is_feasible());
TRACE("cube", tout << "success";); TRACE("cube", tout << "success";);
settings().st().m_cube_success++; settings().st().m_cube_success++;
TRACE("cube", tout << "sat with cube\n";); TRACE("cube", tout << "sat with cube\n";);