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