usage: mobical [ <option> ... ] [ <mode> ]

where '<option>' can be one of the following:

  --help    | -h    print this command line option summary and exit
  --version         print CaDiCaL's three character version and exit
  --build           print build configuration

  -v | --verbose    increase verbosity
  -q | --quiet      be quiet (only print failing and reduced traces)

  --colors          force colors for both '<stdout>' and '<stderr>'
  --no-colors       disable colors if '<stderr>' is connected to terminal
  --no-terminal     assume '<stderr>' is not connected to terminal
  --no-seeds        do not print seeds in random mode

  -<n>              specify the number of solving phases explicitly
  --time <seconds>  set time limit per trace (none=0, default=10)
  --space <MB>      set space limit (none=0, default=1024)
  --bad-alloc       generate failing memory allocations, monitor for crashes
  --leak-alloc      generate failing memory allocations, monitor for leaks

  --do-not-ignore-resource-limits consider out-of-time or memory as error

  --tiny            generate tiny formulas only
  --small           generate small formulas only
  --medium          generate medium sized formulas only
  --big             generate big formulas only

Then '<mode>' is one of these

  <seed>            generate and execute trace for given 64-bit seed
  <seed>  <output>  generate trace, shrink and write it to file
  <input> <output>  read trace, shrink and write it to output file
  <input>           read and replay the specified input trace

In order to let the test execute '<r>' runs (starting from '<seed>') use:

  -L[ ]<r>          execute '<r>' runs

The output trace is not shrunken if it is not failing.  However, before
it is written it is executed, unless '--do-not-execute' is specified:

  --do-not-execute  just write to '<output>' without execution

In order to check memory issues or collect coverage you can force
execution within the main process, which however also means that the
model based tester aborts as soon a test fails

  --do-not-fork     execute all tests in main process directly

In order to replay a trace which violates an API contract use

  --do-not-enforce-contracts

To read from '<stdin>' use '-' as '<input>' and also '-' instead of
'<output>' to write to '<stdout>'.

As the library is compiled with logging support ('-DLOGGING')
one can force to add the 'set log 1' call to the trace with

  --log | -l        force low-level logging for detailed debugging

Implicitly add 'dump' and 'stats' calls to traces:

  --dump  | -d      force dumping the CNF before every 'solve'
  --stats | -s      force printing statistics after every 'solve'

Implicitly add 'configure plain' after setting options:

  --plain | -p

Otherwise if no '<mode>' is specified the default is to generate random
traces internally until the execution of a trace fails, which means it
produces a non-zero exit code.  Then the trace is rerun and shrunken
through delta-debugging to produce a smaller trace.  The shrunken failing
trace is written as 'red-<seed>.trace' to the current working directory.

The following options disable certain parts of the shrinking algorithm:

  --do-not-shrink[-at-all]
  --do-not-add-options[-before-shrinking]
  --do-not-shrink-phases
  --do-not-shrink-clauses
  --do-not-shrink-literals
  --do-not-shrink-basic[-calls]
  --do-not-disable[-options]
  --do-not-reduce[[-option]-values]
  --do-not-shrink-variables
  --do-not-shrink-options

The standard mode of using the model based tester is to start it in
random testing mode without '<input>', '<seed>' nor '<output>' option.
If a failing trace is found it will be shrunken and the resulting
trace written to the current working directory.  Then the model based
tester can be interrupted and then called again with the produced
failing trace as single argument.

This second invocation will execute the trace within the same process
and thus can directly be investigated with a symbolic debugger such
as 'gdb' or maybe first checked for memory issues with 'valgrind'
or recompilation with memory checking '-fsanitize=address'.