[SBV] tests/T21.hs:9:1 Proving "f", using Z3.
** Starting symbolic simulation..
** Generated symbolic trace:
True :: Bool
** Translating to SMT-Lib..
** Checking Theoremhood..
** Generated SMTLib program:
; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
; has user-defined sorts, no logic specified.
; --- uninterpreted sorts ---
(declare-sort sbvChar 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T21.hs:9:3
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () sbvChar) ; tracks user variable "c"
(declare-fun s1 () sbvChar) ; tracks user variable "s_1"
(declare-fun s2 () sbvChar) ; tracks user variable "s_2"
(declare-fun s3 () sbvChar) ; tracks user variable "s_3"
(declare-fun s4 () sbvChar) ; tracks user variable "s_4"
(declare-fun s5 () sbvChar) ; tracks user variable "s_5"
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (not s_1))
** Calling: "z3 -nw -in -smt2"
** Z3 output:
unsat
** Done..
[Z3] Q.E.D.