Institute for Computer Languages
Compilers and Languages Group
The bound propagation tool is implemented using the infrastructure of the first-order theorem prover Vampire. The goal of bound propagation is to solve linear rational arithmetic (LRA) problems, using the algorithm proposed by Konstantin Korovin and Andrei Voronkov. 
The tool takes as input problems written in either SMT-LIB syntax or MIPLIB (mps files).
See this smtlib problems if you want to test the solver on hard smtlib problems.
See this if you are interested in some examples of miplib problems. Upon request, we provide them also in smtlib format.
 Bound Propagation for Arithmetic Reasoning in Vampire, Ioan Dragan, Konstantin Korovin, Laura Kovacs, Andrei Voronkov (SYNASC 2013) (preprint [pdf])
 Bound propagation is based on the technique presented here for solving systems of linear inequalities.