Optimization techniques for Craig Interpolant compaction in Unbounded Model Checking