Computation never terminates

[layderv]

Is it possible that the program below is in an infinite loop?
I've been running it for a lot of time (more than 14h) on a machine with a great amount of resources; the memory usage is extremely small and it uses all the available CPU.

from __future__ import division, print_function
from z3 import *

x0, x1, x2 = Reals('x0 x1 x2')

f = [Not(Implies(Or(x0 != 0, x1 != 0, x2 != 0),
             And(849088067447341/100000000000000000*x2**2 +
                 78074952370137/5000000000000000*x0**2 +
                 193396168334883/200000000000000*x1**2 +
                 17826574354169/1000000000000000*x0*x1 >
                 0,
                 -113348143155153/10000000000*x0**2 +
                 -112697632034153/100000000*x1**2 +
                 -282624397413479/10000000000*x2**2 +
                 89512726293947/2500000000*x0*x2 +
                 225674416915119/1000000000*x0*x1 +
                 -356193564152069/1000000000*x1*x2 <
                 0))),
 0 + x0**3 + x1**3 + x2**3 == 1]

s = Solver()
s.add(f)

if s.check() == sat:
	print(s.model())
else:
	print("unsat")

I've run the same code with Q(p, q) instead of p/q as above.
I can provide some very similar examples, if needed.

[NikolajBjorner]

it spends 99% of time in root isolation and the bulk of that time in big-num arithmetic.
This is somewhat expected when you use large coefficients.