Institute for Computer Languages
Compilers and Languages Group
Bound propagation tool is implemented using the infrastructure of Vampire. It's aim is to solve LRA problems using the algorithm proposed by Konstantin Korovin and Andrei Voronkov.[1]
The tool takes as input problems written in either SMT-LIB 1.2 syntax or MIPLIB (mps files).
See the examples to try Bound Propagation using Gorilla.
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.
[1] Bound propagation is based on the technique presented here for solving systems of linear inequalities.