** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s_2 () Bool false)
[GOOD] (define-fun s_1 () Bool true)
[GOOD] (define-fun s1 () Int 0)
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () Int) ; tracks user variable "a"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s2 () Bool (= s0 s1))
[GOOD] (assert s2)
[GOOD] (declare-fun s3 () Bool)
[GOOD] (declare-fun s4 () (_ BitVec 8))
[GOOD] (declare-fun s5 () (_ BitVec 16))
[GOOD] (declare-fun s6 () (_ BitVec 32))
[GOOD] (declare-fun s7 () (_ BitVec 64))
[GOOD] (declare-fun s8 () (_ BitVec 8))
[GOOD] (declare-fun s9 () (_ BitVec 16))
[GOOD] (declare-fun s10 () (_ BitVec 32))
[GOOD] (declare-fun s11 () (_ BitVec 64))
[GOOD] (declare-fun s12 () (_ FloatingPoint  8 24))
[GOOD] (declare-fun s13 () (_ FloatingPoint 11 53))
[GOOD] (declare-fun s14 () Real)
[GOOD] (declare-fun s15 () Int)
[GOOD] (declare-datatypes () ((BinOp (Plus) (Minus) (Times))))
[GOOD] (define-fun BinOp_constrIndex ((x BinOp)) Int
          (ite (= x Plus) 0 (ite (= x Minus) 1 2))
       )
[GOOD] (declare-fun s16 () BinOp)
[GOOD] (assert s3)
[GOOD] (define-fun s17 () (_ BitVec 8) #x01)
[GOOD] (define-fun s18 () Bool (= s4 s17))
[GOOD] (assert s18)
[GOOD] (define-fun s19 () (_ BitVec 16) #x0002)
[GOOD] (define-fun s20 () Bool (= s5 s19))
[GOOD] (assert s20)
[GOOD] (define-fun s21 () (_ BitVec 32) #x00000003)
[GOOD] (define-fun s22 () Bool (= s6 s21))
[GOOD] (assert s22)
[GOOD] (define-fun s23 () (_ BitVec 64) #x0000000000000004)
[GOOD] (define-fun s24 () Bool (= s7 s23))
[GOOD] (assert s24)
[GOOD] (define-fun s25 () (_ BitVec 8) #x05)
[GOOD] (define-fun s26 () Bool (= s8 s25))
[GOOD] (assert s26)
[GOOD] (define-fun s27 () (_ BitVec 16) #x0006)
[GOOD] (define-fun s28 () Bool (= s9 s27))
[GOOD] (assert s28)
[GOOD] (define-fun s29 () (_ BitVec 32) #x00000007)
[GOOD] (define-fun s30 () Bool (= s10 s29))
[GOOD] (assert s30)
[GOOD] (define-fun s31 () (_ BitVec 64) #x0000000000000008)
[GOOD] (define-fun s32 () Bool (= s11 s31))
[GOOD] (assert s32)
[GOOD] (define-fun s33 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0)))
[GOOD] (define-fun s34 () Bool (fp.eq s12 s33))
[GOOD] (assert s34)
[GOOD] (define-fun s35 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) roundNearestTiesToEven (/ 10.0 1.0)))
[GOOD] (define-fun s36 () Bool (fp.eq s13 s35))
[GOOD] (assert s36)
[GOOD] (define-fun s37 () Real (/ 11.0 1.0))
[GOOD] (define-fun s38 () Bool (= s14 s37))
[GOOD] (assert s38)
[GOOD] (define-fun s39 () Int 12)
[GOOD] (define-fun s40 () Bool (= s15 s39))
[GOOD] (assert s40)
[GOOD] (define-fun s41 () BinOp Plus)
[GOOD] (define-fun s42 () Bool (= s16 s41))
[GOOD] (assert s42)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 0))
[SEND] (get-value (s3))
[RECV] ((s3 true))
[SEND] (get-value (s4))
[RECV] ((s4 #x01))
[SEND] (get-value (s5))
[RECV] ((s5 #x0002))
[SEND] (get-value (s6))
[RECV] ((s6 #x00000003))
[SEND] (get-value (s7))
[RECV] ((s7 #x0000000000000004))
[SEND] (get-value (s8))
[RECV] ((s8 #x05))
[SEND] (get-value (s9))
[RECV] ((s9 #x0006))
[SEND] (get-value (s10))
[RECV] ((s10 #x00000007))
[SEND] (get-value (s11))
[RECV] ((s11 #x0000000000000008))
[SEND] (get-value (s12))
[RECV] ((s12 (fp #b0 #x82 #b00100000000000000000000)))
[SEND] (get-value (s13))
[RECV] ((s13 (fp #b0 #b10000000010 #x4000000000000)))
[SEND] (get-value (s14))
[RECV] ((s14 11.0))
[SEND] (get-value (s15))
[RECV] ((s15 12))
[SEND] (get-value (s16))
[RECV] ((s16 Plus))
*** Solver   : Z3
*** Exit code: ExitSuccess

 FINAL:Satisfiable. Model:
  a        =    0 :: Integer
  vBool    = True :: Bool
  vWord8   =    1 :: Word8
  s5       =    2 :: Word16
  s6       =    3 :: Word32
  vWord64  =    4 :: Word64
  vInt8    =    5 :: Int8
  s9       =    6 :: Int16
  s10      =    7 :: Int32
  vInt64   =    8 :: Int64
  vFloat   =  9.0 :: Float
  s13      = 10.0 :: Double
  s14      = 11.0 :: Real
  vInteger =   12 :: Integer
  vBinOp   = Plus :: BinOp
DONE!