** 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 :pp.max_depth 4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[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 0)) (((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] (declare-fun s17 () (_ FloatingPoint 15 113))
[GOOD] (declare-fun s18 () (_ FloatingPoint 15 113))
[GOOD] (assert s3)
[GOOD] (define-fun s19 () (_ BitVec 8) #x01)
[GOOD] (define-fun s20 () Bool (= s4 s19))
[GOOD] (assert s20)
[GOOD] (define-fun s21 () (_ BitVec 16) #x0002)
[GOOD] (define-fun s22 () Bool (= s5 s21))
[GOOD] (assert s22)
[GOOD] (define-fun s23 () (_ BitVec 32) #x00000003)
[GOOD] (define-fun s24 () Bool (= s6 s23))
[GOOD] (assert s24)
[GOOD] (define-fun s25 () (_ BitVec 64) #x0000000000000004)
[GOOD] (define-fun s26 () Bool (= s7 s25))
[GOOD] (assert s26)
[GOOD] (define-fun s27 () (_ BitVec 8) #x05)
[GOOD] (define-fun s28 () Bool (= s8 s27))
[GOOD] (assert s28)
[GOOD] (define-fun s29 () (_ BitVec 16) #x0006)
[GOOD] (define-fun s30 () Bool (= s9 s29))
[GOOD] (assert s30)
[GOOD] (define-fun s31 () (_ BitVec 32) #x00000007)
[GOOD] (define-fun s32 () Bool (= s10 s31))
[GOOD] (assert s32)
[GOOD] (define-fun s33 () (_ BitVec 64) #x0000000000000008)
[GOOD] (define-fun s34 () Bool (= s11 s33))
[GOOD] (assert s34)
[GOOD] (define-fun s35 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0)))
[GOOD] (define-fun s36 () Bool (fp.eq s12 s35))
[GOOD] (assert s36)
[GOOD] (define-fun s37 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) roundNearestTiesToEven (/ 10.0 1.0)))
[GOOD] (define-fun s38 () Bool (fp.eq s13 s37))
[GOOD] (assert s38)
[GOOD] (define-fun s39 () Real (/ 11.0 1.0))
[GOOD] (define-fun s40 () Bool (= s14 s39))
[GOOD] (assert s40)
[GOOD] (define-fun s41 () Int 12)
[GOOD] (define-fun s42 () Bool (= s15 s41))
[GOOD] (assert s42)
[GOOD] (define-fun s43 () BinOp Plus)
[GOOD] (define-fun s44 () Bool (= s16 s43))
[GOOD] (assert s44)
[GOOD] (define-fun s45 () Bool (fp.eq s17 s18))
[GOOD] (assert s45)
[GOOD] (define-fun s46 () Bool (= s17 s18))
[GOOD] (define-fun s47 () Bool (not s46))
[GOOD] (assert s47)
[GOOD] (define-fun s48 () Bool (fp.isPositive s17))
[GOOD] (assert s48)
[GOOD] (declare-fun array_0 () (Array Int Int))
[GOOD] (define-fun array_0_initializer () Bool true) ; no initializiation needed
[GOOD] (declare-fun s49 () Int)
[GOOD] (declare-fun s50 () Bool)
[GOOD] (define-fun s52 () Int 2)
[GOOD] (define-fun s51 () Int (select array_0 s49))
[GOOD] (define-fun s53 () Bool (= s51 s52))
[GOOD] (assert s53)
[GOOD] (define-fun s55 () String (_ char #x61))
[GOOD] (declare-fun vFArray_uninitializedRead (Bool) String)
[GOOD] (assert (forall ((a1 Bool))
                       (let ((result (vFArray_uninitializedRead a1)))
                            (= 1 (str.len result))
                       )))
[GOOD] (define-fun s54 () String (vFArray_uninitializedRead s50))
[GOOD] (define-fun s56 () Bool (= s54 s55))
[GOOD] (assert s56)
[GOOD] (define-fun s57 () Int 42)
[GOOD] (define-fun array_1 () (Array Int Int) ((as const (Array Int Int)) 42))
[GOOD] (define-fun array_1_initializer () Bool true) ; no initializiation needed
[GOOD] (declare-fun s58 () Int)
[GOOD] (declare-fun s59 () String)
[GOOD] (assert (= 1 (str.len s59)))
[GOOD] (define-fun s60 () Int 96)
[GOOD] (define-fun s61 () Int (select array_1 s60))
[GOOD] (define-fun s62 () Bool (= s58 s61))
[GOOD] (assert s62)
[GOOD] (define-fun s63 () String (_ char #x58))
[GOOD] (define-fun s64 () Bool (= s59 s63))
[GOOD] (assert s64)
[GOOD] (define-fun s65 () Int 1)
[GOOD] (define-fun s66 () Bool (= s49 s65))
[GOOD] (assert s66)
[GOOD] (define-fun s67 () Bool (not s50))
[GOOD] (assert s67)
[GOOD] (declare-fun s68 () String)
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def  true      )
[GOOD] (declare-fun s69 () (Seq Int))
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def  true      )
[GOOD] (declare-fun s70 () (Seq (Seq Int)))
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def  true      )
[GOOD] (declare-fun s71 () (Seq (_ BitVec 8)))
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def  true      )
[GOOD] (declare-fun s72 () (Seq (Seq (_ BitVec 16))))
[GOOD] (define-fun s73 () String "hello")
[GOOD] (define-fun s74 () Bool (= s68 s73))
[GOOD] (assert s74)
[GOOD] (define-fun s75 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4)))
[GOOD] (define-fun s76 () Bool (= s69 s75))
[GOOD] (assert s76)
[GOOD] (define-fun s77 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7)))))
[GOOD] (define-fun s78 () Bool (= s70 s77))
[GOOD] (assert s78)
[GOOD] (define-fun s79 () (Seq (_ BitVec 8)) (seq.++ (seq.unit #x01) (seq.unit #x02)))
[GOOD] (define-fun s80 () Bool (= s71 s79))
[GOOD] (assert s80)
[GOOD] (define-fun s81 () (Seq (Seq (_ BitVec 16))) (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006)))))
[GOOD] (define-fun s82 () Bool (= s72 s81))
[GOOD] (assert s82)
[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)))
[GOOD] (set-option :pp.decimal false)
[SEND] (get-value (s14))
[RECV] ((s14 11.0))
[GOOD] (set-option :pp.decimal true)
[GOOD] (set-option :pp.decimal_precision 16)
[SEND] (get-value (s14))
[RECV] ((s14 11.0))
[SEND] (get-value (s15))
[RECV] ((s15 12))
[SEND] (get-value (s16))
[RECV] ((s16 Plus))
[SEND] (get-value (s49))
[RECV] ((s49 1))
[SEND] (get-value (s50))
[RECV] ((s50 false))
[SEND] (get-value (s58))
[RECV] ((s58 42))
[SEND] (get-value (s59))
[RECV] ((s59 "X"))
[SEND] (get-value (s68))
[RECV] ((s68 "hello"))
[SEND] (get-value (s69))
[RECV] ((s69 (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4))))
[SEND] (get-value (s70))
[RECV] ((s70 (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
               (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7))))))
[SEND] (get-value (s71))
[RECV] ((s71 (seq.++ (seq.unit #x01) (seq.unit #x02))))
[SEND] (get-value (s72))
[RECV] ((s72 (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003)))
               (seq.unit (as seq.empty (Seq (_ BitVec 16))))
               (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006))))))
[SEND] (get-value (s17))
[RECV] ((s17 (_ +zero 15 113)))
[SEND] (get-value (s18))
[RECV] ((s18 (_ -zero 15 113)))
*** 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
  i1       =                    1 :: Integer
  i2       =                False :: Bool
  mustBe42 =                   42 :: Integer
  mustBeX  =                  'X' :: Char
  vString  =              "hello" :: String
  vList1   =            [1,2,3,4] :: [Integer]
  vList2   =  [[1,2,3],[4,5,6,7]] :: [[Integer]]
  vList3   =                [1,2] :: [Word8]
  vList4   = [[1,2,3],[],[4,5,6]] :: [[Word16]]
  vQuad    =                  0.0 :: FloatingPoint 15 113
  wQuad    =                 -0.0 :: FloatingPoint 15 113
DONE!