[YICES-HELP] Using Yices for MaxSMT w/ difference-logic

[Michael D. Moffitt]

Hello,

I'm using Yices to do MaxSMT on a difference-logic instance:

   yices -v 2 < moffittOpt.yices

with this input file:

   http://jeeves.eecs.umich.edu/moffittOpt.yices

After a few seconds, the verbosity trace hits an "r" and reports "unknown".
It gives me a solution with a cost of 7... I don't think that's the optimal
solution (e.g., if you duplicate all the constraints, it finds a solution of
cost 12, not 14).  I get the feeling that it's hitting a time out, but I'm
not sure.  The exact output is below.  Is there something else I need to do
for it to give me an optimal solution?

 - Mike



.cost(9)..cost(7)...........c..........c.r
unknown
(= x13 101) (= x1 -90) (= x11 259) (= x12 -78) (= x5 -120) (= x16 -129) (=
x7 -188) (= x2 -31) (= x14 -48) (= x19 33) (= x8 -121) (= x3 -142) (= x15
159) (= x6 -16) (= x18 -51) (= x4 -131) (= x9 -46) (= x10 0) (= x17 49) (=
x0 -148)
cost: 7
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/yices-help/attachments/20070228/31970e2d/attachment.html