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 & 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
Picture of the Klee-Minty cube: