Exponential example for simplex used in SMT solvers The original simplex algorithm requires an exponential number of pivot operations in the worst case, e.g., if run on the Klee-Minty example [3,4].

What about the simplex algorithm used in SMT solvers [1,2]? Could you provide an example where it requires exponential time?  

The algorithm I have in mind is by Bruno Dutertre and Leonardo de Moura in [1,2], and is presumably used in all modern SMT solvers. The algorithm introduces one slack variable per constraint, the slack variables have lower and upper bounds; and the problem is that of feasibility instead of optimization.

I tried to modify the Klee-Minty example [3,4], but failed so far.
Kroening &amp; Strichman contains this question as an exercise, so you can also hint instead of answering.




Integrating Simplex with DPLL(T) by Bruno Dutertre and Leonardo de Moura:
Decision Procedures: an Algorithmic Point of View by Daniel Kroening and Ofer Strichman
Klee-Minty Polytope Shows Exponential Time Complexity of Simplex Method
Picture of the Klee-Minty cube:
Here, you can find hard examples for DPLL. 
http://www.ioc.ee/~tarmo/tday-torve/itsykson-slides.pdf

For instance, it can be very slow for Tseitin formulas and for some unsatisfaisable formulas (it will try many solutions). 

I hope it will give you some hints :)