[YICES-HELP] Unsatisfiable Cores

[Bruno Dutertre]

Stephan Zimmer wrote:
> Hi,
> 
> is thery any way to avoid the (possibly very long) enumerations of
> (potential) models in the evidence (verbosity >= 2) mode (if the
> context is considered as "unknown" or "sat" by yices) while still
> getting information about unsatisfiable subsets of the formulae
> context ("unsat core ids: ...") in case the context was proven
> unsatisfiable? I.e. after performing a "check" I would only be
> interested in unsatisfiable cores but not in (potential) models.
> 
> Thanks in advance,
> Stephan
> 

Hi Stephan,

There is currently no way to do this since the same flag
controls both model generation and computation of unsatisfiable
cores. I will fix that in the next release by adding separate
flags.

Bruno