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

change formatting

Browse source
This commit is contained in:
Lev Nachmanson 2025-03-06 14:09:54 -10:00
parent 6cee4ae225
commit 1ac9c558c0
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/dioph_eq.cpp
View file

@ -1528,7 +1528,8 @@ namespace lp {
auto st = lra.find_feasible_solution();
if (st == lp_status::INFEASIBLE) {
lra.get_infeasibility_explanation(m_infeas_explanation);
TRACE("dio", tout << "inf explanation:\n"; lra.print_explanation(tout, m_infeas_explanation);); return lia_move::conflict;
TRACE("dio", tout << "inf explanation:\n"; lra.print_explanation(tout, m_infeas_explanation););
return lia_move::conflict;
}
TRACE("dio", tout << "lra is feasible\n";);
return lia_move::undef;