| "lpo" -> Utils.compare_terms := Utils.lpo
| "kbo" -> Utils.compare_terms := Utils.kbo
| "nr-kbo" -> Utils.compare_terms := Utils.nonrec_kbo
+ | "ao" -> Utils.compare_terms := Utils.ao
| o -> raise (Arg.Bad ("Unknown term ordering: " ^ o))
and set_fullred b = S.use_fullred := b
and set_time_limit v = S.time_limit := float_of_int v