I guess many have heard of the existential theory of the reals:
I have read in various papers that the problem lies in PSPACE. I have frequently some problems that I would like to solve by some of these algorithms. As I am often concerned with small finite instances I don't mind if the computation takes several days. Can someone recommend me a usable implementation?
Apparently SAGE has only a "use at your own risk" version.
Also I am not interested in numerical solutions.