Solver Chain
Overview of solver chain and related commandline options
Contents
The solver chain
KLEE has a number of command line options that control the solver chain that
is shared both by the klee
and kleaver
tools.
The solver chain is implemented internally using the decorator design pattern. Thus when a solver query is issued it travels through a nested stack of solvers and may eventually call the underlying SMT solver (core solver).
The reasons for this architecture are:
 Allows transforming the solver query into another form that is hopefully faster for the core solver to solve (e.g. the independence solver).
 Allows querying the core solver to be avoided in some cases (e.g. the counterexample caching solver).
 Allows logging of queries at different stages in the solver chain.
The constructSolverChain()
function is used to create the solver chain.
Core solver
This is the underlying SMT solver. Several solvers are currently supported.
The default is dependent on what solvers were available when KLEE was built.
The solver can be selected using the solverbackend=
option.
MetaSMT
metaSMT: An Embedded Domain Specific Language for SMT link. Use solverbackend=metasmt
.
These are options that only affect the MetaSMT solver.
metasmtbackend=<backend>
This specifies the solver that metaSMT should use. Valid values for <backend>
are stp
(STP), z3
(Z3), and btor
(Boolector). Note that Z3 can also be
used directly through its API via the Z3 core solver.
useconstructhashmetasmt
When set to true (default: true) constructed MetaSMT expressions will be cached (and then cleared) for each constraint to facilitate expression reuse.
STP
STP: Simple Theorem Prover SMT solver link. Use solverbackend=stp
.
These are options that only affect the STP solver.
debugdumpstpqueries
When set to true (default: false) every query that the STP solver receives will be written to standard error in its native format.
ignoresolverfailures
When set to true (default: false) unexpected solver failures in the STP solver will be ignored.
useconstructhash
When set to true (default: true) constructed STP expressions will be cached (and then cleared) for each constraint to facilitate expression reuse.
Z3
Z3: The Z3 Theorem Prover link. Use solverbackend=z3
.
These are options that only affect the Z3 solver.
debugz3dumpqueries=<path>
When set every query that the Z3 solver receives will be logged to the file
at <path>
in the SMTLIBv2 format.
debugz3logapiinteraction=<path>
When set Z3’s C API interaction will be logged to the file at <path>
.
This log can be replayed by the Z3 binary using its log
option.
This option is useful for precisely reproducing KLEE’s interaction with Z3
outside of KLEE.
debugz3validatemodels
When set to true (default: false), Z3 models will be subsituted back into
the Z3 expressions for every query that is satisfiable. This is used to check
that the models that Z3 provides are satisfiable in Z3’s own constraint
language. If a model does not satisfy the constraints information about the
failure is printed to standard error and then an abort()
is called.
Note Z3 models being satisfiable in Z3’s constraint language does not necessarily
imply that the model is satifisable when substituted into KLEE’s own expression
language. This could happen if there was an unintentional semantic mismatch
between Z3’s and KLEE’s expression language. To check that a model satisfies
KLEE’s constraint language use debugassignmentvalidatingsolver
.
debugz3verbosity=<N>
When set, Z3’s verbosity level will be set to level <N>
(default: 0).
This is equivalent to the Z3 binary’s v:<N>
option. This is useful for
observing Z3’s internal behaviour (e.g. what tactic is being applied).
useconstructhashz3
When set to true (default: true) constructed Z3 expressions will be cached (and then cleared) for each query to facilitate expression reuse.
Common core solver options
These are options shared by two or more core solvers.
solveroptimizedivides
This only affects the MetaSMT and STP solvers. When set to true expressions involving division will be optimized (if possible) before being given to the solver.
useforkedsolver
This only affects the MetaSMT and STP solvers. When set to true (default:
true) the solver is created in a seperate process that is forked from the
klee
/kleaver
process. When set to false the solver is created in the
klee
/kleaver
process.
Caching Solvers
These solvers cache previous queries to avoid calling the underlying solver when possible.
Caching solver
This solver caches previous queries and their result to avoid calling the underlying solver in certain situations. The queries are canonicalized to increase the cache hit rate.
This solver can be enabled with the usecache
option.
Counterexample caching solver
This solver caches satisfying assignments to queries (i.e. “counterexamples” to validity) which can be used to avoid calling the underlying solver in certain situations.
This solver can be enabled with the usecexcache
option.
Independence solver
This solver splits a query into disjoint sets of independent constraints and then calls the underlying solver on each set to solve them independently.
This solver can be enabled with the useindependentsolver
option.
Debugging solvers
The remaining solvers are used for debugging.
Assignment validating solver
This solver checks that assignments to satisfiable queries are satisfiable when substituted into the expressions in the query.
This is useful for checking the consistency of KLEE’s constraint language and that of the core solver.
This option can be enabled using the debugassignmentvalidatingsolver
option.
Debug validating solver
This solver is meant for debugging and currently is only useful if building with
assertions is enabled. The solver can be enabled with the debugvalidatesolver
option.
This solver invokes the underlying solver and a separate solver for every query and
then checks that the solvers agree. The separate solver can be set with the
debugcrosscheckcoresolver=
option which takes the same arguments as
solverbackend=
.
This is useful for comparing two completly independent solvers (e.g. STP and Z3) and for checking that invoking the solver chain and a solver directly obtains the same results.
Query logging solver
The query logging solver logs queries at different positions in the chain.
The option to enable this is the usequerylog=
option. The format of the option
is usequerylog=TYPE:FORMAT
, where:

TYPE is either all to log all the queries given to the solver chain. This is before any optimisation (e.g. caching, constraint independence) is performed, or solver to log only the queries passed to the core solver. Note that it is possible that some of the unoptimized queries are never executed or are modified before being executed by KLEE’s underlying solver.

FORMAT is the format in which queries are logged and can be either kquery for the KQuery format, or smt2 for the SMTLIBv2 format.
In addition there are several options that change how these queries are logged.
minquerytimetolog=TIME
(in ms) is used to log only queries that exceed a certain time limit. TIME can be: 0 (default): to log all queries
 <0: a negative value specifies that only queries that timed out should be logged. The timeout value is specified via the
maxsolvertime
option.  >0: only queries that took more that TIME milliseconds should be logged.
logpartialqueriesearly=true
is used to dump the query to the log file before the next part of the solver chain is called. Normally, KLEE prints the query and its solution after it has been solved. But if KLEE crashes inside the solver chain, the suspicious query will not be logged. Enable this option to debug such cases. This option comes with a performance penalty as the log buffer gets always flushed.compressquerylog
is used to compress query log files (default=off)