sbv-14.0: SBVTestSuite/GoldFiles/lambda07.gold
[MEASURE] Verifying termination measures for: sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer]), sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer]), sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_b97075844e @(SBV (Integer,[Integer]) -> SBV Integer), sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)
[MEASURE] Checking: sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])
[MEASURE] sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer]): not in a multi-member cycle, skipping mutual check
[MEASURE] Passed (terminating): sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])
[MEASURE] Checking: sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])
[MEASURE] sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer]): barified = "|sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])|"
[MEASURE] sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer]): Uninterpreted ops in DAG: [("|sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)|",1),("|sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])|",1)]
[MEASURE] sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer]): recursive calls found = 1
[MEASURE] sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer]): trying length arg1
[MEASURE] replayDAG {sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])}: replaying 11 node(s)
** 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 s1 () Int 0)
[GOOD] (define-fun s2 () Int 1)
[GOOD] (define-fun s3 () (Seq Int) (as seq.empty (Seq Int)))
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Seq (Seq Int))) ; tracks user variable "arg"
[GOOD] (declare-fun s8 () Int) ; tracks user variable "__internal_sbv_s8"
[GOOD] (declare-fun s12 () (Seq Int)) ; tracks user variable "__internal_sbv_s12"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s4 () Int (seq.len s0))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] (define-fun s6 () (Seq Int) (seq.nth s0 s1))
[GOOD] (define-fun s7 () (SBVTuple2 Int (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s1 s6))
[GOOD] (define-fun s9 () (Seq Int) (seq.unit s8))
[GOOD] (define-fun s10 () Int (- s4 s2))
[GOOD] (define-fun s11 () (Seq (Seq Int)) (seq.extract s0 s2 s10))
[GOOD] (define-fun s13 () (Seq Int) (seq.++ s9 s12))
[GOOD] (define-fun s14 () (Seq Int) (ite s5 s3 s13))
[GOOD] (define-fun s15 () Bool (>= s4 s1))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s15))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess
[MEASURE] replayDAG {sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])}: replaying 11 node(s)
** 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 s1 () Int 0)
[GOOD] (define-fun s2 () Int 1)
[GOOD] (define-fun s3 () (Seq Int) (as seq.empty (Seq Int)))
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Seq (Seq Int))) ; tracks user variable "arg"
[GOOD] (declare-fun s8 () Int) ; tracks user variable "__internal_sbv_s8"
[GOOD] (declare-fun s12 () (Seq Int)) ; tracks user variable "__internal_sbv_s12"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s4 () Int (seq.len s0))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] (define-fun s6 () (Seq Int) (seq.nth s0 s1))
[GOOD] (define-fun s7 () (SBVTuple2 Int (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s1 s6))
[GOOD] (define-fun s9 () (Seq Int) (seq.unit s8))
[GOOD] (define-fun s10 () Int (- s4 s2))
[GOOD] (define-fun s11 () (Seq (Seq Int)) (seq.extract s0 s2 s10))
[GOOD] (define-fun s13 () (Seq Int) (seq.++ s9 s12))
[GOOD] (define-fun s14 () (Seq Int) (ite s5 s3 s13))
[GOOD] (define-fun s15 () Int (seq.len s11))
[GOOD] (define-fun s16 () Bool (not s5))
[GOOD] (define-fun s17 () Bool (> s4 s15))
[GOOD] (define-fun s18 () Bool (=> s16 s17))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s18))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess
[MEASURE] sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer]): length arg1 -> OK
[MEASURE] Passed (terminating): sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])
[MEASURE] Checking: sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_b97075844e @(SBV (Integer,[Integer]) -> SBV Integer)
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_b97075844e @(SBV (Integer,[Integer]) -> SBV Integer): not in a multi-member cycle, skipping mutual check
[MEASURE] Passed (terminating): sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_b97075844e @(SBV (Integer,[Integer]) -> SBV Integer)
[MEASURE] Checking: sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): barified = "|sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)|"
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): Uninterpreted ops in DAG: [("|sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)|",1)]
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): recursive calls found = 1
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying abs arg1._1
[MEASURE] replayDAG {sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)}: replaying 11 node(s)
** 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 s1 () Int 0)
[GOOD] (define-fun s2 () Int 1)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (SBVTuple2 Int (Seq Int))) ; tracks user variable "arg"
[GOOD] (declare-fun s11 () Int) ; tracks user variable "__internal_sbv_s11"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s3 () (Seq Int) (proj_2_SBVTuple2 s0))
[GOOD] (define-fun s4 () Int (seq.len s3))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] (define-fun s6 () Int (proj_1_SBVTuple2 s0))
[GOOD] (define-fun s7 () Int (seq.nth s3 s1))
[GOOD] (define-fun s8 () Int (- s4 s2))
[GOOD] (define-fun s9 () (Seq Int) (seq.extract s3 s2 s8))
[GOOD] (define-fun s10 () (SBVTuple2 Int (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s6 s9))
[GOOD] (define-fun s12 () Int (+ s7 s11))
[GOOD] (define-fun s13 () Int (ite s5 s6 s12))
[GOOD] (define-fun s14 () Int (abs s6))
[GOOD] (define-fun s15 () Bool (>= s14 s1))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s15))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess
[MEASURE] replayDAG {sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)}: replaying 11 node(s)
** 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 s1 () Int 0)
[GOOD] (define-fun s2 () Int 1)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (SBVTuple2 Int (Seq Int))) ; tracks user variable "arg"
[GOOD] (declare-fun s11 () Int) ; tracks user variable "__internal_sbv_s11"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s3 () (Seq Int) (proj_2_SBVTuple2 s0))
[GOOD] (define-fun s4 () Int (seq.len s3))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] (define-fun s6 () Int (proj_1_SBVTuple2 s0))
[GOOD] (define-fun s7 () Int (seq.nth s3 s1))
[GOOD] (define-fun s8 () Int (- s4 s2))
[GOOD] (define-fun s9 () (Seq Int) (seq.extract s3 s2 s8))
[GOOD] (define-fun s10 () (SBVTuple2 Int (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s6 s9))
[GOOD] (define-fun s12 () Int (+ s7 s11))
[GOOD] (define-fun s13 () Int (ite s5 s6 s12))
[GOOD] (define-fun s14 () Int (abs s6))
[GOOD] (define-fun s15 () Int (proj_1_SBVTuple2 s10))
[GOOD] (define-fun s16 () Int (abs s15))
[GOOD] (define-fun s17 () Bool (not s5))
[GOOD] (define-fun s18 () Bool (> s14 s16))
[GOOD] (define-fun s19 () Bool (=> s17 s18))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s19))
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s14))
[RECV] ((s14 0))
[SEND] (get-value (s16))
[RECV] ((s16 0))
[SEND] (get-value (s0))
[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 2))))
[SEND] (get-value (s11))
[RECV] ((s11 0))
*** Solver : Z3
*** Exit code: ExitSuccess
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): abs arg1._1 failed strict decrease: Falsifiable. Counter-example:
arg = (0,[2]) :: (Integer, [Integer])
before = 0 :: Integer
then = 0 :: Integer
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying next candidate..
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying length arg1._2
[MEASURE] replayDAG {sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)}: replaying 11 node(s)
** 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 s1 () Int 0)
[GOOD] (define-fun s2 () Int 1)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (SBVTuple2 Int (Seq Int))) ; tracks user variable "arg"
[GOOD] (declare-fun s11 () Int) ; tracks user variable "__internal_sbv_s11"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s3 () (Seq Int) (proj_2_SBVTuple2 s0))
[GOOD] (define-fun s4 () Int (seq.len s3))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] (define-fun s6 () Int (proj_1_SBVTuple2 s0))
[GOOD] (define-fun s7 () Int (seq.nth s3 s1))
[GOOD] (define-fun s8 () Int (- s4 s2))
[GOOD] (define-fun s9 () (Seq Int) (seq.extract s3 s2 s8))
[GOOD] (define-fun s10 () (SBVTuple2 Int (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s6 s9))
[GOOD] (define-fun s12 () Int (+ s7 s11))
[GOOD] (define-fun s13 () Int (ite s5 s6 s12))
[GOOD] (define-fun s14 () Bool (>= s4 s1))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s14))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess
[MEASURE] replayDAG {sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)}: replaying 11 node(s)
** 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 s1 () Int 0)
[GOOD] (define-fun s2 () Int 1)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (SBVTuple2 Int (Seq Int))) ; tracks user variable "arg"
[GOOD] (declare-fun s11 () Int) ; tracks user variable "__internal_sbv_s11"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s3 () (Seq Int) (proj_2_SBVTuple2 s0))
[GOOD] (define-fun s4 () Int (seq.len s3))
[GOOD] (define-fun s5 () Bool (= s1 s4))
[GOOD] (define-fun s6 () Int (proj_1_SBVTuple2 s0))
[GOOD] (define-fun s7 () Int (seq.nth s3 s1))
[GOOD] (define-fun s8 () Int (- s4 s2))
[GOOD] (define-fun s9 () (Seq Int) (seq.extract s3 s2 s8))
[GOOD] (define-fun s10 () (SBVTuple2 Int (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s6 s9))
[GOOD] (define-fun s12 () Int (+ s7 s11))
[GOOD] (define-fun s13 () Int (ite s5 s6 s12))
[GOOD] (define-fun s14 () (Seq Int) (proj_2_SBVTuple2 s10))
[GOOD] (define-fun s15 () Int (seq.len s14))
[GOOD] (define-fun s16 () Bool (not s5))
[GOOD] (define-fun s17 () Bool (> s4 s15))
[GOOD] (define-fun s18 () Bool (=> s16 s17))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s18))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess
[MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): length arg1._2 -> OK
[MEASURE] Passed (terminating): sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)
** 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 () Int 0)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Seq (Seq Int)))
[GOOD] (declare-fun s1 () Int)
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; |sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)| :: (SInteger, [SInteger]) -> SInteger [Recursive]
[GOOD] (define-fun-rec |sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)| ((l1_s0 (SBVTuple2 Int (Seq Int)))) 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 Int (Seq Int))) l1_s5 l1_s9)))
(let ((l1_s11 (|sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)| l1_s10)))
(let ((l1_s12 (+ l1_s6 l1_s11)))
(let ((l1_s13 (ite l1_s4 l1_s5 l1_s12)))
l1_s13))))))))))))))
[GOOD] ; |sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_b97075844e @(SBV (Integer,[Integer]) -> SBV Integer)| :: (SInteger, [SInteger]) -> SInteger [Refers to: |sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)|]
[GOOD] (define-fun |sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_b97075844e @(SBV (Integer,[Integer]) -> SBV Integer)| ((s0 (SBVTuple2 Int (Seq Int)))) Int
(let ((s3 0))
(let ((s7 1))
(let ((s1 (proj_2_SBVTuple2 s0)))
(let ((s2 (seq.len s1)))
(let ((s4 (= s2 s3)))
(let ((s5 (proj_1_SBVTuple2 s0)))
(let ((s6 (seq.nth s1 s3)))
(let ((s8 (- s2 s7)))
(let ((s9 (seq.extract s1 s7 s8)))
(let ((s10 ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s5 s9)))
(let ((s11 (|sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)| s10)))
(let ((s12 (+ s6 s11)))
(let ((s13 (ite s4 s5 s12)))
s13))))))))))))))
[GOOD] ; |sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])| :: [[SInteger]] -> [SInteger] [Recursive] [Refers to: |sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)|]
[GOOD] (define-fun-rec |sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])| ((l1_s0 (Seq (Seq Int)))) (Seq Int)
(let ((l1_s2 0))
(let ((l1_s4 (as seq.empty (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_s2 l1_s5)))
(let ((l1_s7 (|sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(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)_1b9bf3f573 @(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] ; --- assignments ---
[GOOD] (define-fun s3 () Bool (= s0 s2))
[GOOD] (define-fun s5 () (Seq Int) (|sbv.map @(SBV [Integer] -> SBV Integer)_1b9bf3f573 @(SBV [[Integer]] -> SBV [Integer])| s0))
[GOOD] (define-fun s6 () (SBVTuple2 Int (Seq Int)) ((as mkSBVTuple2 (SBVTuple2 Int (Seq Int))) s4 s5))
[GOOD] (define-fun s7 () Int (|sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)| s6))
[GOOD] (define-fun s8 () Bool (= s1 s7))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s3)
[GOOD] (assert s8)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s1))
[RECV] ((s1 280))
[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 280))
*** 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 = 280 :: Integer