let assert_comm_axiom ctx f =
  begin
    let t      = Z3.get_range ctx f in
    if Z3.get_domain_size ctx f != 2 || not (equal_sorts ctx (Z3.get_domain ctx f 0) t) || not (equal_sorts ctx (Z3.get_domain ctx f 1) t) then 
      exitf "function must be binary, and argument types must be equal to return type";
    (* Inside the parser, function f will be referenced using the symbol 'f'. *)
    let f_name = Z3.mk_string_symbol ctx "f" in
    (* Inside the parser, type t will be referenced using the symbol 'T'. *)
    let t_name = Z3.mk_string_symbol ctx "T" in
    let str    = "(benchmark comm :formula (forall (x T) (y T) (= (f x y) (f y x))))" in
    let q = Z3.parse_smtlib_string_formula ctx str [|t_name|] [|t|] [|f_name|] [|f|] in
    printf "assert axiom:\n%s\n" (Z3.ast_to_string ctx q);
    Z3.assert_cnstr ctx q;
  end