id     = "DRIVER"
name   = "Driver"

[[option]]
  name       = "version"
  category   = "common"
  short      = "V"
  long       = "version"
  type       = "bool"
  alternate  = false
  help       = "identify this cvc5 binary"

[[option]]
  name       = "help"
  category   = "common"
  short      = "h"
  long       = "help"
  type       = "bool"
  alternate  = false
  help       = "full command line reference"

[[option]]
  category   = "common"
  long       = "show-config"
  type       = "void"
  handler    = "showConfiguration"
  help       = "show cvc5 static configuration"

[[option]]
  category   = "common"
  long       = "copyright"
  type       = "void"
  handler    = "copyright"
  help       = "show cvc5 copyright information"

[[option]]
  name       = "seed"
  category   = "common"
  short      = "s"
  long       = "seed=N"
  type       = "uint64_t"
  default    = "0"
  help       = "seed for random number generator"

[[option]]
  category   = "regular"
  long       = "show-debug-tags"
  type       = "void"
  handler    = "showDebugTags"
  help       = "show all available tags for debugging"

[[option]]
  category   = "regular"
  long       = "show-trace-tags"
  type       = "void"
  handler    = "showTraceTags"
  help       = "show all available tags for tracing"

[[option]]
  name       = "earlyExit"
  category   = "expert"
  long       = "early-exit"
  type       = "bool"
  default    = "true"
  help       = "do not run destructors at exit; default on except in debug builds"

[[option]]
  name       = "interactive"
  category   = "regular"
  long       = "interactive"
  type       = "bool"
  help       = "force interactive shell/non-interactive mode"

[[option]]
  name       = "filename"
  category   = "undocumented"
  long       = "filename=FILENAME"
  type       = "std::string"
  help       = "filename of the input"

[[option]]
  name       = "segvSpin"
  category   = "regular"
  long       = "segv-spin"
  type       = "bool"
  default    = "false"
  help       = "spin on segfault/other crash waiting for gdb"

[[option]]
  name       = "dumpModels"
  category   = "regular"
  long       = "dump-models"
  type       = "bool"
  default    = "false"
  help       = "output models after every SAT/INVALID/UNKNOWN response"

[[option]]
  name       = "dumpProofs"
  category   = "regular"
  long       = "dump-proofs"
  type       = "bool"
  default    = "false"
  help       = "output proofs after every UNSAT/VALID response"

[[option]]
  name       = "dumpInstantiations"
  category   = "regular"
  long       = "dump-instantiations"
  type       = "bool"
  default    = "false"
  help       = "output instantiations of quantified formulas after every UNSAT/VALID response"

[[option]]
  name       = "dumpInstantiationsDebug"
  category   = "regular"
  long       = "dump-instantiations-debug"
  type       = "bool"
  default    = "false"
  help       = "output instantiations of quantified formulas after every UNSAT/VALID response, with debug information"

[[option]]
  name       = "dumpUnsatCores"
  category   = "regular"
  long       = "dump-unsat-cores"
  type       = "bool"
  default    = "false"
  help       = "output unsat cores after every UNSAT/VALID response"

[[option]]
  name       = "dumpUnsatCoresFull"
  category   = "regular"
  long       = "dump-unsat-cores-full"
  type       = "bool"
  default    = "false"
  help       = "dump the full unsat core, including unlabeled assertions"

[[option]]
  name       = "dumpDifficulty"
  category   = "regular"
  long       = "dump-difficulty"
  type       = "bool"
  default    = "false"
  help       = "dump the difficulty measure after every response to check-sat"

[[option]]
  name       = "forceNoLimitCpuWhileDump"
  category   = "regular"
  long       = "force-no-limit-cpu-while-dump"
  type       = "bool"
  default    = "false"
  help       = "Force no CPU limit when dumping models and proofs"