LTL_f Unsat Core Extraction

We leverage on the work [1] below extended to handle LTL_f through rewriting to LTL.

[1] Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta: Boolean Abstraction for Temporal Logic Satisfiability. CAV 2007: 532-546