Boolean logic in SMT-LIB: declare-const, assert and check-sat with Z3

SMT-LIB is the input language of solvers such as Z3: you declare Boolean constants, assert formulas in prefix notation and ask check-sat. The listing below is the engine's SMT-LIB export of the entry rule, which phrases each check as a question a solver can answer.

Logic	SMT-LIB	Note
`NOT A`	`(not a)`
`A AND B`	`(and a b)`	n-ary: `(and a b c)`
`A OR B`	`(or a b)`	n-ary
`A XOR B`	`(xor a b)`	n-ary; a chain is parity
`A -> B`	`(=> a b)`	right-associative when chained
`A <-> B`	`(= a b)`	`=` on Bool is the biconditional
`TRUE`, `FALSE`	`true`, `false`	lower case

A Boolean input is (declare-const member Bool); the operators are prefix and n-ary, (and a b c), (or a b), (not a), (xor a b), implication (=> a b) and the biconditional (= a b), since = on two Booleans is equality of truth values. (assert φ) adds a constraint, (check-sat) answers sat, unsat or unknown, and (get-model) after sat prints a satisfying assignment, which is a witness in this reference's vocabulary.

The questions are asked by negation. To show that a formula is a tautology, assert its negation and expect unsat: no assignment makes the negation true. To show two formulas equivalent, assert (not (= f g)) and expect unsat; a sat answer comes with a model, which is the row on which they differ. The export does exactly this, one push/pop block per question, so assertions never accumulate across questions, and it states what each answer means.

The header names the profile, the SMT-LIB 2.6 Boolean subset with logic QF_UF, and the Z3 version the export was tested with. It also says what an unsat is: solver-checked, not an independently checked proof certificate, and unknown settles nothing. That is the same honesty rule as the rest of the engine, whose own checks are exhaustive up to a limit and solver cross-checked where both apply; the glossary explains the exhaustive check and the SAT solver.

The entry rule, as the engine exports it

allow_entry := (member OR invited) AND NOT banned

; Tangibool SMT-LIB export (tangibool.smtlib/1)
; Profile: SMT-LIB 2.6 Boolean subset (QF_UF): Bool constants, define-fun, let, push/pop, assert, check-sat, echo.
; Tested with Z3 5.1.0 (z3-solver 5.2.0, WebAssembly build).
; Model: not stated
; Source revision: reference
; Interpretation status: not stated
; Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
; Logic digest: f0daa82174670c788f59eb058d07f7601cd0ace4ed94d61a747cc26c41fd4e0d
; Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
; Mode: decision
;
; Reading results: each query block states what sat and unsat mean for its question. A sat
; answer comes with a witness or counterexample (ask for it with (get-model) after sat only);
; unsat settles that scoped query and is solver-checked, not an independently checked proof
; certificate; unknown settles nothing. Blocks are scoped with push/pop, so assertions never
; accumulate across questions. This checks the supplied model, not whether it is a complete,
; legal, or safe statement of a real-world rule.
;
; Symbols (stable ID: name -> symbol):
;   v_79df34978043: member -> in_member
;   v_8afde06f51e3: invited -> in_invited
;   v_60b2536f5dc8: banned -> in_banned
;   f_ae8686d89791: allow_entry -> out_allow_entry

(set-option :produce-models true)
(set-info :smt-lib-version 2.6)
(set-logic QF_UF)

; ---- Inputs (declared order)
(declare-const in_member Bool) ; member
(declare-const in_invited Bool) ; invited
(declare-const in_banned Bool) ; banned

; ---- Outputs (dependencies first)
; output allow_entry (stable ID f_ae8686d89791): (member OR invited) AND NOT banned
(define-fun out_allow_entry () Bool (and (or in_member in_invited) (not in_banned)))

; ---- Assumptions (the scope K; never folded into an output)
; K: conjunction of the enabled, confirmed assumptions (true when there are none)
(define-fun K () Bool true)

; ---- Definitions only: nothing is asserted and no check is run.
; Add (assert ...) and (check-sat) inside (push 1) ... (pop 1) to ask a question.

The common slip

Asserting the formula itself and reading sat as “the rule is valid”. sat only says that some assignment makes it true. Validity is unsat of the negation, and the export's blocks are written that way round so the answer cannot be misread.

Questions

What does unknown mean?

That the solver gave up within its limits. It is not a pass and not a fail; the export says so in its header, and the engine reports the same situation as “Not determined”.

Which solver was it tested with?

The header of the generated file names the Z3 version and build it was run against. Other SMT-LIB 2.6 solvers should accept the Boolean subset, but the file does not claim that.

Languages

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.