[YICES-HELP] Unsatisfiable Cores

Stephan Zimmer st.zimmer at web.de
Mon May 14 07:59:37 PDT 2007


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



More information about the YICES-HELP mailing list