NAME

       mobical - CaDiCaL Simplified Satisfiability Solver

DESCRIPTION

       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     increase verbosity

       --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)

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

       --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

       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>'.

       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'

       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 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'.