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

[Cesare Tinelli]

Daniela,

Since your questions below are about Z3, a better forum for them is probably one of the Z3 mailing lists (at http://research.microsoft.com/en-us/um/redmond/projects/z3/mail.html).

Best,


Cesare


On 26 Nov 2010, at 09:20, Daniela da Cruz wrote:

> 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
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib