how to deal with this expression?

Reply

xyz031702 Posted: 09-28-2009 5:45 AM

rated by 0 users

Dear All

       I got a problem when dealing with the following Z3 expression:

(benchmark tst  :extrafuns ((V1 Real)(flag Real)) :formula (not (=  (* V1 flag) flag)))

The output result is a bit strange:

 potential model:    V1--->0  ,  flag---->0

So does this mean Z3 cannot find a possible solution for it ? Is there any other similar cases?  Or what is a general expression for these similar cases?

Expecting for replies ,

Thanks and  best regards,

Ding Sun

Reply

xyz031702 replied on 09-28-2009 5:47 AM

rated by 0 users

Or say is there a list of cases which Z3 cannot prove?