From 5352a5fb85b7ade9633f9b16907e9ea04c5d5aa8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 10 May 2019 13:41:10 -0700 Subject: [PATCH] fix the factorization sign to be equal to the monomial sign Signed-off-by: Lev Nachmanson --- src/util/lp/int_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index 3b46b423b..20c398f49 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -269,7 +269,7 @@ lia_move int_solver::find_cube() { m_lar_solver->pop(); m_lar_solver->round_to_integer_solution(); m_lar_solver->set_status(lp_status::FEASIBLE); - lp_assert(is_feasible()); + lp_assert(settings().get_cancel_flag() || is_feasible()); TRACE("cube", tout << "success";); settings().st().m_cube_success++; TRACE("cube", tout << "sat with cube\n";);