Does Z3 python handle x ** 2 other than x * x?

Question

It seems that the Z3 Python interface does not like the ** operator, it can deal with x * x, but not with x ** 2, as shown in the example below

>>> x,y = x,y=Reals('x y') >>> z3.prove(Implies(x -6 == 0,x**2 -36 == 0)) failed to prove [x = 6] >>> z3.prove(Implies(x -6 == 0,x*x -36 == 0)) proved 

Answer 1

You are probably using version 4.3.0 for Linux or OSX. Version 4.3.0 has configuration problems on these platforms. If so, I suggest you download version 4.3.1 . Version 4.3.1 will contain both queries on Linux and OSX. In version 4.3.0, auto-tuning is enabled by default on Linux and OSX. Thus, Z3 will always use a general-purpose solver that is not complete for nonlinear arithmetic and does not support the power operator. When autoconfiguration is enabled, Z3 detects that these two problems are in a non-linear real arithmetic fragment, and switches to nlsat solver .

BTW, to manually enable automatic configuration on version 4.3.0, you can use the z3.set_option(auto_config=True) command.