To test if an instruction is useful, we need to evaluate the
preconditions to know if there is an integer solution to the
predicate. For this purpose, we use the linear algebra library
that provides support for vector and matrix operations, feasibility
tests with simplex of FOURIER-MOTZKIN, etc.
In this example, we use in
statement_weakly_feasible_p() that calls the function
sc_empty_p() to know if there is a solution to the system of