tests: Run reasoner in new process for each formula

As it stands, cool leaks tons of memory with each `isSat` call. Until
this is fixed, the new `--slow` testsuite would need at least 16GB of
memory if all formulas are decided in one process. Thus, we now call
isSat in a new child-process and allow the OS to reclaim memory after
the child exits.

NB: This uses the Unix.fork API, which is not available on Windows.

src/testsuite/Testsuite.ml

@@ -38,8 +38,15 @@ let runSatCheck (_,logic,input) =
         Some 0
       in
       let (tbox, f) = CoAlgFormula.importQuery input in
-      let res = CoAlgReasoner.isSat logic nomTable tbox f in
-      if res then Sat else Unsat
+      (* isSat leaks tons of memory. Call it in new process to allow the OS to
+         reclaim that memory between calls. *)
+      match Unix.fork () with
+      | 0 -> let res = CoAlgReasoner.isSat logic nomTable tbox f in
+             if res then exit 0 else exit 1
+      | -1 -> raise (CoAlgFormula.CoAlgException "fork() failed")
+      | _ -> match Unix.wait () with
+             | (_,Unix.WEXITED 0) -> Sat
+             | _ -> Unsat
   with | Stream.Error _ -> ParseError
        | CoAlgFormula.CoAlgException _ -> ParseError