diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml index 2bfbf206c16f339affdb9ead83fd1fa5522404e6..25df277e58c6df6fdfcf1e16a0139b3fc472dce8 100644 --- a/src/coalg/coalg.ml +++ b/src/coalg/coalg.ml @@ -94,9 +94,12 @@ let verbose = ref false let choiceSat () = let verb = !verbose in let sorts = (FE.sortTableFromString Sys.argv.(2)) in - if Array.exists (fun (func,_) -> func == CM.GML || func == CM.PML) sorts then + + (* test if GML or PML occurs in sort table *) + if Array.fold_left (fun x (func,_) -> x || func == CM.GML || func == CM.PML) false sorts then raise (CF.CoAlgException "GML and PML are currently not supported") else (); + let printRes sat = if not verb then print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")