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