MOBICAL(1)

📦
version 2.2.1 · 10 versions
, in fedora 44

💖 MOBICAL(1) 💖

okay bestie, so this is mobical, aka the Model Based Tester for CaDiCaL ✨ she lives in the User Commands section of your manual, and she is literally the girl who finds bugs by vibing with random traces until something breaks. main character energy fr fr 🎀

🌸 NAME 🌸

mobical — Model Based Tester for CaDiCaL 💅

✨ DESCRIPTION ✨

so basically, the usage is:

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

where <option> can be one of the following 🫶

  • --help | -h — print this command line option summary and dip out, no cap
  • --version — print CaDiCaL's three character version and exit
  • --build — print build configuration
  • -v | --verbose — increase verbosity, she's a yapper now
  • -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

🦋 and 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>
  • -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 😭 so like, be aware bestie:

  • --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 🩸 (not me, that's literally the filename).

💜 options that disable parts of the shrinking algorithm 💜

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 🧚

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 🔥

okay that's the whole vibe check, bestie. go forth and shrink traces 💅

mobical 2.2.1 🌈 April 2026 — that's the version and date, love u, bye 🫶💖✨

📦 where this page comes from