** 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-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) [GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] (declare-datatypes ((SBVMaybe 1)) ((par (T) ((nothing_SBVMaybe) (just_SBVMaybe (get_just_SBVMaybe T)))))) [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () Int 2) [GOOD] (define-fun s4 () Int 0) [GOOD] (define-fun s8 () Int 1) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq (SBVMaybe (_ BitVec 8)))) ; tracks user variable "lst" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (seq.len s0)) [GOOD] (define-fun s3 () Bool (= s1 s2)) [GOOD] (define-fun s5 () (SBVMaybe (_ BitVec 8)) (seq.nth s0 s4)) [GOOD] (define-fun s6 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 8)))) s5)) [GOOD] (define-fun s7 () Bool (ite s6 false true)) [GOOD] (define-fun s9 () Int (- s1 s8)) [GOOD] (define-fun s10 () (Seq (SBVMaybe (_ BitVec 8))) (seq.extract s0 s8 s9)) [GOOD] (define-fun s11 () (SBVMaybe (_ BitVec 8)) (seq.nth s10 s4)) [GOOD] (define-fun s12 () Bool ((_ is (nothing_SBVMaybe () (SBVMaybe (_ BitVec 8)))) s11)) [GOOD] (define-fun s13 () Bool (ite s12 true false)) [GOOD] (assert s3) [GOOD] (assert s7) [GOOD] (assert s13) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 (seq.++ (seq.unit (just_SBVMaybe #x00)) (seq.unit nothing_SBVMaybe)))) *** Solver : Z3 *** Exit code: ExitSuccess FINAL OUTPUT: [Just '\NUL',Nothing]