unfold fixpoints when creating new Cores

src/lib/CoAlgReasoner.ml

@@ -476,6 +476,23 @@ let newCore sort bs =
         assert (okay1);
         let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
         assert (okay2)
+	| MuF
+	| NuF ->
+	   (*
+          Dest of a fixpoint is it's unfolded version. This adds just
+          an simple forward implication that could be optimised out
+          though not without nontrivial transformation of code
+
+            f = μ X . φ   |---> lf
+            φ[X |-> f]    |---> lf1
+
+          Then adding lf -> lf1 to minisat
+		*)
+	   let f1 = lfGetDest1 sort f in
+	   addClauses f1;
+	   let lf1 = fhtMustFind fht f1 in
+	   let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
+       assert (okay1);
     | _ -> ()
         (* case 2.(c)
             We don't need to do anything except adding f to the fht