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)

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

mobical 2.1.3                                     December 2025                                       MOBICAL(1)