1** Calling: z3 -nw -in -smt2 2[GOOD] ; Automatically generated by SBV. Do not edit. 3[GOOD] (set-option :print-success true) 4[GOOD] (set-option :global-declarations true) 5[GOOD] (set-option :smtlib2_compliant true) 6[GOOD] (set-option :diagnostic-output-channel "stdout") 7[GOOD] (set-option :produce-models true) 8[GOOD] (set-option :pp.max_depth 4294967295) 9[GOOD] (set-option :pp.min_alias_size 4294967295) 10[GOOD] (set-option :model.inline_def true ) 11[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. 12[GOOD] ; --- uninterpreted sorts --- 13[GOOD] ; --- tuples --- 14[GOOD] ; --- sums --- 15[GOOD] ; --- literal constants --- 16[GOOD] ; --- skolem constants --- 17[GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "a" 18[GOOD] (declare-fun s1 () (Seq Int)) ; tracks user variable "b" 19[GOOD] (declare-fun s2 () (Seq Int)) ; tracks user variable "c" 20[GOOD] ; --- constant tables --- 21[GOOD] ; --- skolemized tables --- 22[GOOD] ; --- arrays --- 23[GOOD] ; --- uninterpreted constants --- 24[GOOD] ; --- user given axioms --- 25[GOOD] ; --- formula --- 26[GOOD] (define-fun s3 () Bool (seq.contains s0 s1)) 27[GOOD] (define-fun s4 () Bool (seq.contains s1 s2)) 28[GOOD] (define-fun s5 () Bool (seq.contains s0 s2)) 29[GOOD] (define-fun s6 () Bool (not s5)) 30[GOOD] (assert s3) 31[GOOD] (assert s4) 32[GOOD] (assert s6) 33[SEND] (check-sat) 34[RECV] unsat 35*** Solver : Z3 36*** Exit code: ExitSuccess 37