[SMT-LIB] Non nested arithmetic pattern causing formula to be not valid

[Daniela da Cruz]

Hi.

I have this SMT code:

:extrafuns (( x Int)  ( result Int))

:formula (not (implies (>= x 0 ) (exists (_v1  Int) (and (>= _v1 0) (= x (-
_v1 100 ) ) ) ) ) )

And I got this Warning in Z3 (version 2.4):

*WARNING: using non nested arith. pattern (quantifier id: k!6), the weight
was in
creased to 10 (this value can be modified using
PI_NON_NESTED_ARITH_WEIGHT=<val>
).*


This causes the formula to be "sat" but is "unsat". In previous version of
Z3 I got no warnings neither and got too "unsat".

Do you have any idea why this is happening? I made some tests and it seems
to be caused by the "and" operator.
However, I don't know how to solve it.

thanks
daniela