** 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 s3 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) [GOOD] (define-fun s5 () (Seq Int) (seq.++ (seq.unit 6) (seq.unit 7) (seq.unit 8))) [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Seq Int)) [GOOD] (declare-fun s1 () (Seq Int)) [GOOD] (declare-fun s2 () (Seq (Seq Int))) [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user defined functions --- [GOOD] ; |sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer])| :: (SInteger, [SInteger]) -> [SInteger] [Recursive] [GOOD] (define-fun-rec |sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer])| ((l1_s0 (SBVTuple2 Int (Seq Int)))) (Seq Int) (let ((l1_s3 0)) (let ((l1_s5 (as seq.empty (Seq Int)))) (let ((l1_s10 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_s6 (proj_1_SBVTuple2 l1_s0))) (let ((l1_s7 (seq.nth l1_s1 l1_s3))) (let ((l1_s8 (+ l1_s6 l1_s7))) (let ((l1_s9 (seq.unit l1_s8))) (let ((l1_s11 (- l1_s2 l1_s10))) (let ((l1_s12 (seq.extract l1_s1 l1_s10 l1_s11))) (let ((l1_s13 ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) l1_s6 l1_s12))) (let ((l1_s14 (|sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer])| l1_s13))) (let ((l1_s15 (seq.++ l1_s9 l1_s14))) (let ((l1_s16 (ite l1_s4 l1_s5 l1_s15))) l1_s16))))))))))))))))) [GOOD] ; |sbv.map @(SBV Integer -> SBV [Integer])_8a19cac1b3 @(SBV [Integer] -> SBV [[Integer]])| :: [SInteger] -> [[SInteger]] [Recursive] [Refers to: |sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer])|] [GOOD] (define-fun-rec |sbv.map @(SBV Integer -> SBV [Integer])_8a19cac1b3 @(SBV [Integer] -> SBV [[Integer]])| ((l1_s0 (Seq Int))) (Seq (Seq Int)) (let ((l1_s2 0)) (let ((l1_s4 (as seq.empty (Seq (Seq Int))))) (let ((l1_s9 1)) (let ((l1_s1 (seq.len l1_s0))) (let ((l1_s3 (= l1_s1 l1_s2))) (let ((l1_s5 (seq.nth l1_s0 l1_s2))) (let ((l1_s6 ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) l1_s5 s0))) (let ((l1_s7 (|sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer])| l1_s6))) (let ((l1_s8 (seq.unit l1_s7))) (let ((l1_s10 (- l1_s1 l1_s9))) (let ((l1_s11 (seq.extract l1_s0 l1_s9 l1_s10))) (let ((l1_s12 (|sbv.map @(SBV Integer -> SBV [Integer])_8a19cac1b3 @(SBV [Integer] -> SBV [[Integer]])| l1_s11))) (let ((l1_s13 (seq.++ l1_s8 l1_s12))) (let ((l1_s14 (ite l1_s3 l1_s4 l1_s13))) l1_s14))))))))))))))) [GOOD] ; |sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_3339bda50c @(SBV (Integer,[Integer]) -> SBV [Integer])| :: (SInteger, [SInteger]) -> [SInteger] [Refers to: |sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer])|] [GOOD] (define-fun |sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_3339bda50c @(SBV (Integer,[Integer]) -> SBV [Integer])| ((s0 (SBVTuple2 Int (Seq Int)))) (Seq Int) (let ((s3 0)) (let ((s5 (as seq.empty (Seq Int)))) (let ((s10 1)) (let ((s1 (proj_2_SBVTuple2 s0))) (let ((s2 (seq.len s1))) (let ((s4 (= s2 s3))) (let ((s6 (proj_1_SBVTuple2 s0))) (let ((s7 (seq.nth s1 s3))) (let ((s8 (+ s6 s7))) (let ((s9 (seq.unit s8))) (let ((s11 (- s2 s10))) (let ((s12 (seq.extract s1 s10 s11))) (let ((s13 ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s6 s12))) (let ((s14 (|sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer])| s13))) (let ((s15 (seq.++ s9 s14))) (let ((s16 (ite s4 s5 s15))) s16))))))))))))))))) [GOOD] ; --- assignments --- [GOOD] (define-fun s4 () Bool (= s0 s3)) [GOOD] (define-fun s6 () Bool (= s1 s5)) [GOOD] (define-fun s7 () (Seq (Seq Int)) (|sbv.map @(SBV Integer -> SBV [Integer])_8a19cac1b3 @(SBV [Integer] -> SBV [[Integer]])| s1)) [GOOD] (define-fun s8 () Bool (= s2 s7)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- [GOOD] (assert s4) [GOOD] (assert s6) [GOOD] (assert s8) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s2)) [RECV] ((s2 (seq.++ (seq.unit (seq.++ (seq.unit 7) (seq.unit 8) (seq.unit 9))) (seq.unit (seq.++ (seq.unit 8) (seq.unit 9) (seq.unit 10))) (seq.unit (seq.++ (seq.unit 9) (seq.unit 10) (seq.unit 11)))))) [SEND] (get-value (s0)) [RECV] ((s0 (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))) [SEND] (get-value (s1)) [RECV] ((s1 (seq.++ (seq.unit 6) (seq.unit 7) (seq.unit 8)))) [SEND] (get-value (s2)) [RECV] ((s2 (seq.++ (seq.unit (seq.++ (seq.unit 7) (seq.unit 8) (seq.unit 9))) (seq.unit (seq.++ (seq.unit 8) (seq.unit 9) (seq.unit 10))) (seq.unit (seq.++ (seq.unit 9) (seq.unit 10) (seq.unit 11)))))) *** Solver : Z3 *** Exit code: ExitSuccess RESULT: s0 = [1,2,3] :: [Integer] s1 = [6,7,8] :: [Integer] s2 = [[7,8,9],[8,9,10],[9,10,11]] :: [[Integer]]