Q. F. Smt-comp-;-results-for and . Lia, , 2018.

Q. F. Smt-comp-;-results-for and . Lra, , 2018.

S. The and . Workbench,

C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanovi? et al., CAV, vol.6806, 2011.

C. Barrett, P. Fontaine, and C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016.

C. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Splitting on demand in SAT modulo theories, Logic for Programming, vol.4246, pp.512-526, 2006.

M. Bromberger, A reduction from unbounded linear mixed arithmetic problems into bounded problems, Automated Reasoning, vol.10900, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01942228

M. Bromberger, M. Fleury, S. Schwarz, and C. Weidenbach, SPASS-SATT -A CDCL(LA) solver, editor, Automated Deduction -CADE 27 -27th International Conference on Automated Deduction, vol.11716, pp.111-122, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02405524

M. Bromberger, T. Sturm, and C. Weidenbach, Linear integer arithmetic revisited, LNCS, vol.9195, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239394

M. Bromberger and C. Weidenbach, Fast cube tests for LIA constraint solving, IJCAR 2016, vol.9706, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01403200

M. Bromberger and C. Weidenbach, New Techniques for Linear Arithmetic: Cubes and Equalities, Formal Methods in System Design, vol.51, issue.3, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01656397

J. R. Burch, Techniques for verifying superscalar microprocessors, DAC, pp.552-557, 1996.

A. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani, The MathSAT5 SMT Solver, TACAS, vol.7795, 2013.

M. Codish, Y. Fekete, C. Fuhs, J. Giesl, and J. Waldmann, Exotic semi-ring constraints, SMT@IJCAR, vol.20, pp.88-97, 2012.

L. M. De-moura and N. Bjørner, Z3: an efficient SMT solver, LNCS, vol.4963, pp.337-340, 2008.

. Springer, , 2008.

I. Dillig, T. Dillig, and A. Aiken, Cuts from proofs: A complete and practical technique for solving linear inequalities over integers, CAV, vol.5643, 2009.

B. Dutertre, Yices 2.2, CAV 2014, vol.8559, 2014.

B. Dutertre and L. M. De-moura, Extended version: Integrating simplex with DPLL(T), CSL, SRI INTERNATIONAL, vol.4144, 2006.

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, DPLL(T): fast decision procedures, CAV, 2004.

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

P. L. Hammer and S. Rudeanu, Boolean methods in operations research and related areas, 2012.

W. Hart, F. Johansson, and S. Pancratz, FLINT: Fast Library for Number Theory, 2013.

D. Jovanovi? and L. M. De-moura, Cutting to the chase solving linear integer arithmetic, CADE, vol.6803, pp.338-353, 2011.

R. M. Karp, Reducibility among combinatorial problems, Complexity of Computer Computations, The IBM Research Symposia Series, pp.85-103, 1972.

H. Kim, F. Somenzi, and H. Jin, Efficient term-ite conversion for satisfiability modulo theories, SAT, vol.5584, pp.195-208, 2009.

R. Nieuwenhuis, The IntSat method for integer linear programming, Principles and Practice of Constraint Programming, vol.8656, 2014.

R. Nieuwenhuis and A. Oliveras, DPLL(T) with exhaustive theory propagation and its application to difference logic, CAV, pp.321-334, 2005.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T ), J. ACM, vol.53, issue.6, pp.937-977, 2006.

A. Nonnengart and C. Weidenbach, Computing small clause normal forms, Handbook of Automated Reasoning, vol.1, 2001.

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

R. Sebastiani, Lazy satisability modulo theories, JSAT, vol.3, issue.3-4, pp.141-224, 2007.

G. Tseitin, On the complexity of derivations in propositional calculus, Automation of Reasoning: Classical Papers on Computational Logic, vol.2, pp.466-483, 1968.

C. Weidenbach, D. Dimova, A. Fietzke, M. Suda, and P. Wischnewski, SPASS version 3.5, 22nd International Conference on Automated Deduction, vol.5663, pp.140-145, 2009.