STP(1)

📦
version 2.4.1 · 4 versions
, in arch rolling

💅 STP(1) — like, the whole manual, but make it make sense

okay so you opened the man page for stp and it's giving "User Commands", which basically means "a program you run in your terminal, bestie." It's the Simple Theorem Prover SMT solver, and yes, the name says "simple" but the option list said otherwise 😭. Don't worry tho — I got you. Sit down, grab a strawberry drink 🍓, and let's go through it together.

✨ NAME ✨

stp — the Simple Theorem Prover SMT solver 🧚

🌸 DESCRIPTION 🌸

Here's the whole vibe for how you actually run it:

USAGE: stp [options] <input-file>

...where input is SMTLIB1/2 or CVC, depending on your options and the file extension. So like, the file tells on itself a little bit. iykyk 💅

👑 Most important options (a.k.a. the ones you'll actually touch)

  • -h, --help — prints this help. Your "hello, what is this" button 🫶
  • --version — prints the version number. Receipts, basically.

🎀 Simplifications

These control how much STP tidies up your problem before it starts solving. Genuinely iconic behaviour — the solver lowkey loves a glow-up.

  • --disable-simplifications — turns all the simplifications off. All of them. Like, every last one 💀
  • -w, --switch-word — switches off the wordlevel solver
  • -a, --disable-opt-inc — disables the rewriting simplifier
  • --disable-cbitp — disables constant bit propagation
  • --disable-equality — disables equality propagation
  • --size-reducing-only — size-reducing simplifications only, nothing that could make things bigger
  • --unconstrained-variable-elimination arg (=1) — unconstrained variables are eliminated. (Default 1.)
  • --aig-rewrite-passes arg (=0) — how many iterations of AIG rewriting to perform. (Default 0.)
  • --flattening arg (=0) — enables sharing-aware flattening of >2 arity nodes. (Default 0.)
  • --rewriting arg (=1) — enables sharing-aware rewriting. (Default 1.)
  • --split-extracts arg (=1) — creates new variables for some extracts. (Default 1.)
  • --ite-context-simplifications arg (=0) — uses what's known to be true in an if-then-else node to simplify the true or false branches. (Default 0.)
  • --aig-core-simplification arg (=0) — simplifies the propositional core with AIGs. (Default 0.)
  • --use-intervals arg (=1) — simplifies with interval analysis. (Default 1.)
  • --pure-literals arg (=1) — pure literals get replaced. (Default 1.)
  • --merge-same arg (=0) — uses simple boolean algebra rules to combine conjuncts at the top level. (Default 0.)
  • --bit-blast-simplification arg (=0) — part-way through simplifying, converts to AIGs and looks 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. (Default 0.)
  • --size-reducing-fixed-point-limit arg (=0) — if the number of non-leaf nodes is fewer than this number, runs size-reducing simplifications to a fixed-point. -1 means always. (Default 0.)
  • --simplify-to-constants-only arg (=0) — uses just the simplifications from the potentially size increasing suite that transform nodes to constants. (Default 0.)
  • --difficulty-reversion arg (=1) — undoes size increasing simplifications if they haven't made the problem simpler. (Default 1.)

🔥 SAT Solver options

Pick your solver, bestie. It's giving "choose your fighter" energy.

  • --cryptominisat — uses cryptominisat as the solver. Only use CryptoMiniSat 5.0 or above tho, fr fr.
  • --threads arg (=1) — number of threads for cryptominisat. (Default 1.)
  • --simplifying-minisat — uses the installed simplifying minisat version as the solver
  • --minisat — uses the installed minisat version as the solver
  • --search-bias arg — tunes 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. Main character energy for verification girlies 👑

🦋 Refinement options

  • -r, --ackermanize — eagerly encodes array-read axioms (Ackermannistaion). Yes that's how it's spelled in here, I'm just the messenger 🙈

⭐ Bit-blasting options

  • --bb.div-v1 arg (=1) — unsigned division encoding variant 1. (Default 1.)
  • --bb.div-v2 arg (=1) — unsigned division encoding variant 2. (Default 1.)
  • --bb.div-v3 arg (=0) — unsigned division encoding variant 3. (Default 0.)
  • --bb.add-v1 arg (=1) — addition encoding variant 1. (Default 1.)
  • --bb.add-v2 arg (=1) — addition encoding variant 2. (Default 1.)
  • --bb.vle-v1 arg (=1) — comparison encoding variant 1. (Default 1.)
  • --bb.mult-variant arg (=1) — unsigned multiplication variant. (Default 1.)
  • --bb.mult-v2 arg (=0) — unsigned multiplication variant 2. (Default 0.)
  • --bb.conjoin-constant arg (=0) — when constant-bit propagation detects a constant bit during AIG construction, asserts the AIG node and replaces it, in the AIG, by the constant bit. (Default 0.)

💖 Printing options

So many ways to print things. We love options 💅

  • -b, --print-stpinput — prints STP input back to cout
  • --print-back-CVC — prints input in CVC format, then exits
  • --print-back-SMTLIB2 — prints input in SMT-LIB2 format, then exits
  • --print-back-SMTLIB1 — prints input in SMT-LIB1 format, then exits
  • --print-back-GDL — prints AiSee's graph format, then exits
  • --print-back-dot — prints dotty/neato's graph format, then exits
  • -p, --print-counterex — prints counterexample
  • -y, --print-counterexbin — prints counterexample in binary
  • -q, --print-arrayval — prints arrayval in declared order
  • -s, --print-functionstat — prints function statistics
  • -t, --print-quickstat — prints quick statistics
  • -v, --print-nodes — prints nodes
  • -n, --print-output — print output

🌈 Input options

  • -m, --SMTLIB1 — uses the SMT-LIB1 format parser
  • --SMTLIB2 — uses the SMT-LIB2 format parser
  • --CVC — uses the CVC format parser

💜 Output options

  • --output-CNF — saves the CNF into output_[0..n].cnf.
⚠️ NOTE (read this one, seriously): variables cannot be mapped back, and problems solved by the preprocessing simplifier alone will not generate any CNF, because the SAT solver is never invoked. No solver, no CNF, no cap.
  • --output-bench — saves in ABC's bench format to output.bench

🍓 Output options — yes, again, there's a second section with the same name 😭

We don't make the rules, we just report them.

  • --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. (Default medium.)
  • --exit-after-CNF — exits after the CNF has been generated
  • --parse-only — exits after parsing the input, without solving. Like reading the group chat and not replying 🫶
  • --interactive arg — reads 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. (Default -1.)
  • -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. (Default -1.)
  • -d, --check-sanity — constructs counterexample and checks it. Self-care, but for solver output ✨

🙈 Hidden options

(shhh)

  • --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, this command:

info stp

should give you access to the complete manual. That's the whole manual-manual, bestie 📚

okay that's the page!! go solve something, you're literally gonna slay 💜

sign-off era: this was stp 2.4.1, dated October 2026 — that's the version and date, and I'm putting them here instead of copying the footer line, because we're cute like that 🎀✨

📦 where this page comes from