Well, you must continue with the strengthening until an integer solution is found, or it turns out that there is no solution with the strengthened constraints. In the first case, it terminates with a solution, in the second case, you backtrack and tray with floor. It that should also fail, there is no solution at all.