You are probably using version 4.3.0 on Linux or OSX. Version 4.3.0 has a configuration problem on these platforms. If that is the case, I suggest you download version 4.3.1. Version 4.3.1 will prove both queries on Linux and OSX. In version 4.3.0 auto-configuration is not enabled by default on Linux and OSX. Thus, Z3 will always use a general purpose solver that is not complete for nonlinear arithmetic, nor has support for the power operator. When auto-configuration is enabled, Z3 detects that these two problems are in the nonlinear real arithmetic fragment, and switches to the nlsat solver.
BTW, to manually enable auto-configuration on version 4.3.0, you may use the command z3.set_option(auto_config=True)
.