[YICES] Max-sat and unsat core

Bruno Dutertre bruno at csl.sri.com
Mon Apr 11 11:17:19 PDT 2011


Sanjai Narain wrote:
>  Hi Bruno: The specification is unsatisfiable even with max-sat because 
> the weights are not specified, hence are assumed to be infinite. 
> Correct? -- Sanjai
> 

Yes, you're right. Then, there's no reason not to print the
unsat core in this case. That will be fixed in the next
release,

Bruno



More information about the YICES mailing list