exponent constraint is unknown in Z3 C API?

Question

I want to get the solution from Z3 C API for the constraint followed:

   2^x < a < 2^(x+1)

expression for 2^x is :

    t_x=Z3_mk_power(ctx,two,x), two is the expression of "2";

    2^(x+1) is similar,

"a" is a int const ,which value is 10:

   a=Z3_mk_int(ctx,10);

the constraints are:

   c1=Z3_mk_lt(ctx,t_x,a);

   c2=Z3_mk_lt(ctx,a,t_x_plus_one);

then I get the model is "unknown", Z3 C API cannot get a model like this?

Answer 1

From the description it's not clear which solving method Z3 employs in the end, but in general non-linear integer arithmetic is undecidable and Z3 can only handle simple cases of exponentials. See also Leo's answers to similar questions:

How does Z3 handle non-linear integer arithmetic?

Z3 supports for nonlinear arithmetics