let check ctx expected_result =
  begin
    let (result,m) = Z3.check_and_get_model ctx in
    (match result with
    | Z3.L_FALSE -> printf "unsat\n";
    | Z3.L_UNDEF ->
      printf "unknown\n";
      printf "potential model:\n%s\n" (Z3.model_to_string ctx m);
    | Z3.L_TRUE -> printf "sat\n%s\n" (Z3.model_to_string ctx m);
    );
    if result != expected_result then exitf "unexpected result";
  end