So far, the development and implementation of decision procedures for
linear arithmetic in the context of Satisfiability Modulo Theories
(SMT) has been mostly independent from the technology used in
Operations Research (OR). This situation has been justified given that
the requirements for linear SMT solvers are different from
those of OR linear programming tools for optimization: they have to
handle disequalities and strict inequalities, and in order to
guarantee correctness, infinite precision arithmetic instead of
floating-point arithmetic must be used. In this talk we will describe
ongoing experiments in which we have used the linear programming tool CPLEX
as a linear SMT solver.