let verify_arg_spec () = [
    (arg_spec_of_symbols
       "-mc-engine"
       mc_engine_names
       mc_engine_opt
       "Model-checking engine")
    ;
    (arg_spec_of_symbols
       "-tc-engine"
       tc_engine_names
       tc_engine_opt
       "Trace-checking engine")
    ;
    (arg_spec_of_integer
       "-k-min"
       (-1)
       k_min_opt
       "Minimum value of extrapolation parameter")
    ;
    (arg_spec_of_integer
       "-k-max"
       0
       k_max_opt
       "Maximum value of extrapolation parameter")
    ;
    ("-tc-discard-states",
     Arg.Set tc_discard_states_opt,
     " Ignore abstract states for trace checking")
    ;
    ("-tc-validate",
     Arg.Set tc_validate_opt,
     " Validate all trace-checking results")
    ;
    (arg_spec_of_integer
       "-limit"
       0
       limit_opt
       "Maximum number of model-checker iterations")
    ;
    ("-no-scm-consistency-check",
     Arg.Clear scm_consistency_check_opt,
     " Disable consistency check of input SCM description")
    ;
    ("-no-validation",
     Arg.Clear result_validation_opt,
     " Disable validation of the model-checking result")
    ;
    ("-statistics",
     Arg.Set show_statistics_opt,
     " Show performance statistics")
  ]