Experiments on the feasibility of using a floating-point simplex in an SMT solver

SMT solvers use simplex-based decision procedures to solve decision problems whose formulas are quantifier-free and atoms are linear constraints over the rationals. State-of-art SMT solvers use rational (exact) simplex implementations, which have shown good performance for typical software, hardware or protocol verification problems over the years.Yet, most other scientific and technical fields use (inexact) floating-point computations, which are deemed far more efficient than exact ones.It is therefore tempting to use a floating-point simplex implementation inside an SMT solver, though special precautions must be taken to avoid unsoundness.In this work, we describe experimental results, over common benchmarks (SMT-LIB) of the integration of a mature floating-point implementation of the simplex algorithm (GLPK) into an existing SMT solver (OpenSMT).We investigate whether commonly cited reasons for and against the use of floating-point truly apply to real cases from verification problems.