** 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] ; --- literal constants ---
[GOOD] (define-fun s2 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4) (seq.unit 5))) (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7) (seq.unit 8) (seq.unit 9) (seq.unit 10))) (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7) (seq.unit 8) (seq.unit 9) (seq.unit 10) (seq.unit 11) (seq.unit 12) (seq.unit 13) (seq.unit 14) (seq.unit 15) (seq.unit 16) (seq.unit 17) (seq.unit 18) (seq.unit 19) (seq.unit 20)))))
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Seq (Seq Int)))
[GOOD] (declare-fun s1 () (Seq Int))
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- Firstified function definitions
[GOOD] ; Firstified function: concat :: [[SInteger]] -> [SInteger]
[GOOD] (define-fun-rec sbv.concat_712066 ((lst (Seq (Seq Int)))) (Seq Int)
                       (ite (= lst (as seq.empty (Seq (Seq Int))))
                            (as seq.empty (Seq Int))
                            (seq.++ (seq.nth lst 0) (sbv.concat_712066 (seq.extract lst 1 (- (seq.len lst) 1))))))
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s3 () Bool (= s0 s2))
[GOOD] (define-fun s4 () (Seq Int) (sbv.concat_712066 s0))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s3)
[GOOD] (assert s5)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s1))
[RECV] ((s1 (seq.++ (seq.unit 1)
               (seq.unit 2)
               (seq.unit 3)
               (seq.unit 4)
               (seq.unit 5)
               (seq.unit 1)
               (seq.unit 2)
               (seq.unit 3)
               (seq.unit 4)
               (seq.unit 5)
               (seq.unit 6)
               (seq.unit 7)
               (seq.unit 8)
               (seq.unit 9)
               (seq.unit 10)
               (seq.unit 1)
               (seq.unit 2)
               (seq.unit 3)
               (seq.unit 4)
               (seq.unit 5)
               (seq.unit 6)
               (seq.unit 7)
               (seq.unit 8)
               (seq.unit 9)
               (seq.unit 10)
               (seq.unit 11)
               (seq.unit 12)
               (seq.unit 13)
               (seq.unit 14)
               (seq.unit 15)
               (seq.unit 16)
               (seq.unit 17)
               (seq.unit 18)
               (seq.unit 19)
               (seq.unit 20))))
[SEND] (get-value (s0))
[RECV] ((s0 (seq.++ (seq.unit (seq.++ (seq.unit 1)
                                 (seq.unit 2)
                                 (seq.unit 3)
                                 (seq.unit 4)
                                 (seq.unit 5)))
               (seq.unit (seq.++ (seq.unit 1)
                                 (seq.unit 2)
                                 (seq.unit 3)
                                 (seq.unit 4)
                                 (seq.unit 5)
                                 (seq.unit 6)
                                 (seq.unit 7)
                                 (seq.unit 8)
                                 (seq.unit 9)
                                 (seq.unit 10)))
               (seq.unit (seq.++ (seq.unit 1)
                                 (seq.unit 2)
                                 (seq.unit 3)
                                 (seq.unit 4)
                                 (seq.unit 5)
                                 (seq.unit 6)
                                 (seq.unit 7)
                                 (seq.unit 8)
                                 (seq.unit 9)
                                 (seq.unit 10)
                                 (seq.unit 11)
                                 (seq.unit 12)
                                 (seq.unit 13)
                                 (seq.unit 14)
                                 (seq.unit 15)
                                 (seq.unit 16)
                                 (seq.unit 17)
                                 (seq.unit 18)
                                 (seq.unit 19)
                                 (seq.unit 20))))))
[SEND] (get-value (s1))
[RECV] ((s1 (seq.++ (seq.unit 1)
               (seq.unit 2)
               (seq.unit 3)
               (seq.unit 4)
               (seq.unit 5)
               (seq.unit 1)
               (seq.unit 2)
               (seq.unit 3)
               (seq.unit 4)
               (seq.unit 5)
               (seq.unit 6)
               (seq.unit 7)
               (seq.unit 8)
               (seq.unit 9)
               (seq.unit 10)
               (seq.unit 1)
               (seq.unit 2)
               (seq.unit 3)
               (seq.unit 4)
               (seq.unit 5)
               (seq.unit 6)
               (seq.unit 7)
               (seq.unit 8)
               (seq.unit 9)
               (seq.unit 10)
               (seq.unit 11)
               (seq.unit 12)
               (seq.unit 13)
               (seq.unit 14)
               (seq.unit 15)
               (seq.unit 16)
               (seq.unit 17)
               (seq.unit 18)
               (seq.unit 19)
               (seq.unit 20))))
*** Solver   : Z3
*** Exit code: ExitSuccess

RESULT:
  s0 = [[1,2,3,4,5],[1,2,3,4,5,6,7,8,9,10],[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]] :: [[Integer]]
  s1 =       [1,2,3,4,5,1,2,3,4,5,6,7,8,9,10,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20] :: [Integer]