solver.options().setReporter(oldReporter);
// If unsatisfiable, then retreive the unsat core if desired
if (inst==null && solver.options().solver()==SATFactory.MiniSatProver) {
try {
lCore = new LinkedHashSet<Node>();
Proof p = sol.proof();
if (sol.outcome()==UNSATISFIABLE) {
// only perform the minimization if it was UNSATISFIABLE, rather than TRIVIALLY_UNSATISFIABLE
int i = p.highLevelCore().size();
rep.minimizing(cmd, i);
if (opt.coreMinimization==0) try { p.minimize(new RCEStrategy(p.log())); } catch(Throwable ex) {}
if (opt.coreMinimization==1) try { p.minimize(new HybridStrategy(p.log())); } catch(Throwable ex) {}
rep.minimized(cmd, i, p.highLevelCore().size());
}
for(Iterator<TranslationRecord> it=p.core(); it.hasNext();) {
Object n=it.next().node();
if (n instanceof Formula) lCore.add((Formula)n);
}
Map<Formula,Node> map = p.highLevelCore();
hCore = new LinkedHashSet<Node>(map.keySet());
hCore.addAll(map.values());
} catch(Throwable ex) {
lCore = hCore = null;
}