** 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] ; --- tuples --- [GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) ((mkSBVTuple2 (proj_1_SBVTuple2 T1) (proj_2_SBVTuple2 T2)))))) [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] (define-fun s4 () (Seq Int) (as seq.empty (Seq Int))) [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] ; --- user defined functions --- [GOOD] ; |sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])| :: ([SInteger], [[SInteger]]) -> [SInteger] [Recursive] [GOOD] (define-fun-rec |sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])| ((l1_s0 (SBVTuple2 (Seq Int) (Seq (Seq Int))))) (Seq Int) (let ((l1_s3 0)) (let ((l1_s7 1)) (let ((l1_s1 (proj_2_SBVTuple2 l1_s0))) (let ((l1_s2 (seq.len l1_s1))) (let ((l1_s4 (= l1_s2 l1_s3))) (let ((l1_s5 (proj_1_SBVTuple2 l1_s0))) (let ((l1_s6 (seq.nth l1_s1 l1_s3))) (let ((l1_s8 (- l1_s2 l1_s7))) (let ((l1_s9 (seq.extract l1_s1 l1_s7 l1_s8))) (let ((l1_s10 ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) l1_s5 l1_s9))) (let ((l1_s11 (|sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])| l1_s10))) (let ((l1_s12 (seq.++ l1_s6 l1_s11))) (let ((l1_s13 (ite l1_s4 l1_s5 l1_s12))) l1_s13)))))))))))))) [GOOD] ; --- assignments --- [GOOD] (define-fun s3 () Bool (= s0 s2)) [GOOD] (define-fun s5 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s4 s0)) [GOOD] (define-fun s6 () (Seq Int) (|sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])| s5)) [GOOD] (define-fun s7 () Bool (= s1 s6)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- [GOOD] (assert s3) [GOOD] (assert s7) [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]