T19.hs.golden

[SBV] tests/T19.hs:9:1 Proving "f", using Z3.
** Starting symbolic simulation..
** Generated symbolic trace:
SORTS
  |[Char]|
INPUTS
  s0 :: |[Char]|, aliasing "s"
CONSTANTS
  s_2 = False :: Bool
  s_1 = True :: Bool
TABLES
ARRAYS
UNINTERPRETED CONSTANTS
  [uninterpreted] reverse :: |[Char]| -> |[Char]|
  [uninterpreted] |==| :: |[Char]| -> |[Char]| -> SBool
USER GIVEN CODE SEGMENTS
AXIOMS
DEFINE
  s1 :: |[Char]| = [uninterpreted] reverse s0
  s2 :: |[Char]| = [uninterpreted] reverse s1
  s3 :: SBool = s2 [uninterpreted] |==| s0
CONSTRAINTS
ASSERTIONS
OUTPUTS
  s3
** 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 |[Char]| 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T19.hs:9:3
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () |[Char]|) ; tracks user variable "s"
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
(declare-fun reverse (|[Char]|) |[Char]|)
(declare-fun |==| (|[Char]| |[Char]|) Bool)
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s1 (reverse s0)))
   (let ((s2 (reverse s1)))
   (let ((s3 (|==| s2 s0)))
   (not s3)))))
** Calling: "z3 -nw -in -smt2"
** Sending the following model extraction commands:
(get-value (s0))
** Z3 output:
sat
((s0 |[Char]!val!0|))
** Done..
[Z3] Falsifiable. Counter-example:
  s = |[Char]!val!0| :: |[Char]|
[SBV] Counter-example might be bogus due to uninterpreted constants:
  [<no location info>] ==      :: [Char] -> [Char] -> Bool
  [<no location info>] reverse :: [Char] -> [Char]
[SBV] Failed. (Use option 'IgnoreFailure' to continue.)