SMT-LIB 2.7 compatibility¶

STP targets the SMT-LIB 2.7 reference, release 2025-02-05 for its supported quantifier-free theories. This is the target of the compatibility work tracked in issue 500. It is not a claim that STP implements every SMT-LIB theory or every feature added in 2.7.

The command-line reader and the API’s EXECUTE and PARSE_ONLY script modes enforce the command protocol. The API’s DECLARE_AND_ASSERT mode also accepts fragments in an existing solver context; it does not require a complete, standalone SMT-LIB script.

Writing a script¶

For portable scripts, place options that control the products of solving before set-logic, as the specification prescribes. STP also accepts them after set-logic, like cvc5 and Bitwuzla. For example:

(set-option :produce-models true)
(set-option :produce-assignments true)
(set-logic QF_BV)
(set-info :smt-lib-version 2.7)
(define-sort Byte () (_ BitVec 8))
(declare-const x Byte)
(assert (! (= x #x2a) :named answer))
(check-sat)
(get-value (x))
(get-assignment)
(exit)

An explicit set-logic precedes declarations, assertions and checks, and may occur only once between resets. If omitted, STP selects ALL when the first such command needs a logic, like the default frontends of cvc5 and Bitwuzla. ALL selects STP’s supported quantifier-free theories together. Array logics enable extensional array equality automatically; UF logics enable uninterpreted functions. See Overview for the accepted logic names and Linear real arithmetic for the linear arithmetic fragment.

A model query requires the relevant option and a current satisfiable context. An assertion, declaration, nonzero push or pop, or reset-assertions ends that context: check again before querying a model. Definitions and zero-level stack operations preserve the model; they add no constraints or unconstrained symbols. reset returns to the initial state, including default options and output channels. reset-assertions preserves options and the logic, and retains declarations only when :global-declarations is true.

Implemented language and protocol features¶

Area	Behavior
Declarations and definitions	`declare-const`, `declare-fun`, `define-const` and nonrecursive `define-fun`; nullary uninterpreted sorts in logics that support them; scoped, parameterized `define-sort` aliases with simultaneous substitution of their parameters.
Terms	Simultaneous `let` bindings, lexical shadowing of user names, sort-qualified identifiers `(as f Sort)`, general attributes and `:named` inline definitions. As a compatibility extension, local binders may also shadow theory names; top-level theory names remain protected. A qualification checks the result sort; it does not convert a value.
Operator attributes	N-ary Core connectives and equality, including Real equality; pairwise `distinct`; right-associative implication; supported bit-vector operators with their associative syntax. The usual minimum arities still apply.
Symbols and strings	Quoted and simple spellings identify the same symbol. Reserved words used as names require quoting, except that the SMT-LIB 2.6 identifier `lambda` remains accepted. Strings escape a double quote by doubling it; backslashes are literal characters.
Attributes and metadata	General attribute values and nested s-expressions are parsed. Unknown term attributes and metadata may be ignored; unknown options report `unsupported`. A `:named` term must be closed and introduces a definition in the current declaration scope.
Model inspection	`get-model`, scalar and array `get-value`, and `get-assignment` for named Boolean terms. Abstract values of uninterpreted sorts are qualified, for example `(as @S!0 S)`, and can be used in `get-value` for the same model.
Other queries	`check-sat-assuming` accepts Boolean terms; `get-unsat-assumptions` and `get-unsat-core` require their production options. Named cores report labels on active assertions. STP always retains assertions, so `get-assertions` works regardless of `:produce-assertions`. `get-info :all-statistics` is available before solving and after context changes. Other information and option queries report the implemented settings.
Random seed	`:random-seed` accepts unsigned 64-bit numerals and is used by every SAT backend. `get-option` reports the selected seed.
Responses and channels	`:print-success` defaults to false. `echo` produces one string response. Regular and diagnostic output channels support `stdout`, `stderr` and append-mode files. Errors produce an `(error "...")` response and end the script, consistent with `:error-behavior immediate-exit`.

Compatibility with other frontends¶

STP accepts common, unambiguous extensions rather than using the SMT-LIB command modes as a strict input validator. The following cases were run against cvc5 1.3.5.dev+main@1689f13331 and Bitwuzla 0.9.1-dev-main@f0f74238. The table describes their default frontends; cvc5’s strict parser was also checked and differs here only by requiring an explicit logic. These comparisons inform compatibility choices; the 2.7 reference remains the language target. In particular, that cvc5 build reports that it uses 2.6 semantics when asked for version 2.7.

Input	cvc5	Bitwuzla	STP
`:produce-models` after `set-logic`, before declarations	Accepts	Accepts	Accepts
No `set-logic`	Accepts	Accepts	Selects `ALL`
Statistics before solving	Accepts	Command unsupported	Accepts
`get-assertions` with `:produce-assertions false`	Accepts	Command unsupported	Accepts
Model query after `define-fun`	Accepts	Accepts	Preserves the model
Model query after `push 0` or `pop 0`	Accepts	Rejects	Preserves the model
A local `let` variable named `and`	Accepts	Accepts	Accepts
`lambda` as an ordinary identifier	Accepts	Accepts	Accepts; quotes it in output
`get-value` after adding a contradictory assertion	Returns the prior model’s value	Rejects	Rejects
Model query without model production enabled	Rejects	Rejects	Rejects

Restrictions needed for a reliable answer remain. Assertions, declarations and nonzero stack changes invalidate the current model. The existing restriction on changing :global-declarations after declarations or assertions prevents changing their scope retroactively. :reason-unknown requires an unknown result, as it does in cvc5; Bitwuzla does not implement get-info.

Malformed option values, incorrect result sorts, malformed let bindings, and non-closed :named terms still produce errors. The two other solvers also reject the first three; cvc5 rejects non-closed named terms. Names beginning with @ or . remain reserved because STP uses them for internal symbols and abstract model values. Local shadowing and the legacy lambda identifier are extensions; portable 2.7 scripts avoid shadowing theory names and quote |lambda|.

Random seed¶

(set-option :random-seed 42) seeds the SAT backend through the same setting as --random-seed=42. The default, 0, leaves the backend’s own default in place. Nonzero seeds make its random choices repeatable for the same input, backend and configuration. Different backends may map the 64-bit seed into smaller ranges; distinct seeds need not produce distinct results. Parallel solving and wall-clock limits can still make runs differ.

For portable scripts, set the seed before set-logic. STP also accepts it after set-logic and between checks. A change preserves the last model or core and rebuilds persistent solving state at the next solve. push, pop and reset-assertions preserve the option; reset restores the startup value, including a seed supplied on the command line. An API script’s seed applies within that parse call; afterwards the caller’s solver options are restored.

Named unsat cores¶

Enable :produce-unsat-cores before the check whose core is needed. Like the other production options, it is accepted before or after set-logic. After an unsat answer, get-unsat-core returns a list of assertion labels:

(set-option :produce-unsat-cores true)
(set-logic QF_BV)
(declare-const p Bool)
(declare-const q Bool)
(assert (! p :named positive))
(assert (! q :named unrelated))
(assert (! (not p) :named negative))
(check-sat)
(get-unsat-core)
; unsat
; (|positive| |negative|)

STP projects its failed-assumption core onto named assertion occurrences. Only an annotation on the whole asserted term contributes a label; naming a nested subterm or using a previously defined name does not label an assertion. Unnamed assertions remain background constraints. An empty core is therefore possible when that background is already unsatisfiable. Origins are retained through assertion-local lowering and conjunction splitting. Repeated formulas and shared conjuncts can be represented by one sufficient originating assertion; their other labels need not appear.

After check-sat-assuming, assumptions also remain background for get-unsat-core. When get-unsat-assumptions is enabled too, both answers project the same engine core: the returned named assertions, unnamed assertions and returned assumptions together are unsatisfiable. Neither query prints the other query’s entries.

Labels follow their assertions through push, pop and reset-assertions, even when :global-declarations true retains the definitions introduced by :named. A new check replaces the previous core, and a context change makes it unavailable until another unsat check.

Cores need not be minimal. Core production engages the assumption solver from the first check where supported. UF applications and whole-array equality retain individual assertion origins through private SAT selectors, including when solving requires theory refinement. This path bypasses UF pre-propagation, whole-stack elimination and DISTINCT symmetry breaking: those passes do not yet preserve dependencies for individual core entries.

With --incremental=off, Real arithmetic, or a standalone DISTINCT-ordering block without UF applications or whole-array equality, the engine still exposes only a coarse core. Those checks return all active assertion labels and, when requested, all user assumptions.

Remaining limits and extensions¶

Global sort parameters and polymorphic function declarations from 2.7 are not implemented. declare-sort-parameter reports unsupported. Parameterized sort aliases are supported, but declare-sort with a positive arity is not.
Quantifiers, higher-order maps and lambda terms, datatypes, pattern matching and recursive definitions are not implemented. Datatype and recursive-definition commands report unsupported; unsupported term syntax is rejected. A declaration that reported unsupported has not introduced a usable symbol.
Int, integer/bit-vector conversions, nonlinear real arithmetic, strings, sequences, sets and other theories outside STP’s supported fragments are not implemented. Selecting ALL does not enable them.
Arrays support Boolean, bit-vector, floating-point, rounding-mode and uninterpreted index and element sorts. Boolean indices have exactly two values, false and true, and Boolean cells retain their Bool sort in terms and models. Real and nested array components are not supported. Arrays are not accepted as uninterpreted function arguments or results.
Proofs are not produced. :produce-proofs reports unsupported when enabled; a query without an enabled production option is an error. Unsupported optional settings such as :reproducible-resource-limit also report unsupported.
Constant arrays, spelled ((as const (Array I E)) value), are an extension used in array model output. fp.to_ieee_bv and some logic combinations are also extensions. Model text containing these forms needs a reader that supports them.
Some older permissive syntax remains accepted, including extra parentheses in term positions. get-value may print a normalized spelling of the queried term. STP is not a strict syntax validator for arbitrary SMT-LIB input.

Unsupported commands and options have a response distinct from an error: unsupported leaves the script running. A malformed command, an invalid command state, an unsupported logic or a rejected term ends the script. These responses should be handled before using later results.

Regression coverage¶

Language and protocol regressions live in tests/query-files/smt2-command-tests, the theory-specific query files, tests/smtlib_protocol.py and the C++ parsing and model tests. The protocol tests check output channels and exit status as well as responses; model tests also replay values in fresh solver contexts. See Testing for running the suites. The coverage is a collection of regression checks, not a certification of full SMT-LIB conformance.