What do Z3 and other SMT solvers do if you ask them about undecidable questions? Do they potentially run forever?