How to write 2 power n i.e. 2^n in Z3?

Question

I am using this link to compile and see the result (http://rise4fun.com/Z3)

I just want to write 2^n say 2^100 in Z3.

Please help me how to write?

Answer 1

Like so: (^ 2 n), see example.

Note that Z3 will often give up on non-linear arithmetic (as is the case in the example). See also: How does Z3 handle non-linear integer arithmetic? and Z3 support for nonlinear arithmetic.