Reading the above, I wonder if the people who are writing the linear equality/inequality parts of SAT solvers for program proof know that. Internally, numerical equalities and inequalities become rows in a sparse matrix. The columns represent program variables. Solution is done with rational arithmetic. The original Oppen-Nelson prover of the 1970s solved those with a Gauss-Jordan approach, and most follow-on work through at least the 1990s was basically the same machinery.