Using the $C3$ linear algebra library

 

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 $C3$ 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 dead_statement_filter() statement_weakly_feasible_p() that calls the $C3$ function sc_empty_p() to know if there is a solution to the system of constraints.