+;; *)\r
+\r
+let parse x =\r
+ match read_smt ([],[]) (explode x) with\r
+ | Some [y], [], _ -> y\r
+ | _, _, _ -> assert false\r
+;;\r
+\r
+\r
+let parse_many strs =\r
+ let f (x, y) z = match read_smt y (explode z) with\r
+ | Some[tm], [], vars -> (tm :: x, vars)\r
+ | _, _, _ -> assert false\r
+ in let aux = List.fold_left f ([], ([], []))\r
+ in let (tms, (_, free)) = aux strs\r
+ in (List.rev tms, free)\r