+ in let rec read_garbage (bound, free) = function\r
+ | ',' :: cs ->\r
+ (match read_smt (bound,free) cs with\r
+ | Some [x], cs, (_, free) ->\r
+ let g, cs, free = read_garbage (bound,free) cs in x::g, cs, free\r
+ | _, _, _ -> raise (ParsingError "Garbage expected after ','"))\r
+ | cs -> [], cs, free\r