x = 1.138539433479309  (x*3)*5 = 17.078092575073242  x*15 = 17.07809066772461
for the constants 2.0 and 3.0 z3 says: unsat (multiplying by 2.0 is exact, so there is no second rounding)
