** 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 () Int 0) [GOOD] (define-fun s5 () Int 1) [GOOD] (define-fun s81 () Int 10) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (Seq Int)) ; tracks user variable "ints" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- [GOOD] (define-fun s1 () Int (seq.len s0)) [GOOD] (define-fun s3 () Bool (= s1 s2)) [GOOD] (define-fun s4 () Int (seq.nth s0 s2)) [GOOD] (define-fun s6 () Int (- s1 s5)) [GOOD] (define-fun s7 () (Seq Int) (seq.extract s0 s5 s6)) [GOOD] (define-fun s8 () Int (seq.len s7)) [GOOD] (define-fun s9 () Bool (= s2 s8)) [GOOD] (define-fun s10 () Int (seq.nth s7 s2)) [GOOD] (define-fun s11 () Int (- s8 s5)) [GOOD] (define-fun s12 () (Seq Int) (seq.extract s7 s5 s11)) [GOOD] (define-fun s13 () Int (seq.len s12)) [GOOD] (define-fun s14 () Bool (= s2 s13)) [GOOD] (define-fun s15 () Int (seq.nth s12 s2)) [GOOD] (define-fun s16 () Int (- s13 s5)) [GOOD] (define-fun s17 () (Seq Int) (seq.extract s12 s5 s16)) [GOOD] (define-fun s18 () Int (seq.len s17)) [GOOD] (define-fun s19 () Bool (= s2 s18)) [GOOD] (define-fun s20 () Int (seq.nth s17 s2)) [GOOD] (define-fun s21 () Int (- s18 s5)) [GOOD] (define-fun s22 () (Seq Int) (seq.extract s17 s5 s21)) [GOOD] (define-fun s23 () Int (seq.len s22)) [GOOD] (define-fun s24 () Bool (= s2 s23)) [GOOD] (define-fun s25 () Int (seq.nth s22 s2)) [GOOD] (define-fun s26 () Int (- s23 s5)) [GOOD] (define-fun s27 () (Seq Int) (seq.extract s22 s5 s26)) [GOOD] (define-fun s28 () Int (seq.len s27)) [GOOD] (define-fun s29 () Bool (= s2 s28)) [GOOD] (define-fun s30 () Int (seq.nth s27 s2)) [GOOD] (define-fun s31 () Int (- s28 s5)) [GOOD] (define-fun s32 () (Seq Int) (seq.extract s27 s5 s31)) [GOOD] (define-fun s33 () Int (seq.len s32)) [GOOD] (define-fun s34 () Bool (= s2 s33)) [GOOD] (define-fun s35 () Int (seq.nth s32 s2)) [GOOD] (define-fun s36 () Int (- s33 s5)) [GOOD] (define-fun s37 () (Seq Int) (seq.extract s32 s5 s36)) [GOOD] (define-fun s38 () Int (seq.len s37)) [GOOD] (define-fun s39 () Bool (= s2 s38)) [GOOD] (define-fun s40 () Int (seq.nth s37 s2)) [GOOD] (define-fun s41 () Int (- s38 s5)) [GOOD] (define-fun s42 () (Seq Int) (seq.extract s37 s5 s41)) [GOOD] (define-fun s43 () Int (seq.len s42)) [GOOD] (define-fun s44 () Bool (= s2 s43)) [GOOD] (define-fun s45 () Int (seq.nth s42 s2)) [GOOD] (define-fun s46 () Int (- s43 s5)) [GOOD] (define-fun s47 () (Seq Int) (seq.extract s42 s5 s46)) [GOOD] (define-fun s48 () Int (seq.len s47)) [GOOD] (define-fun s49 () Bool (= s2 s48)) [GOOD] (define-fun s50 () Int (seq.nth s47 s2)) [GOOD] (define-fun s51 () Bool (<= s50 s2)) [GOOD] (define-fun s52 () Int (ite s51 s2 s50)) [GOOD] (define-fun s53 () Int (ite s49 s2 s52)) [GOOD] (define-fun s54 () Bool (<= s45 s53)) [GOOD] (define-fun s55 () Int (ite s54 s53 s45)) [GOOD] (define-fun s56 () Int (ite s44 s2 s55)) [GOOD] (define-fun s57 () Bool (<= s40 s56)) [GOOD] (define-fun s58 () Int (ite s57 s56 s40)) [GOOD] (define-fun s59 () Int (ite s39 s2 s58)) [GOOD] (define-fun s60 () Bool (<= s35 s59)) [GOOD] (define-fun s61 () Int (ite s60 s59 s35)) [GOOD] (define-fun s62 () Int (ite s34 s2 s61)) [GOOD] (define-fun s63 () Bool (<= s30 s62)) [GOOD] (define-fun s64 () Int (ite s63 s62 s30)) [GOOD] (define-fun s65 () Int (ite s29 s2 s64)) [GOOD] (define-fun s66 () Bool (<= s25 s65)) [GOOD] (define-fun s67 () Int (ite s66 s65 s25)) [GOOD] (define-fun s68 () Int (ite s24 s2 s67)) [GOOD] (define-fun s69 () Bool (<= s20 s68)) [GOOD] (define-fun s70 () Int (ite s69 s68 s20)) [GOOD] (define-fun s71 () Int (ite s19 s2 s70)) [GOOD] (define-fun s72 () Bool (<= s15 s71)) [GOOD] (define-fun s73 () Int (ite s72 s71 s15)) [GOOD] (define-fun s74 () Int (ite s14 s2 s73)) [GOOD] (define-fun s75 () Bool (<= s10 s74)) [GOOD] (define-fun s76 () Int (ite s75 s74 s10)) [GOOD] (define-fun s77 () Int (ite s9 s2 s76)) [GOOD] (define-fun s78 () Bool (<= s4 s77)) [GOOD] (define-fun s79 () Int (ite s78 s77 s4)) [GOOD] (define-fun s80 () Int (ite s3 s2 s79)) [GOOD] (define-fun s82 () Bool (> s80 s81)) [GOOD] (define-fun s83 () Bool (not s82)) [GOOD] (define-fun s84 () Bool (< s50 s2)) [GOOD] (define-fun s85 () Bool (> s50 s81)) [GOOD] (define-fun s86 () Bool (or s84 s85)) [GOOD] (define-fun s87 () Bool (not s49)) [GOOD] (define-fun s88 () Bool (and s86 s87)) [GOOD] (define-fun s89 () Bool (< s45 s2)) [GOOD] (define-fun s90 () Bool (> s45 s81)) [GOOD] (define-fun s91 () Bool (or s89 s90)) [GOOD] (define-fun s92 () Bool (or s88 s91)) [GOOD] (define-fun s93 () Bool (not s44)) [GOOD] (define-fun s94 () Bool (and s92 s93)) [GOOD] (define-fun s95 () Bool (< s40 s2)) [GOOD] (define-fun s96 () Bool (> s40 s81)) [GOOD] (define-fun s97 () Bool (or s95 s96)) [GOOD] (define-fun s98 () Bool (or s94 s97)) [GOOD] (define-fun s99 () Bool (not s39)) [GOOD] (define-fun s100 () Bool (and s98 s99)) [GOOD] (define-fun s101 () Bool (< s35 s2)) [GOOD] (define-fun s102 () Bool (> s35 s81)) [GOOD] (define-fun s103 () Bool (or s101 s102)) [GOOD] (define-fun s104 () Bool (or s100 s103)) [GOOD] (define-fun s105 () Bool (not s34)) [GOOD] (define-fun s106 () Bool (and s104 s105)) [GOOD] (define-fun s107 () Bool (< s30 s2)) [GOOD] (define-fun s108 () Bool (> s30 s81)) [GOOD] (define-fun s109 () Bool (or s107 s108)) [GOOD] (define-fun s110 () Bool (or s106 s109)) [GOOD] (define-fun s111 () Bool (not s29)) [GOOD] (define-fun s112 () Bool (and s110 s111)) [GOOD] (define-fun s113 () Bool (< s25 s2)) [GOOD] (define-fun s114 () Bool (> s25 s81)) [GOOD] (define-fun s115 () Bool (or s113 s114)) [GOOD] (define-fun s116 () Bool (or s112 s115)) [GOOD] (define-fun s117 () Bool (not s24)) [GOOD] (define-fun s118 () Bool (and s116 s117)) [GOOD] (define-fun s119 () Bool (< s20 s2)) [GOOD] (define-fun s120 () Bool (> s20 s81)) [GOOD] (define-fun s121 () Bool (or s119 s120)) [GOOD] (define-fun s122 () Bool (or s118 s121)) [GOOD] (define-fun s123 () Bool (not s19)) [GOOD] (define-fun s124 () Bool (and s122 s123)) [GOOD] (define-fun s125 () Bool (< s15 s2)) [GOOD] (define-fun s126 () Bool (> s15 s81)) [GOOD] (define-fun s127 () Bool (or s125 s126)) [GOOD] (define-fun s128 () Bool (or s124 s127)) [GOOD] (define-fun s129 () Bool (not s14)) [GOOD] (define-fun s130 () Bool (and s128 s129)) [GOOD] (define-fun s131 () Bool (< s10 s2)) [GOOD] (define-fun s132 () Bool (> s10 s81)) [GOOD] (define-fun s133 () Bool (or s131 s132)) [GOOD] (define-fun s134 () Bool (or s130 s133)) [GOOD] (define-fun s135 () Bool (not s9)) [GOOD] (define-fun s136 () Bool (and s134 s135)) [GOOD] (define-fun s137 () Bool (< s4 s2)) [GOOD] (define-fun s138 () Bool (> s4 s81)) [GOOD] (define-fun s139 () Bool (or s137 s138)) [GOOD] (define-fun s140 () Bool (or s136 s139)) [GOOD] (define-fun s141 () Bool (not s3)) [GOOD] (define-fun s142 () Bool (and s140 s141)) [GOOD] (define-fun s143 () Bool (or s83 s142)) [GOOD] (assert s143) [SEND] (check-sat) [RECV] sat *** Solver : Z3 *** Exit code: ExitSuccess