T16.hs.golden

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