[YICES-HELP] Question for (max-sat) result

[Eunkyoung Jee]

Hello,

I have a question about max-sat result.

 

My input file has three input variables:

(define p::(subrange 0 30000))

(define tl::bool)

(define tc:(subrange 0 20))

When I executed (max-sat) about 13 assertions, I got a model ((=tl true),
(=p 0), (=tc 0)) satisfying 7 assertions among total 13. Unsatisfied
assertion ids were 1 7 8 9 11 12.

 

To validate the result, I executed (max-sat) again about the same 13
assertions with the generated model, 

i.e., (define p::int 0) (define tl::bool true) (define tc::int 0) instead of
(define p::(subrange 0 30000)) (define tl::bool) (define tc:(subrange 0
20)).

In this case, unsatisfied assertion ids were 5 6 7 8 10 11 12.

 

I could not understand why two unsatisfied assertion ids were different.

I checked the generated model (true, 0, 0) for (tl, p, tc) satisfied 1 2 3 4
9 13 assertions.

Can you help me to understand why the first execution reported "unsatisfied
assertion ids: 1 7 8 9 11 12" even though the generated model satisfied 1
and 9 assertions?

 

Best regards,

Eunkyoung Jee

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/yices-help/attachments/20090419/db7559f2/attachment.html