Generated SMT-Lib for the uninterpreted sort example

gistfile1.txt

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
; Has unbounded values (Int/Real) or uninterpreted sorts; no logic specified.
; --- uninterpreted sorts ---
(declare-sort A 0)  ; N.B. Uninterpreted: A.A: not a nullary constructor
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () Int) ; tracks user variable "x1"
(declare-fun s1 () Bool) ; tracks user variable "x2"
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
(declare-fun bool2A (Bool) A)
(declare-fun int2A (Int) A)
(declare-fun prop (A) Bool)
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s2 (int2A s0)))
   (let ((s3 (prop s2)))
   (let ((s4 (bool2A s1)))
   (let ((s5 (prop s4)))
   (let ((s6 (and s3 s5)))
   s6))))))
(check-sat)