[YICES] Max-sat and unsat core

[Bruno Dutertre]

Sanjai Narain wrote:
>  The following spec is unsatisfiable but Yices does not print the 
> unsat-core. Replacing (max-sat) with (check) does. Is there a way to get 
> unsat-core with (max-sat)? Thanks -- Sanjai
> 
> 
> (define-type node (scalar a b))
> (define prop::(-> node int))
> (assert+ (= (prop a) (prop b)))
> (assert+ (= (prop a) 1))
> (assert+ (= (prop b) 2))
> 
> (max-sat)
> 

I'm not sure what you mean by unsat core if you use max-sat.
The whole point of max-sat is to search for a Boolean assignment
that satisfies as many assertions as possible, so from a "max-sat"
point-of-view, these assertions are satisfiable and there's no
unsat core.

Bruno