(theory Empty :written_by {Cesare Tinelli} :date {08/04/05} :sorts (U) :definition "This theory has no axioms and a signature consisting of the sort U." :notes "Since SMT-LIB's underlying logic is a logic with equality, this theory in effect corresponds to the so called theory of equality over uninterpreted symbols. That is, a formula over arbitrary sort, function and predicate symbols is satisfiable in Empty iff it is consistent with the properties of equality (reflexivity, symmetry, transitivity, and substitutivity). " )