HaifaSmtMuc (HSmtMUC) is a minimal unsatisfiable core extractor for SMT formulas.
HSmtMuc is a tool for extracting a minimal unsatisfiable core of Satisfiability Modulo Theories (SMT) formulas. It is implemented on top of Microsoft’s Z3 SMT solver.
Given an unsatisfiable formula in conjunctive normal form (CNF), an unsatisfiable core (UC) is any subset of these clauses that is still unsatisfiable. An unsatisfiable core is called minimal if it is irreducible, i.e., no single clause can be removed without making the formula satisfiable. A minimal core is also a minimum core if its size is the smallest possible for an unsatisfiable core. HSmtMuc finds minimal cores, which are not necessarily minimum.