I guess many have heard of the existential theory of the reals:

https://en.wikipedia.org/wiki/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?

Preferably, non-commercial.

Apparently SAGE has only a "use at your own risk" version.

Also I am not interested in numerical solutions.

best Till

International Conference on Automated Deduction. Springer Berlin Heidelberg, 2013. Journal link $\endgroup$