Skip to content

Show default value of options by default

Viktor Kuncak requested to merge github/fork/romac/better-flags into master

Created by: romac

Before:

[  Info  ] Inox solver (https://github.com/epfl-lara/inox)
[  Info  ] Version: 1.1.0-332-ga6cbf8e-SNAPSHOT
[  Info  ]
[  Info  ] Usage: inox [OPTION]... FILE...
[  Info  ]
[  Info  ] General
[  Info  ] --debug=d1,d2,...                      Enable detailed messages per component.
[  Info  ]                                        Available:
[  Info  ]                                          solver, timers,
[  Info  ]                                          tip
[  Info  ] --help                                 Show help message
[  Info  ] --solvers=s1,s2,...                    Use solvers s1,s2,...
[  Info  ]                                        Available:
[  Info  ]                                          nativez3       : Native Z3 with z3-templates for unrolling
[  Info  ]                                          nativez3-opt   : Native Z3 optimizer with z3-templates for unrolling
[  Info  ]                                          princess       : Princess with inox unrolling
[  Info  ]                                          smt-cvc4       : CVC4 through SMT-LIB
[  Info  ]                                          smt-z3         : Z3 through SMT-LIB
[  Info  ]                                          smt-z3-opt     : Z3 optimizer through SMT-LIB
[  Info  ]                                          unrollz3       : Native Z3 with inox-templates for unrolling
[  Info  ] --timeout=t                            Set a timeout for the solver (in sec.)
[  Info  ]
[  Info  ] Evaluators
[  Info  ] --ignore-contracts                     Don't fail on invalid contracts during evaluation
[  Info  ] --max-calls=<PosInt> | -1 (unbounded)  Maximum function invocations allowed during evaluation
[  Info  ]
[  Info  ] Printing
[  Info  ] --print-chooses                        Display partial models for chooses when printing models
[  Info  ] --print-ids                            Always print unique ids
[  Info  ] --print-positions                      Attach positions to trees when printing
[  Info  ] --print-types                          Attach types to trees when printing
[  Info  ]
[  Info  ] Solvers
[  Info  ] --assume-checked                       Assume that all impure expression have been checked
[  Info  ] --check-models                         Double-check counter-examples with evaluator
[  Info  ] --feeling-lucky                        Use evaluator to find counter-examples early
[  Info  ] --model-finding=<PosInt> | 0 (off)     Enhance model-finding capabilities of solvers by given aggressivity
[  Info  ] --no-simplifications                   Disable selector/quantifier simplifications in solvers
[  Info  ] --silent-errors                        Fail silently into UNKNOWN when encountering an error
[  Info  ] --solver:cvc4=<cvc4-opt>               Pass extra options to CVC4
[  Info  ] --unroll-assumptions                   Use unsat-assumptions to drive unfolding while remaining fair
[  Info  ] --unroll-factor=<PosInt>               Number of unrollings to perform in each unfold step

After:

[  Info  ] Inox solver (https://github.com/epfl-lara/inox)
[  Info  ] Version: 1.1.0-332-ga6cbf8e-SNAPSHOT
[  Info  ]
[  Info  ] Usage: inox [OPTION]... FILE...
[  Info  ]
[  Info  ] General
[  Info  ] --debug=d1,d2,...                      Enable detailed messages per component. (default: <none>)
[  Info  ]                                        Available:
[  Info  ]                                          solver, timers,
[  Info  ]                                          tip
[  Info  ] --help                                 Show help message
[  Info  ] --solvers=s1,s2,...                    Use solvers s1,s2,... (default: nativez3)
[  Info  ]                                        Available:
[  Info  ]                                          nativez3       : Native Z3 with z3-templates for unrolling
[  Info  ]                                          nativez3-opt   : Native Z3 optimizer with z3-templates for unrolling
[  Info  ]                                          princess       : Princess with inox unrolling
[  Info  ]                                          smt-cvc4       : CVC4 through SMT-LIB
[  Info  ]                                          smt-z3         : Z3 through SMT-LIB
[  Info  ]                                          smt-z3-opt     : Z3 optimizer through SMT-LIB
[  Info  ]                                          unrollz3       : Native Z3 with inox-templates for unrolling
[  Info  ] --timeout=t                            Set a timeout for the solver (in sec.) (default: 0 days)
[  Info  ]
[  Info  ] Evaluators
[  Info  ] --ignore-contracts[=true|false]        Don't fail on invalid contracts during evaluation (default: false)
[  Info  ] --max-calls=<PosInt> | -1 (unbounded)  Maximum function invocations allowed during evaluation (default: 50000)
[  Info  ]
[  Info  ] Printing
[  Info  ] --print-chooses[=true|false]           Display partial models for chooses when printing models (default: false)
[  Info  ] --print-ids[=true|false]               Always print unique ids (default: false)
[  Info  ] --print-positions[=true|false]         Attach positions to trees when printing (default: false)
[  Info  ] --print-types[=true|false]             Attach types to trees when printing (default: false)
[  Info  ]
[  Info  ] Solvers
[  Info  ] --assume-checked[=true|false]          Assume that all impure expression have been checked (default: false)
[  Info  ] --check-models[=true|false]            Double-check counter-examples with evaluator (default: false)
[  Info  ] --feeling-lucky[=true|false]           Use evaluator to find counter-examples early (default: false)
[  Info  ] --model-finding=<PosInt> | 0 (off)     Enhance model-finding capabilities of solvers by given aggressivity (default: 0)
[  Info  ] --no-simplifications[=true|false]      Disable selector/quantifier simplifications in solvers (default: false)
[  Info  ] --silent-errors[=true|false]           Fail silently into UNKNOWN when encountering an error (default: false)
[  Info  ] --solver:cvc4=<cvc4-opt>               Pass extra options to CVC4 (default: <none>)
[  Info  ] --unroll-assumptions[=true|false]      Use unsat-assumptions to drive unfolding while remaining fair (default: false)
[  Info  ] --unroll-factor=<PosInt>               Number of unrollings to perform in each unfold step (default: 1)

Merge request reports