--- name: "stp" section: "1" platform: "linux" package: "stp" version: "2.4.1-2" release: "Arch Linux 2026-11-01" platforms: ["linux"] url: "https://new.carta.tech/stp" --- # stp(1) Simple Theorem Prover SMT solver ## NAME stp - Simple Theorem Prover SMT solver ## DESCRIPTION USAGE: stp \[options\] \ - where input is SMTLIB1/2 or CVC depending on options and file extension ### Most important options: - **-h** \[ **--help** \] print this help - **--version** print version number ### Simplifications: - **--disable-simplifications** disable all simplifications - **-w** \[ **--switch-word** \] switch off wordlevel solver - **-a** \[ **--disable-opt-inc** \] disable rewriting simplifier - **--disable-cbitp** disable constant bit propagation - **--disable-equality** disable equality propagation - **--size-reducing-only** size reducing simplifications only - **--unconstrained-variable-elimination** arg (=1) Unconstrained variables are eliminated. - **--aig-rewrite-passes** arg (=0) Iterations of AIG rewriting to perform - **--flattening** arg (=0) Enable sharing-aware flattening of \>2 arity nodes - **--rewriting** arg (=1) Enable sharing-aware rewriting - **--split-extracts** arg (=1) Create new variables for some extracts - **--ite-context-simplifications** arg (=0) Use what is known to be true in an if-then-else node to simplify the true or false branches - **--aig-core-simplification** arg (=0) Simplify the propositional core with AIGs - **--use-intervals** arg (=1) Simplify with interval analysis - **--pure-literals** arg (=1) Pure literals are replaced. - **--merge-same** arg (=0) Uses simple boolean algebra rules to combine conjuncts at the top level - **--bit-blast-simplification** arg (=0) Part-way through simplifying, convert to AIGs and look for bits that the AIGs figure out are true/false or the same as another node. If the difficulty is less than this number. **-1** means always. - **--size-reducing-fixed-point-limit** arg (=0) If the number of non-leaf nodes is fewer than this number, run size-reducing simplifications to a fixed-point. **-1** means always. - **--simplify-to-constants-only** arg (=0) Use just the simplifications from the potentially size increasing suite that transform nodes to constants - **--difficulty-reversion** arg (=1) Undo size increasing simplifications if they haven't made the problem simpler ### SAT Solver options: - **--cryptominisat** use cryptominisat as the solver. Only use CryptoMiniSat 5.0 or above - **--threads** arg (=1) Number of threads for cryptominisat - **--simplifying-minisat** use installed simplifying minisat version as the solver - **--minisat** use installed minisat version as the solver - **--search-bias** arg tune the SAT search towards one answer: 'unsat' (best for unsatisfiable / verification workloads), 'sat', or 'none' (the default, leaving the solver at its own settings). Solvers with no such setting ignore it ### Refinement options: - **-r** \[ **--ackermanize** \] eagerly encode array-read axioms (Ackermannistaion) ### Bit-blasting options: - **--bb**.div-v1 arg (=1) unsigned division encoding variant 1 - **--bb**.div-v2 arg (=1) unsigned division encoding variant 2 - **--bb**.div-v3 arg (=0) unsigned division encoding variant 3 - **--bb**.add-v1 arg (=1) addition encoding variant 1 - **--bb**.add-v2 arg (=1) addition encoding variant 2 - **--bb**.vle-v1 arg (=1) comparison encoding variant 1 - **--bb**.mult-variant arg (=1) unsigned multiplication variant - **--bb**.mult-v2 arg (=0) unsigned multiplication variant 2 - **--bb**.conjoin-constant arg (=0) When constant-bit propagation detects a constant bit during AIG construction, assert the AIG node and replace it, in the AIG, by the constant bit ### Printing options: - **-b** \[ **--print-stpinput** \] print STP input back to cout - **--print-back-CVC** print input in CVC format, then exit - **--print-back-SMTLIB2** print input in SMT-LIB2 format, then exit - **--print-back-SMTLIB1** print input in SMT-LIB1 format, then exit - **--print-back-GDL** print AiSee's graph format, then exit - **--print-back-dot** print dotty/neato's graph format, then exit - **-p** \[ **--print-counterex** \] print counterexample - **-y** \[ **--print-counterexbin** \] print counterexample in binary - **-q** \[ **--print-arrayval** \] print arrayval declared order - **-s** \[ **--print-functionstat** \] print function statistics - **-t** \[ **--print-quickstat** \] print quick statistics - **-v** \[ **--print-nodes** \] print nodes - **-n** \[ **--print-output** \] Print output ### Input options: - **-m** \[ **--SMTLIB1** \] use the SMT-LIB1 format parser - **--SMTLIB2** use the SMT-LIB2 format parser - **--CVC** use the CVC format parser ### Output options: - **--output-CNF** Save the CNF into output\_\[0..n\].cnf. NOTE: variables cannot be mapped back, and problems solved by the preprocessing simplifier alone will not generate any CNF as the SAT solver is never invoked - **--output-bench** save in ABC's bench format to output.bench ### Output options: - **--cnf-generation-effort** arg (=medium) effort spent minimising the CNF: very-low, low, medium, high, very-high. Higher is slower to generate but yields a smaller CNF - **--exit-after-CNF** exit after the CNF has been generated - **--parse-only** exit after parsing the input, without solving - **--interactive** arg read the input a character at a time, as needed when driving stp interactively over a pipe. Off reads in blocks, which is faster. Default: on when reading from stdin, off when reading from a file. SMT-LIB2 only. - **-g** \[ **--max-num-confl** \] arg (=-1) Number of conflicts after which the SAT solver gives up. **-1** means never, 0 means give up without searching. - **-k** \[ **--max-time** \] arg (=-1) Number of seconds after which the SAT solver gives up. The budget is for the whole query, not for each call into the SAT solver. **-1** means never, 0 means give up without searching. - **-d** \[ **--check-sanity** \] construct counterexample and check it ### Hidden options: - **--file** arg input file ## SEE ALSO The full documentation for **stp** is maintained as a Texinfo manual. If the **info** and **stp** programs are properly installed at your site, the command - **info stp** should give you access to the complete manual.