Your company here, and a link to your site. Click to find out more.

stp - Man Page

Simple Theorem Prover SMT solver


USAGE: stp [options] <input-file>

where input is SMTLIB1/2 or CVC depending on options and file extension

Most important options

-h [ --help ]

print this help


print version number



disable all simplifications

-w [ --switch-word ]

switch off wordlevel solver

-a [ --disable-opt-inc ]

disable potentially size-increasing optimisations


disable constant bit propagation


disable equality propagation

SAT Solver options


use cryptominisat as the solver. Only use CryptoMiniSat 5.0 or above (default).

--threads arg (=1)

Number of threads for cryptominisat


use installed simplifying minisat version as the solver


use installed minisat version as the solver

Refinement options

-r [ --ackermanize ]

eagerly encode array-read axioms (Ackermannistaion)

Printing options

-b [ --print-stpinput ]

print STP input back to cout


print input in CVC format, then exit


print input in SMT-LIB2 format, then exit


print input in SMT-LIB1 format, then exit


print AiSee's graph format, then exit


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


use the SMT-LIB2 format parser


use the CVC format parser

Output options


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


save in ABC's bench format to output.bench

Output options


exit after the CNF has been generated

-g [ --timeout ] arg

Number of conflicts after which the SAT solver gives up. -1 means never (default)

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


February 2024 stp 2.3.3