E. M. Beale, An alternative method for linear programming, Mathematical Proceedings of the Cambridge Philosophical Society, vol.50, issue.04, pp.513-523, 1954.
DOI : 10.1017/S0305004100029650

N. Bjørner, Integrating decision procedures for temporal verification, 1999.

F. Bobot, S. Conchon, E. Contejean, M. Iguernelala, A. Mahboubi et al., A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic, IJCAR 2012, pp.67-81, 2012.
DOI : 10.1007/978-3-642-31365-3_8

URL : https://hal.archives-ouvertes.fr/hal-00687640

S. Boyd and L. Vandenberghe, Convex Optimization, 2004.

M. Bromberger, T. Sturm, and C. Weidenbach, Linear Integer Arithmetic Revisited, LNCS, vol.9195, pp.25-623, 2015.
DOI : 10.1007/978-3-319-21401-6_42

URL : https://hal.archives-ouvertes.fr/hal-01239394

M. Bromberger and C. Weidenbach, Computing a complete basis for equalities implied by a system of LRA constraints, SMT 2016, pp.15-30, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01403214

M. Bromberger and C. Weidenbach, Fast Cube Tests for LIA Constraint Solving, IJCAR 2016, 2016.
DOI : 10.1145/322276.322287

URL : https://hal.archives-ouvertes.fr/hal-01403200

R. Bruttomesso, A. Cimatti, A. Franzen, A. Griggio, and R. Sebastiani, Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis, AMAI, vol.55, issue.1, pp.63-99, 2009.

I. Dillig, T. Dillig, and A. Aiken, Cuts from proofs: A complete and practical technique for solving linear inequalities over integers, CAV, LNCS, pp.233-247, 2009.

A. Dolzmann, T. Sturm, and V. Weispfenning, Real Quantifier Elimination in Practice, Algorithmic Algebra and Number Theory, pp.221-247, 1999.
DOI : 10.1007/978-3-642-59932-3_11

B. Dutertre, Yices??2.2, CAV 2014, 2014.
DOI : 10.1007/978-3-319-08867-9_49

B. Dutertre and L. De-moura, A fast linear-arithmetic solver for DPLL(T) Extended version: Integrating simplex with DPLL(T), CAV, pp.81-94, 2006.

G. Faure, R. Nieuwenhuis, A. Oliveras, and E. Rodríguez-carbonell, SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers, SAT 2008, pp.77-90, 2008.
DOI : 10.1007/978-3-540-79719-7_8

URL : https://hal.archives-ouvertes.fr/inria-00358813

A. Griggio, A practical approach to satisfiability modulo linear integer arithmetic, JSAT, vol.8, issue.12, pp.1-27, 2012.

F. S. Hillier, Efficient Heuristic Procedures for Integer Linear Programming with an Interior, Operations Research, vol.17, issue.4, pp.600-637, 1969.
DOI : 10.1287/opre.17.4.600

D. Jovanovi´cjovanovi´c and L. De-moura, Cutting to the Chase, Journal of Automated Reasoning, vol.28, issue.4, pp.79-108, 2013.
DOI : 10.1145/125826.125848

R. Kannan and L. Lovász, Covering minima and lattice point free convex bodies, FSTTCS, pp.193-213, 1986.

N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica, vol.244, issue.S, pp.373-396, 1984.
DOI : 10.1007/BF02579150

C. E. Lemke, The dual method of solving the linear programming problem, Naval Research Logistics Quarterly, vol.1, issue.1, pp.36-47, 1954.
DOI : 10.1002/nav.3800010107

R. Loos and V. Weispfenning, Applying Linear Quantifier Elimination, The Computer Journal, vol.36, issue.5, pp.450-462, 1993.
DOI : 10.1093/comjnl/36.5.450

L. De-moura and N. Bjørner, Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.4963, pp.337-340, 2008.

C. H. Papadimitriou, On the complexity of integer programming, Journal of the ACM, vol.28, issue.4, pp.765-768, 1981.
DOI : 10.1145/322276.322287

W. Pugh, The Omega test: a fast and practical integer programming algorithm for dependence analysis, Proceedings of the 1991 ACM/IEEE conference on Supercomputing , Supercomputing '91, pp.4-13, 1991.
DOI : 10.1145/125826.125848

P. Refalo, Approaches to the incremental detection of implicit equalities with the revised simplex method, PLILP 1998, pp.481-496, 1998.
DOI : 10.1007/BFb0056634

H. Rueß and N. Shankar, Solving linear arithmetic constraints, Tech. rep., SRI International, 2004.

A. Schrijver, Theory of Linear and Integer Programming, 1986.

T. Sturm, Real quadratic quantifier elimination in risa/asir, 1996.

J. Telgen, Identifying Redundant Constraints and Implicit Equalities in Systems of Linear Constraints, Management Science, vol.29, issue.10, pp.1209-1222, 1983.
DOI : 10.1287/mnsc.29.10.1209

P. Van-hentenryck and T. Graf, Standard forms for rational linear arithmetic in constraint logic programming, Annals of Mathematics and Artificial Intelligence, vol.5, issue.2-4, pp.303-319, 1992.
DOI : 10.2140/pjm.1955.5.183