NAME

       alt-ergo - Execute Alt-Ergo on the given file.

SYNOPSIS

       alt-ergo [OPTION]… [FILE]

ARGUMENTS

       FILE
           Source file. Must be suffixed by .ae, (.mlw and .why are depreciated, .smt2 or .psmt2.

OPTIONS

       -d, --debug
           Set the debugging flag.

       -i FMT, --input=FMT
           Set the default input format to FMT and must be one of native, altergo, alt-ergo,
           smtlib2, smt-lib2 or why3. Useful when the extension does not allow to automatically
           select a parser (eg. JS mode, GUI mode, ...).

       -m VAL, --model=VAL (absent=none)
           Experimental support for models on labeled terms. VAL must be one of none, default,
           complete or all. 'complete' shows a complete model and 'all' shows all models.

       -o FMT, --output=FMT
           Control the output format of the solver, FMT must be either native or smtlib.The
           alt-ergo native format outputs Valid/Invalid/I don't know.The smtlib format outputs
           unsat/sat/unknown.If left unspecified, Alt-Ergo will use its heuristics to determine
           the adequate output format according to the input format.It must be noticed that not
           specifying an output format will let Alt-Ergo set it according to the input file's
           extension.

       -p, --pretty-output
           Print output with formatting rules, headers and colors

       -r, --replay-used-context
           Replay with axioms and predicates saved in .used file.

       -S STEPS, --steps-bound=STEPS (absent=-1)
           Set the maximum number of steps.

       -s, --save-used-context
           Save used axioms and predicates in a .used file. This option implies --unsat-core.

       -t VAL, --timelimit=VAL
           Set the time limit to VAL seconds (not supported on Windows).

       -u, --unsat-core
           Experimental support for computing and printing unsat-cores.

       -v, --verbose
           Set the verbose mode.

EXECUTION OPTIONS

       --add-parser=VAL
           Register a new parser for Alt-Ergo.

       --colors-in-output
           Print output with colors.

       --frontend=FTD (absent=legacy)
           Select the parsing and typing frontend.

       --no-forced-flush-in-output
           Print output without forced flush at the end of each print.

       --no-formatting-in-output
           Don not use formatting rule in output.

       --no-headers-in-output
           Print output without headers.

       --no-locs-in-answers
           Do not show the locations of goals when printing solver's answers.

       --parse-only
           Stop after parsing.

       --prelude=VAL
           Add a file that will be loaded as a prelude. The command is cumulative, and the order
           of successive preludes is preserved.

       --type-only
           Stop after typing.

       --type-smt2
           Stop after SMT2 typing.

LIMIT OPTIONS

       --age-bound=AGE (absent=50)
           Set the age limit bound.

       --fm-cross-limit=VAL (absent=10000)
           Skip Fourier-Motzkin variables elimination steps that may produce a number of
           inequalities that is greater than the given limit. However, unit eliminations are
           always done.

       --timelimit-interpretation=SEC
           Set the time limit to SEC seconds for model generation (not supported on Windows).

       --timelimit-per-goal
           Set the timelimit given by the --timelimit option to apply for each goal, in case of
           multiple goals per file. In this case, time spent in preprocessing is separated from
           resolution time. Not relevant for GUI-mode.

INTERNAL OPTIONS

       --disable-weaks
           Prevent the GC from collecting hashconsed data structrures that are not reachable
           (useful for more determinism).

       --enable-assertions
           Enable verification of some heavy invariants.

       --gc-policy=PLCY (absent=0)
           Set the gc policy allocation. 0 = next-fit policy, 1 = first-fit policy, 2 = best-fit
           policy. See the Gc module of the OCaml distribution for more informations.

       --warning-as-error
           Enable warning as error

OUTPUT OPTIONS

       --interpretation=VAL (absent=0)
           Experimental support for counter-example generation. Possible values are 1, 2, or 3 to
           compute an interpretation before returning Unknown, before instantiation (1), or
           before every decision (2) or instantiation (3). A negative value (-1, -2, or -3) will
           disable interpretation display. Note that  --max-split limitation will be ignored in
           model generation phase.

CONTEXT OPTIONS

       --replay
           Replay session saved in file_name.agr.

       --replay-all-used-context
           Replay with all axioms and predicates saved in .used files of the current directory.

PROFILING OPTIONS

       --cumulative-time-profiling
           Record the time spent in called functions in callers

       --profiling=DELAY
           Activate the profiling module with the given frequency. Use Ctrl-C to switch between
           different views and "Ctrl + AltGr + \ " to exit.

       --profiling-plugin=PGN
           Use the given profiling plugin.

SAT OPTIONS

       --bottom-classes
           Show equivalence classes at each bottom of the sat.

       --disable-flat-formulas-simplification
           Disable facts simplifications in satML's flat formulas.

       --enable-restarts
           For satML: enable restarts or not. Default behavior is 'false'.

       --no-arith-matching
           Disable (the weak form of) matching modulo linear arithmetic.

       --no-backjumping
           Disable backjumping mechanism in the functional SAT solver.

       --no-backward
           Disable backward reasoning step (starting from the goal) done in the default SAT
           solver before deciding.

       --no-decisions
           Disable decisions at the SAT level.

       --no-decisions-on=[INST1; INST2; ...]
           Disable decisions at the SAT level for the instances generated from the given axioms.
           Arguments should be separated with a comma.

       --no-minimal-bj
           Disable minimal backjumping in satML CDCL solver.

       --no-sat-learning
           Disable learning/caching of unit facts in the Default SAT. These facts are used to
           improve bcp.

       --no-tableaux-cdcl-in-instantiation
           When satML is used, this disables the use of a tableaux-likemethod for instantiations
           with the CDCL solver.

       --no-tableaux-cdcl-in-theories
           When satML is used, this disables the use of a tableaux-likemethod for theories with
           the CDCL solver.

       --sat-plugin=VAL
           Use the given SAT-solver instead of the default DFS-based SAT solver.

       --sat-solver=SAT (absent=CDCL-Tableaux)
           Choose the SAT solver to use. Default value is CDCL (i.e. satML solver). Possible
           options are one of CDCL, satML, CDCL-Tableaux, satML-Tableaux or Tableaux-CDCL.

QUANTIFIERS OPTIONS

       --inst-after-bj
           Make a (normal) instantiation round after every backjump/backtrack.

       --instantiation-heuristic=VAL (absent=auto)
           Change the instantiation heuristic. VAL must be one of normal, auto or greedy. By
           default 'auto' is used for both sat solvers. 'normal' does one less phase of
           instantiation. 'greedy' use all available ground terms in instantiation.

       --max-multi-triggers-size=VAL (absent=4)
           Maximum size of multi-triggers, i.e. the maximum number of independent patterns in a
           multi-trigger.

       --nb-triggers=VAL (absent=2)
           Maximum number of triggers used (including regular and multi triggers).

       --no-ematching
           Disable matching modulo ground equalities.

       --no-user-triggers
           Ignore user triggers, except for triggers of theories' axioms

       --normalize-instances
           Normalize generated substitutions by matching w.r.t. the state of the theory. This
           means that only terms that are greater (w.r.t. depth) than the initial terms of the
           problem are normalized.

       --triggers-var
           Allows variables as triggers.

TERM OPTIONS

       --disable-ites
           Disable handling of ite(s) on terms in the backend.

       --inline-lets
           Enable substitution of variables bounds by Let. The default behavior is to only
           substitute variables that are bound to a constant, or that appear at most once.

       --rwt, --rewriting
           Use rewriting instead of axiomatic approach.

       --term-like-pp
           Output semantic values as terms.

THEORY OPTIONS

       --disable-adts
           Disable Algebraic Datatypes theory.

       --inequalities-plugin=VAL
           Use the given module to handle inequalities of linear arithmetic.

       --no-ac
           Disable the AC theory of Associative and Commutative function symbols.

       --no-contracongru
           Disable contracongru.

       --no-fm
           Disable Fourier-Motzkin algorithm.

       --no-nla
           Disable non-linear arithmetic reasoning (i.e. non-linear multplication, division and
           modulo on integers and rationals). Non-linear multiplication remains AC.

       --no-tcp
           Deactivate Boolean Constant Propagation (BCP) modulo theories.

       --no-theory
           Completely deactivate theory reasoning.

       --restricted
           Restrict set of decision procedures (equality, arithmetic and AC).

       --tighten-vars
           Compute the best bounds for arithmetic variables.

       --use-fpa
           Enable support for floating-point arithmetic.

CASE SPLIT OPTIONS

       --case-split-policy=PLCY (absent=after-theory-assume)
           Case-split policy. Set the case-split policy to use. Possible values are one of
           after-theory-assume, before-matching or after-matching.

       --enable-adts-cs
           Enable case-split for Algebraic Datatypes theory.

       --max-split=VAL (absent=1000000)
           Maximum size of case-split.

HALTING OPTIONS

       --version-info
           Print some info about this version (version, date released, date commited) .

       --where=DIR
           Print the directory of DIR. Possible arguments are one of lib, plugins, preludes, data
           or man.

FORMATTER OPTIONS

       --err-formatter=VAL (absent=stderr)
           Set the error formatter used by default to output error, debug and warning
           informations. Possible values are one of stdout, stderr or <filename>.

       --std-formatter=VAL (absent=stdout)
           Set the standard formatter used by default to output the results, models and unsat
           cores. Possible values are one of stdout, stderr or <filename>.

DEBUG OPTIONS

       These options are used to output debug info for the concerned part of the solver.They are
       not used to check internal consistency.

       --dac
           Set the debugging flag of ac.

       --dadt
           Set the debugging flag of ADTs.

       --darith
           Set the debugging flag of Arith (without fm).

       --darrays
           Set the debugging flag of arrays.

       --dbitv
           Set the debugging flag of bitv.

       --dcc
           Set the debugging flag of cc.

       --dcombine
           Set the debugging flag of combine.

       --dconstr
           Set the debugging flag of constructors.

       --debug-interpretation
           Set debug flag for interpretation generatation.

       --debug-unsat-core
           Replay unsat-cores produced by --unsat-core. The option implies --unsat-core.

       --dexplanations
           Set the debugging flag of explanations.

       --dfm
           Set the debugging flag of inequalities.

       --dfpa=VAL (absent=0)
           Set the debugging flag of floating-point.

       --dgc
           Prints some debug info about the GC's activity.

       --dite
           Set the debugging flag of ite.

       --dmatching=FLAG (absent=0)
           Set the debugging flag of E-matching (0=disabled, 1=light, 2=full).

       --dsat
           Set the debugging flag of sat.

       --dsplit
           Set the debugging flag of case-split analysis.

       --dsum
           Set the debugging flag of Sum.

       --dtriggers
           Set the debugging flag of triggers.

       --dtypes
           Set the debugging flag of types.

       --dtyping
           Set the debugging flag of typing.

       --duf
           Set the debugging flag of uf.

       --duse
           Set the debugging flag of use.

       --dwarnings
           Set the debugging flag of warnings.

       --rule=TR (absent=none)
           TR = parsing|typing|sat|cc|arith, output rule used on stderr.

COMMON OPTIONS

       --help[=FMT] (default=auto)
           Show this help in format FMT. The value FMT must be one of auto, pager, groff or
           plain. With auto, the format is pager or plain whenever the TERM env var is dumb or
           undefined.

       --version
           Show version information.

EXIT STATUS

       alt-ergo exits with the following status:

       0   on success.

       1   on default errors

       123 on indiscriminate errors reported on standard error.

       124 on command line parsing errors.

       125 on unexpected internal errors (bugs).

       142 on timeout errors

BUGS

       You can open an issue on: https://github.com/OCamlPro/alt-ergo/issues

       Or you can write to:
          alt-ergo@ocamlpro.com

AUTHORS

       CURRENT AUTHORS
          Sylvain Conchon
          Albin Coquereau
          Guillaume Bury
          Mattias Roux

       ORIGINAL AUTHORS
          Sylvain Conchon
          Evelyne Contejean
          Mohamed Iguernlala
          Stephane Lescuyer
          Alain Mebsout