Untersuchungsergebnis.certs Download desIsabelle {Isabelle[99] Haskell[203] Coq[225]}zum Wurzelverzeichnis wechseln
8ec9d30fc9fdbc0ea292e0fdf148a6230c16dbca 2924 0
unsat
((set-logic <null>)
(declare-fun ?v0!15 () Int)
(declare-fun ?v0!14 () Int)
(declare-fun ?v0!13 () Int)
(proof
(let ((?x10076 (b_S_array$ b_T_T_u1$ v_b_P_H_len$)))
(let ((?x22595 (b_S_ptr$ ?x10076 v_b_P_H_arr$)))
(let ((?x24598 (b_S_idx$ ?x22595 v_b_L_H_p_G_0$ b_T_T_u1$)))
(let ((?x10272 (b_S_typemap$ v_b_S_s$)))
(let ((?x24302 (b_S_select_o_tm$ ?x10272 ?x24598)))
(let ((?x24605 (b_S_ts_n_emb$ ?x24302)))
(let (($x24606 (= ?x24605 ?x22595)))
(let (($x24611 (b_S_typed$ v_b_S_s$ ?x24598)))
(let (($x24614 (not $x24611)))
(let (($x24608 (b_S_ts_n_is_n_volatile$ ?x24302)))
(let (($x24607 (not $x24606)))
(let (($x24615 (or $x24607 $x24608 (not (b_S_ts_n_is_n_array_n_elt$ ?x24302)) $x24614)))
(let (($x24616 (not $x24615)))
(let (($x11901 (>= v_b_L_H_p_G_0$ 0)))
(let (($x20030 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10238 (= ?x10163 v_b_S_result_G_0$)))
(let (($x11800 (>= (+ ?v0 (* (- 1) v_b_P_H_len$)) 0)))
(let (($x12168 (<= ?v0 4294967295)))
(let (($x16553 (not $x12168)))
(let (($x2815 (>= ?v0 0)))
(let (($x3763 (not $x2815)))
(or $x3763 $x16553 $x11800 (not $x10238))))))))) :pattern ( (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$) ) :qid k!704))
))
(let (($x20035 (not $x20030)))
(let (($x20022 (forall ((?v0 Int) )(! (let ((?x11816 (* (- 1) v_b_S_result_G_0$)))
(let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x11818 (<= (+ ?x10163 ?x11816) 0)))
(let (($x11800 (>= (+ ?v0 (* (- 1) v_b_P_H_len$)) 0)))
(let (($x12168 (<= ?v0 4294967295)))
(let (($x16553 (not $x12168)))
(let (($x2815 (>= ?v0 0)))
(let (($x3763 (not $x2815)))
(or $x3763 $x16553 $x11800 $x11818))))))))) :pattern ( (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$) ) :qid k!704))
))
(let (($x20027 (not $x20022)))
(let (($x20038 (or $x20027 $x20035)))
(let (($x20041 (not $x20038)))
(let ((?x10078 (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$)))
(let ((?x15743 (b_S_idx$ ?x10078 ?v0!15 b_T_T_u1$)))
(let ((?x15744 (b_S_read_n_u1$ v_b_S_s$ ?x15743)))
(let ((?x16029 (* (- 1) ?x15744)))
(let (($x16031 (>= (+ v_b_S_result_G_0$ ?x16029) 0)))
(let (($x16009 (<= (+ v_b_P_H_len$ (* (- 1) ?v0!15)) 0)))
(let (($x15737 (<= ?v0!15 4294967295)))
(let (($x19560 (not $x15737)))
(let (($x15736 (>= ?v0!15 0)))
(let (($x19559 (not $x15736)))
(let (($x19575 (or $x19559 $x19560 $x16009 $x16031)))
(let (($x19580 (not $x19575)))
(let (($x20044 (or $x19580 $x20041)))
(let (($x20047 (not $x20044)))
(let (($x10222 (= v_b_S_result_G_0$ v_b_L_H_max_G_1$)))
(let (($x19640 (not $x10222)))
(let (($x10220 (= v_b_SL_H_witness_G_2$ v_b_SL_H_witness_G_0$)))
(let (($x19639 (not $x10220)))
(let (($x10218 (= v_b_L_H_p_G_2$ v_b_L_H_p_G_0$)))
(let (($x19638 (not $x10218)))
(let (($x10216 (= v_b_L_H_max_G_4$ v_b_L_H_max_G_1$)))
(let (($x19637 (not $x10216)))
(let (($x11432 (>= v_b_SL_H_witness_G_0$ 0)))
(let (($x19501 (not $x11432)))
(let (($x11429 (>= v_b_L_H_p_G_0$ 1)))
(let (($x19474 (not $x11429)))
(let (($x15729 (not b_S_position_n_marker$)))
(let (($x20050 (or $x15729 $x19474 $x19501 $x19637 $x19638 $x19639 $x19640 $x20047)))
(let (($x20053 (not $x20050)))
(let (($x20056 (or $x15729 $x20053)))
(let (($x20059 (not $x20056)))
(let ((?x11484 (* (- 1) v_b_L_H_p_G_0$)))
(let ((?x11485 (+ v_b_P_H_len$ ?x11484)))
(let (($x11486 (<= ?x11485 0)))
(let (($x11487 (not $x11486)))
(let (($x20062 (or $x11487 $x19474 $x19501 $x20059)))
(let (($x20065 (not $x20062)))
(let ((?x10372 (b_S_idx$ ?x10078 v_b_SL_H_witness_G_1$ b_T_T_u1$)))
(let ((?x10373 (b_S_read_n_u1$ v_b_S_s$ ?x10372)))
(let (($x10374 (= ?x10373 v_b_L_H_max_G_3$)))
(let (($x19411 (not $x10374)))
(let (($x11647 (<= (+ v_b_P_H_len$ (* (- 1) v_b_SL_H_witness_G_1$)) 0)))
(let (($x19412 (or $x11647 $x19411)))
(let (($x19413 (not $x19412)))
(let (($x19906 (forall ((?v0 Int) )(! (let ((?x11631 (* (- 1) v_b_L_H_max_G_3$)))
(let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x11633 (<= (+ ?x10163 ?x11631) 0)))
(let (($x11615 (>= (+ ?v0 (* (- 1) v_b_L_H_p_G_1$)) 0)))
(let (($x12168 (<= ?v0 4294967295)))
(let (($x16553 (not $x12168)))
(let (($x2815 (>= ?v0 0)))
(let (($x3763 (not $x2815)))
(or $x3763 $x16553 $x11615 $x11633))))))))) :pattern ( (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$) ) :qid k!704))
))
(let (($x19911 (not $x19906)))
(let (($x19914 (or $x19911 $x19413)))
(let (($x19917 (not $x19914)))
(let ((?x15633 (b_S_idx$ ?x10078 ?v0!14 b_T_T_u1$)))
(let ((?x15634 (b_S_read_n_u1$ v_b_S_s$ ?x15633)))
(let ((?x15891 (* (- 1) ?x15634)))
(let (($x15893 (>= (+ v_b_L_H_max_G_3$ ?x15891) 0)))
(let (($x15871 (<= (+ v_b_L_H_p_G_1$ (* (- 1) ?v0!14)) 0)))
(let (($x15627 (<= ?v0!14 4294967295)))
(let (($x19366 (not $x15627)))
(let (($x15626 (>= ?v0!14 0)))
(let (($x19365 (not $x15626)))
(let (($x19381 (or $x19365 $x19366 $x15871 $x15893)))
(let (($x19386 (not $x19381)))
(let (($x19920 (or $x19386 $x19917)))
(let (($x19923 (not $x19920)))
(let (($x11608 (>= (+ v_b_P_H_len$ (* (- 1) v_b_L_H_p_G_1$)) 0)))
(let (($x11612 (not $x11608)))
(let (($x19926 (or $x11612 $x19923)))
(let (($x19929 (not $x19926)))
(let (($x19932 (or $x11612 $x19929)))
(let (($x19935 (not $x19932)))
(let (($x11536 (>= v_b_SL_H_witness_G_1$ 0)))
(let (($x19455 (not $x11536)))
(let (($x11578 (>= v_b_L_H_p_G_1$ 2)))
(let (($x19454 (not $x11578)))
(let (($x10358 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_16_o_24$ b_H_loc_o_p$ v_b_L_H_p_G_1$ b_T_T_u4$)))
(let (($x19453 (not $x10358)))
(let ((?x11581 (* (- 1) v_b_L_H_p_G_1$)))
(let ((?x11582 (+ v_b_L_H_p_G_0$ ?x11581)))
(let (($x11580 (= ?x11582 (- 1))))
(let (($x19452 (not $x11580)))
(let (($x13353 (<= v_b_L_H_p_G_0$ 4294967294)))
(let (($x15614 (not $x13353)))
(let (($x11570 (>= v_b_L_H_p_G_0$ (- 1))))
(let (($x15611 (not $x11570)))
(let (($x19938 (or $x15611 $x15614 $x19452 $x19453 $x19454 $x19455 $x19935)))
(let (($x19941 (not $x19938)))
(let (($x19944 (or $x15611 $x15614 $x19941)))
(let (($x19947 (not $x19944)))
(let (($x10392 (= v_b_SL_H_witness_G_1$ v_b_SL_H_witness_G_0$)))
(let (($x19513 (not $x10392)))
(let (($x10391 (= v_b_L_H_max_G_3$ v_b_L_H_max_G_1$)))
(let (($x19512 (not $x10391)))
(let ((?x10320 (b_S_idx$ ?x10078 v_b_L_H_p_G_0$ b_T_T_u1$)))
(let ((?x10327 (b_S_read_n_u1$ v_b_S_s$ ?x10320)))
(let ((?x11517 (* (- 1) ?x10327)))
(let (($x11516 (>= (+ v_b_L_H_max_G_1$ ?x11517) 0)))
(let (($x11515 (not $x11516)))
(let (($x19980 (or $x11515 $x19501 $x19512 $x19513 $x19474 $x19455 $x19947)))
(let (($x19983 (not $x19980)))
(let (($x10340 (= v_b_SL_H_witness_G_1$ v_b_L_H_p_G_0$)))
(let (($x19473 (not $x10340)))
(let (($x10338 (= v_b_L_H_max_G_3$ v_b_L_H_max_G_2$)))
(let (($x19472 (not $x10338)))
(let (($x10335 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_24_o_47$ b_H_loc_o_witness$ v_b_L_H_p_G_0$ b_T_T_u4$)))
(let (($x19471 (not $x10335)))
(let (($x10334 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_23_o_7$ b_H_loc_o_max$ v_b_L_H_max_G_2$ b_T_T_u1$)))
(let (($x19470 (not $x10334)))
(let (($x10333 (= v_b_L_H_max_G_2$ ?x10327)))
(let (($x19469 (not $x10333)))
(let (($x10324 (b_S_thread_n_local$ v_b_S_s$ ?x10320)))
(let (($x15599 (not $x10324)))
(let (($x10321 (b_S_is$ ?x10320 b_T_T_u1$)))
(let (($x15590 (not $x10321)))
(let (($x19950 (or $x15590 $x15599 $x19469 $x19470 $x19471 $x19472 $x19473 $x19474 $x19455 $x19947)))
(let (($x19953 (not $x19950)))
(let (($x19956 (or $x15590 $x15599 $x19953)))
(let (($x19959 (not $x19956)))
(let (($x10322 (b_S_typed$ v_b_S_s$ ?x10320)))
(let (($x15593 (not $x10322)))
(let (($x19962 (or $x15590 $x15593 $x19959)))
(let (($x19965 (not $x19962)))
(let (($x19968 (or $x15590 $x15593 $x19965)))
(let (($x19971 (not $x19968)))
(let (($x19974 (or $x11516 $x19474 $x19501 $x19971)))
(let (($x19977 (not $x19974)))
(let (($x19986 (or $x19977 $x19983)))
(let (($x19989 (not $x19986)))
(let (($x19992 (or $x15590 $x15599 $x19474 $x19501 $x19989)))
(let (($x19995 (not $x19992)))
(let (($x19998 (or $x15590 $x15599 $x19995)))
(let (($x20001 (not $x19998)))
(let (($x20004 (or $x15590 $x15593 $x20001)))
(let (($x20007 (not $x20004)))
(let (($x20010 (or $x15590 $x15593 $x20007)))
(let (($x20013 (not $x20010)))
(let (($x20016 (or $x11486 $x19474 $x19501 $x20013)))
(let (($x20019 (not $x20016)))
(let (($x20068 (or $x20019 $x20065)))
(let (($x20071 (not $x20068)))
(let ((?x2238 (b_S_ptr_n_to$ b_T_T_u1$)))
(let (($x10296 (b_S_local_n_value_n_is_n_ptr$ v_b_S_s$ b_H_tok_S_1_T_16_o_3$ b_H_loc_o_arr$ ?x10078 ?x2238)))
(let (($x19683 (not $x10296)))
(let ((?x10105 (b_S_ptr_n_to_n_int$ ?x10078)))
(let (($x10295 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_16_o_3$ b_H_loc_o_arr$ ?x10105 ?x2238)))
(let (($x19682 (not $x10295)))
(let (($x10294 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_16_o_3$ b_H_loc_o_len$ v_b_P_H_len$ b_T_T_u4$)))
(let (($x19681 (not $x10294)))
(let (($x10293 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_16_o_3$ b_H_loc_o_max$ v_b_L_H_max_G_1$ b_T_T_u1$)))
(let (($x19680 (not $x10293)))
(let (($x10292 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_16_o_3$ b_H_loc_o_witness$ v_b_SL_H_witness_G_0$ b_T_T_u4$)))
(let (($x19679 (not $x10292)))
(let (($x10291 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_16_o_3$ b_H_loc_o_p$ v_b_L_H_p_G_0$ b_T_T_u4$)))
(let (($x19678 (not $x10291)))
(let (($x10097 (b_S_full_n_stop$ v_b_S_s$)))
(let (($x19677 (not $x10097)))
(let (($x10204 (b_S_good_n_state_n_ext$ b_H_tok_S_1_T_16_o_3$ v_b_S_s$)))
(let (($x19676 (not $x10204)))
(let (($x10284 (b_S_call_n_transition$ v_b_S_s$ v_b_S_s$)))
(let (($x19675 (not $x10284)))
(let ((?x10190 (b_S_idx$ ?x10078 v_b_SL_H_witness_G_0$ b_T_T_u1$)))
(let ((?x10191 (b_S_read_n_u1$ v_b_S_s$ ?x10190)))
(let (($x10192 (= ?x10191 v_b_L_H_max_G_1$)))
(let (($x19674 (not $x10192)))
(let (($x11867 (<= (+ v_b_P_H_len$ (* (- 1) v_b_SL_H_witness_G_0$)) 0)))
(let (($x19898 (forall ((?v0 Int) )(! (let ((?x11887 (* (- 1) v_b_L_H_max_G_1$)))
(let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x11889 (<= (+ ?x10163 ?x11887) 0)))
(let (($x11871 (>= (+ ?v0 (* (- 1) v_b_L_H_p_G_0$)) 0)))
(let (($x12168 (<= ?v0 4294967295)))
(let (($x16553 (not $x12168)))
(let (($x2815 (>= ?v0 0)))
(let (($x3763 (not $x2815)))
(or $x3763 $x16553 $x11871 $x11889))))))))) :pattern ( (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$) ) :qid k!704))
))
(let (($x19903 (not $x19898)))
(let (($x11898 (>= ?x11485 0)))
(let (($x19672 (not $x11898)))
(let (($x13326 (<= v_b_L_H_p_G_0$ 4294967295)))
(let (($x19671 (not $x13326)))
(let (($x19670 (not $x11901)))
(let (($x13315 (<= v_b_SL_H_witness_G_0$ 4294967295)))
(let (($x19669 (not $x13315)))
(let (($x13304 (<= v_b_L_H_max_G_1$ 255)))
(let (($x19668 (not $x13304)))
(let (($x11911 (>= v_b_L_H_max_G_1$ 0)))
(let (($x19667 (not $x11911)))
(let ((?x10137 (b_S_idx$ ?x10078 0 b_T_T_u1$)))
(let ((?x10144 (b_S_read_n_u1$ v_b_S_s$ ?x10137)))
(let (($x10167 (= ?x10144 v_b_L_H_max_G_0$)))
(let (($x15548 (not $x10167)))
(let (($x11259 (<= v_b_P_H_len$ 0)))
(let (($x20074 (or $x11259 $x15548 $x19667 $x19668 $x19669 $x19670 $x19671 $x19672 $x19903 $x11867 $x19674 $x19675 $x19676 $x19677 $x19678 $x19679 $x19680 $x19681 $x19682 $x19683 $x19474 $x19501 $x20071)))
(let (($x20077 (not $x20074)))
(let (($x10145 (= v_b_L_H_max_G_0$ ?x10144)))
(let (($x20080 (or $x11259 $x15548 $x20077)))
(let (($x20083 (not $x20080)))
(let (($x19890 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x11404 (>= (+ v_b_L_H_max_G_0$ (* (- 1) ?x10163)) 0)))
(let (($x11388 (>= ?v0 1)))
(let (($x12168 (<= ?v0 4294967295)))
(let (($x16553 (not $x12168)))
(let (($x2815 (>= ?v0 0)))
(let (($x3763 (not $x2815)))
(or $x3763 $x16553 $x11388 $x11404)))))))) :pattern ( (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$) ) :qid k!704))
))
(let (($x19895 (not $x19890)))
(let (($x20086 (or $x19895 $x20083)))
(let (($x20089 (not $x20086)))
(let ((?x15529 (b_S_idx$ ?x10078 ?v0!13 b_T_T_u1$)))
(let ((?x15530 (b_S_read_n_u1$ v_b_S_s$ ?x15529)))
(let ((?x15531 (* (- 1) ?x15530)))
(let (($x15533 (>= (+ v_b_L_H_max_G_0$ ?x15531) 0)))
(let (($x15525 (>= ?v0!13 1)))
(let (($x15524 (<= ?v0!13 4294967295)))
(let (($x19298 (not $x15524)))
(let (($x15523 (>= ?v0!13 0)))
(let (($x19297 (not $x15523)))
(let (($x19313 (or $x19297 $x19298 $x15525 $x15533)))
(let (($x19318 (not $x19313)))
(let (($x20092 (or $x19318 $x20089)))
(let (($x20095 (not $x20092)))
(let (($x11382 (>= v_b_P_H_len$ 1)))
(let (($x11385 (not $x11382)))
(let (($x20098 (or $x11385 $x20095)))
(let (($x20101 (not $x20098)))
(let (($x20104 (or $x11385 $x20101)))
(let (($x20107 (not $x20104)))
(let (($x10148 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_16_o_8$ b_H_loc_o_p$ 1 b_T_T_u4$)))
(let (($x19727 (not $x10148)))
(let (($x10147 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_14_o_3$ b_H_loc_o_witness$ 0 b_T_T_u4$)))
(let (($x19726 (not $x10147)))
(let (($x10146 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_12_o_3$ b_H_loc_o_max$ v_b_L_H_max_G_0$ b_T_T_u1$)))
(let (($x19725 (not $x10146)))
(let (($x19724 (not $x10145)))
(let (($x10141 (b_S_thread_n_local$ v_b_S_s$ ?x10137)))
(let (($x15511 (not $x10141)))
(let (($x10138 (b_S_is$ ?x10137 b_T_T_u1$)))
(let (($x15502 (not $x10138)))
(let (($x20110 (or $x15502 $x15511 $x19724 $x19725 $x19726 $x19727 $x20107)))
(let (($x20113 (not $x20110)))
(let (($x20116 (or $x15502 $x15511 $x20113)))
(let (($x20119 (not $x20116)))
(let (($x10139 (b_S_typed$ v_b_S_s$ ?x10137)))
(let (($x15505 (not $x10139)))
(let (($x20122 (or $x15502 $x15505 $x20119)))
(let (($x20125 (not $x20122)))
(let ((?x22478 (b_S_select_o_tm$ ?x10272 ?x10137)))
(let (($x22602 (b_S_ts_n_is_n_volatile$ ?x22478)))
(let (($x22603 (or $x15505 $x22602)))
(let (($x22604 (not $x22603)))
(let ((?x10079 (b_S_ref$ ?x10078)))
(let ((?x10080 (b_S_ptr$ ?x10076 ?x10079)))
(let ((?x21014 (b_S_ref$ ?x10080)))
(let ((?x21983 (b_S_ptr$ ?x10076 ?x21014)))
(let ((?x22343 (b_S_domain$ v_b_S_s$ ?x21983)))
(let (($x22596 (b_S_set_n_in$ ?x22595 ?x22343)))
(let (($x21179 (= ?x10079 v_b_P_H_arr$)))
(let (($x19835 (forall ((?v0 B_S_ctype$) (?v1 Int) )(! (= (b_S_ref$ (b_S_ptr$ ?v0 ?v1)) ?v1) :pattern ( (b_S_ptr$ ?v0 ?v1) ) :qid k!627))
))
(let (($x9655 (forall ((?v0 B_S_ctype$) (?v1 Int) )(! (= (b_S_ref$ (b_S_ptr$ ?v0 ?v1)) ?v1) :qid k!627))
))
(let (($x9654 (= (b_S_ref$ (b_S_ptr$ ?1 ?0)) ?0)))
(let ((@x15356 (mp~ (asserted $x9655) (nnf-pos (refl (~ $x9654 $x9654)) (~ $x9655 $x9655)) $x9655)))
(let ((@x19840 (mp @x15356 (quant-intro (refl (= $x9654 $x9654)) (= $x9655 $x19835)) $x19835)))
(let (($x21152 (not $x19835)))
(let (($x21184 (or $x21152 $x21179)))
(let ((@x21185 ((_ quant-inst b_T_T_u1$ v_b_P_H_arr$) $x21184)))
(let ((@x23445 (unit-resolution @x21185 @x19840 $x21179)))
(let ((@x23680 (monotonicity (symm @x23445 (= v_b_P_H_arr$ ?x10079)) (= ?x22595 ?x10080))))
(let (($x21990 (= ?x10080 ?x21983)))
(let (($x10084 (b_S_is$ ?x10080 ?x10076)))
(let (($x11245 (>= (+ b_S_max_o_u4$ (* (- 1) v_b_P_H_len$)) 0)))
(let (($x11243 (>= v_b_P_H_len$ 0)))
(let (($x10439 (forall ((?v0 B_S_ptr$) )(! (let (($x10113 (b_S_in_n_writes_n_at$ v_b_H_wrTime_S_1_T_6_o_1$ ?v0)))
(not $x10113)) :pattern ( (b_S_in_n_writes_n_at$ v_b_H_wrTime_S_1_T_6_o_1$ ?v0) ) :qid k!704))
))
(let ((?x10111 (b_S_current_n_timestamp$ v_b_S_s$)))
(let (($x10112 (= v_b_H_wrTime_S_1_T_6_o_1$ ?x10111)))
(let (($x10109 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_6_o_1$ b_H_loc_o_len$ v_b_P_H_len$ b_T_T_u4$)))
(let (($x10107 (b_S_local_n_value_n_is_n_ptr$ v_b_S_s$ b_H_tok_S_1_T_6_o_1$ b_H_loc_o_arr$ ?x10078 ?x2238)))
(let (($x10106 (b_S_local_n_value_n_is$ v_b_S_s$ b_H_tok_S_1_T_6_o_1$ b_H_loc_o_arr$ ?x10105 ?x2238)))
(let (($x11256 (forall ((?v0 B_S_pure_n_function$) )(! (let (($x11251 (>= (+ (b_S_frame_n_level$ ?v0) (* (- 1) b_S_current_n_frame_n_level$)) 0)))
(not $x11251)) :pattern ( (b_S_frame_n_level$ ?v0) ) :qid k!704))
))
(let (($x10096 (b_S_good_n_state_n_ext$ b_H_tok_S_1_T_6_o_1$ v_b_S_s$)))
(let (($x10095 (b_S_function_n_entry$ v_b_S_s$)))
(let (($x10089 (b_S_is_n_non_n_primitive$ ?x10076)))
(let ((?x10086 (b_S_kind_n_of$ ?x10076)))
(let (($x10087 (= ?x10086 b_S_kind_n_primitive$)))
(let (($x10088 (not $x10087)))
(let (($x10085 (b_S_typed$ v_b_S_s$ ?x10080)))
(let ((?x10082 (b_S_owner$ v_b_S_s$ ?x10080)))
(let (($x10083 (= ?x10082 b_S_me$)))
(let (($x10081 (b_S_closed$ v_b_S_s$ ?x10080)))
(let (($x11260 (not $x11259)))
(let (($x11263 (>= v_b_P_H_len$ 1099511627776)))
(let (($x11264 (not $x11263)))
(let (($x11270 (>= (+ b_S_max_o_u4$ (* (- 1) v_b_SL_H_witness$)) 0)))
(let (($x11268 (>= v_b_SL_H_witness$ 0)))
(let (($x11278 (>= (+ b_S_max_o_u4$ (* (- 1) v_b_L_H_p$)) 0)))
(let (($x11276 (>= v_b_L_H_p$ 0)))
(let (($x11286 (>= (+ b_S_max_o_u1$ (* (- 1) v_b_L_H_max$)) 0)))
(let (($x11284 (>= v_b_L_H_max$ 0)))
(let (($x11342 (and $x11284 $x11286 $x11276 $x11278 $x11268 $x11270 $x11264 $x11260 $x10081 $x10083 $x10084 $x10085 $x10088 $x10089 $x10095 $x10096 $x10097 $x11256 $x10106 $x10107 $x10109 $x10112 $x10439 $x11243 $x11245)))
(let (($x11844 (exists ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10238 (= ?x10163 v_b_S_result_G_0$)))
(let (($x11800 (>= (+ ?v0 (* (- 1) v_b_P_H_len$)) 0)))
(let (($x11802 (not $x11800)))
(let ((?x3113 (* (- 1) b_S_max_o_u4$)))
(let ((?x3114 (+ ?v0 ?x3113)))
(let (($x3115 (<= ?x3114 0)))
(let (($x2815 (>= ?v0 0)))
(and $x2815 $x3115 $x11802 $x10238))))))))) :qid k!704))
))
(let (($x11824 (forall ((?v0 Int) )(! (let ((?x11816 (* (- 1) v_b_S_result_G_0$)))
(let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x11818 (<= (+ ?x10163 ?x11816) 0)))
(let (($x11800 (>= (+ ?v0 (* (- 1) v_b_P_H_len$)) 0)))
(let (($x11802 (not $x11800)))
(let ((?x3113 (* (- 1) b_S_max_o_u4$)))
(let ((?x3114 (+ ?v0 ?x3113)))
(let (($x3115 (<= ?x3114 0)))
(let (($x2815 (>= ?v0 0)))
(let (($x11808 (and $x2815 $x3115 $x11802)))
(let (($x11813 (not $x11808)))
(or $x11813 $x11818)))))))))))) :qid k!704))
))
(let (($x11827 (not $x11824)))
(let (($x11847 (or $x11827 $x11844)))
(let (($x11850 (and $x11824 $x11847)))
(let (($x11792 (and b_S_position_n_marker$ $x11429 $x11432 $x10216 $x10218 $x10220 $x10222)))
(let (($x11797 (not $x11792)))
(let (($x11853 (or $x11797 $x11850)))
(let (($x11856 (and b_S_position_n_marker$ $x11853)))
(let (($x11772 (and $x11486 $x11429 $x11432)))
(let (($x11777 (not $x11772)))
(let (($x11859 (or $x11777 $x11856)))
(let (($x11648 (not $x11647)))
(let (($x11651 (and $x11648 $x10374)))
(let (($x11639 (forall ((?v0 Int) )(! (let ((?x11631 (* (- 1) v_b_L_H_max_G_3$)))
(let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x11633 (<= (+ ?x10163 ?x11631) 0)))
(let (($x11615 (>= (+ ?v0 (* (- 1) v_b_L_H_p_G_1$)) 0)))
(let (($x11617 (not $x11615)))
(let ((?x3113 (* (- 1) b_S_max_o_u4$)))
(let ((?x3114 (+ ?v0 ?x3113)))
(let (($x3115 (<= ?x3114 0)))
(let (($x2815 (>= ?v0 0)))
(let (($x11623 (and $x2815 $x3115 $x11617)))
(let (($x11628 (not $x11623)))
(or $x11628 $x11633)))))))))))) :qid k!704))
))
(let (($x11642 (not $x11639)))
(let (($x11654 (or $x11642 $x11651)))
(let (($x11657 (and $x11639 $x11654)))
(let (($x11660 (or $x11612 $x11657)))
(let (($x11663 (and $x11608 $x11660)))
(let ((?x11574 (+ b_S_max_o_u4$ ?x11484)))
(let (($x11573 (>= ?x11574 1)))
(let (($x11600 (and $x11570 $x11573 $x11580 $x10358 $x11578 $x11536)))
(let (($x11605 (not $x11600)))
(let (($x11666 (or $x11605 $x11663)))
(let (($x11672 (and $x11570 $x11573 $x11666)))
(let (($x11725 (and $x11516 $x11432 $x10391 $x10392 $x11429 $x11536)))
(let (($x11730 (not $x11725)))
(let (($x11733 (or $x11730 $x11672)))
(let (($x11562 (and $x10321 $x10324 $x10333 $x10334 $x10335 $x10338 $x10340 $x11429 $x11536)))
(let (($x11567 (not $x11562)))
(let (($x11677 (or $x11567 $x11672)))
(let (($x11683 (and $x10321 $x10324 $x11677)))
(let (($x10323 (and $x10321 $x10322)))
(let (($x11001 (not $x10323)))
(let (($x11688 (or $x11001 $x11683)))
(let (($x11694 (and $x10321 $x10322 $x11688)))
(let (($x11527 (and $x11515 $x11429 $x11432)))
(let (($x11532 (not $x11527)))
(let (($x11699 (or $x11532 $x11694)))
(let (($x11736 (and $x11699 $x11733)))
(let (($x11507 (and $x10321 $x10324 $x11429 $x11432)))
(let (($x11512 (not $x11507)))
(let (($x11739 (or $x11512 $x11736)))
(let (($x11745 (and $x10321 $x10324 $x11739)))
(let (($x11750 (or $x11001 $x11745)))
(let (($x11756 (and $x10321 $x10322 $x11750)))
(let (($x11496 (and $x11487 $x11429 $x11432)))
(let (($x11501 (not $x11496)))
(let (($x11761 (or $x11501 $x11756)))
(let (($x11862 (and $x11761 $x11859)))
(let (($x11476 (and $x10284 $x10204 $x10097 $x10291 $x10292 $x10293 $x10294 $x10295 $x10296 $x11429 $x11432)))
(let (($x11481 (not $x11476)))
(let (($x11868 (not $x11867)))
(let (($x11895 (forall ((?v0 Int) )(! (let ((?x11887 (* (- 1) v_b_L_H_max_G_1$)))
(let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x11889 (<= (+ ?x10163 ?x11887) 0)))
(let (($x11871 (>= (+ ?v0 (* (- 1) v_b_L_H_p_G_0$)) 0)))
(let (($x11873 (not $x11871)))
(let ((?x3113 (* (- 1) b_S_max_o_u4$)))
(let ((?x3114 (+ ?v0 ?x3113)))
(let (($x3115 (<= ?x3114 0)))
(let (($x2815 (>= ?v0 0)))
(let (($x11879 (and $x2815 $x3115 $x11873)))
(let (($x11884 (not $x11879)))
(or $x11884 $x11889)))))))))))) :qid k!704))
))
(let (($x11904 (>= ?x11574 0)))
(let (($x11907 (>= (+ b_S_max_o_u4$ (* (- 1) v_b_SL_H_witness_G_0$)) 0)))
(let (($x11914 (>= (+ b_S_max_o_u1$ (* (- 1) v_b_L_H_max_G_1$)) 0)))
(let (($x11957 (and $x11260 $x10167 $x11911 $x11914 $x11907 $x11901 $x11904 $x11898 $x11895 $x11868 $x10192 $x11429 $x11432)))
(let (($x11962 (not $x11957)))
(let (($x11971 (or $x11962 $x11481 $x11862)))
(let (($x11979 (and $x11260 $x10167 $x11971)))
(let (($x11411 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x11404 (>= (+ v_b_L_H_max_G_0$ (* (- 1) ?x10163)) 0)))
(let (($x11388 (>= ?v0 1)))
(let (($x11389 (not $x11388)))
(let ((?x3113 (* (- 1) b_S_max_o_u4$)))
(let ((?x3114 (+ ?v0 ?x3113)))
(let (($x3115 (<= ?x3114 0)))
(let (($x2815 (>= ?v0 0)))
(let (($x11395 (and $x2815 $x3115 $x11389)))
(let (($x11400 (not $x11395)))
(or $x11400 $x11404))))))))))) :qid k!704))
))
(let (($x11414 (not $x11411)))
(let (($x11984 (or $x11414 $x11979)))
(let (($x11987 (and $x11411 $x11984)))
(let (($x11990 (or $x11385 $x11987)))
(let (($x11993 (and $x11382 $x11990)))
(let (($x11374 (and $x10138 $x10141 $x10145 $x10146 $x10147 $x10148)))
(let (($x11379 (not $x11374)))
(let (($x11996 (or $x11379 $x11993)))
(let (($x12002 (and $x10138 $x10141 $x11996)))
(let (($x10140 (and $x10138 $x10139)))
(let (($x11209 (not $x10140)))
(let (($x12007 (or $x11209 $x12002)))
(let (($x12013 (and $x10138 $x10139 $x12007)))
(let (($x10136 (b_S_in_n_domain_n_lab$ v_b_S_s$ ?x10080 ?x10080 b_l_H_public$)))
(let (($x11221 (not $x10136)))
(let (($x12018 (or $x11221 $x12013)))
(let (($x12021 (and $x10136 $x12018)))
(let (($x12027 (not (or (not $x11342) $x12021))))
(let (($x10242 (exists ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10238 (= ?x10163 v_b_S_result_G_0$)))
(let (($x10233 (< ?v0 v_b_P_H_len$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(and $x2766 (and $x3097 (and $x10233 $x10238)))))))) :qid k!704))
))
(let (($x10244 (and $x10242 (=> $x10242 true))))
(let (($x10237 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10235 (<= ?x10163 v_b_S_result_G_0$)))
(let (($x10233 (< ?v0 v_b_P_H_len$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10234 (and $x3098 $x10233)))
(=> $x10234 $x10235)))))))) :qid k!704))
))
(let (($x10245 (=> $x10237 $x10244)))
(let (($x10227 (and true (and $x10216 (and $x10218 (and $x10220 (and $x10222 true)))))))
(let (($x10174 (<= 0 v_b_SL_H_witness_G_0$)))
(let (($x10181 (<= 1 v_b_L_H_p_G_0$)))
(let (($x10182 (and $x10181 $x10174)))
(let (($x10230 (and true (and $x10182 (and $x10182 $x10227)))))
(let (($x10247 (=> (and b_S_position_n_marker$ (and $x10182 $x10230)) (and $x10237 $x10245))))
(let (($x10248 (and b_S_position_n_marker$ $x10247)))
(let (($x10206 (and true $x10182)))
(let (($x10207 (and $x10182 $x10206)))
(let (($x10411 (and $x10182 $x10207)))
(let (($x10412 (and true $x10411)))
(let (($x10413 (and $x10182 $x10412)))
(let (($x10410 (<= v_b_P_H_len$ v_b_L_H_p_G_0$)))
(let (($x10416 (and true (and $x10182 (and $x10410 $x10413)))))
(let (($x10417 (=> $x10416 $x10248)))
(let (($x10377 (=> (and (and (< v_b_SL_H_witness_G_1$ v_b_P_H_len$) $x10374) false) true)))
(let (($x10375 (and (< v_b_SL_H_witness_G_1$ v_b_P_H_len$) $x10374)))
(let (($x10378 (and $x10375 $x10377)))
(let (($x10370 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10368 (<= ?x10163 v_b_L_H_max_G_3$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10367 (and $x3098 (< ?v0 v_b_L_H_p_G_1$))))
(=> $x10367 $x10368))))))) :qid k!704))
))
(let (($x10379 (=> $x10370 $x10378)))
(let (($x10365 (<= v_b_L_H_p_G_1$ v_b_P_H_len$)))
(let (($x10381 (=> $x10365 (and $x10370 $x10379))))
(let (($x10341 (<= 0 v_b_SL_H_witness_G_1$)))
(let (($x10360 (and (<= 2 v_b_L_H_p_G_1$) $x10341)))
(let (($x10363 (and (= v_b_L_H_p_G_1$ (+ v_b_L_H_p_G_0$ 1)) (and $x10358 (and $x10360 true)))))
(let (($x10355 (and (<= 0 (+ v_b_L_H_p_G_0$ 1)) (<= (+ v_b_L_H_p_G_0$ 1) b_S_max_o_u4$))))
(let (($x10383 (=> (and $x10355 $x10363) (and $x10365 $x10381))))
(let (($x10384 (and $x10355 $x10383)))
(let (($x10395 (and true (and $x10391 (and $x10392 (and true (and $x10181 $x10341)))))))
(let (($x10398 (and true (and $x10182 (and $x10182 $x10395)))))
(let (($x10390 (<= ?x10327 v_b_L_H_max_G_1$)))
(let (($x10402 (and true (and $x10182 (and $x10390 (and $x10182 $x10398))))))
(let (($x10403 (=> $x10402 $x10384)))
(let (($x10346 (and true (and $x10338 (and $x10340 (and true (and $x10181 $x10341)))))))
(let (($x10325 (and $x10321 $x10324)))
(let (($x10351 (and $x10325 (and $x10333 (and $x10334 (and $x10335 (and (and $x10181 $x10181) $x10346)))))))
(let (($x10385 (=> $x10351 $x10384)))
(let (($x10387 (=> $x10323 (and $x10325 $x10385))))
(let (($x10331 (and true (and $x10182 (and (< v_b_L_H_max_G_1$ ?x10327) $x10207)))))
(let (($x10389 (=> $x10331 (and $x10323 $x10387))))
(let (($x10326 (and $x10325 $x10182)))
(let (($x10405 (=> $x10326 (and $x10389 $x10403))))
(let (($x10407 (=> $x10323 (and $x10325 $x10405))))
(let (($x10319 (and true (and $x10182 (and (< v_b_L_H_p_G_0$ v_b_P_H_len$) $x10207)))))
(let (($x10409 (=> $x10319 (and $x10323 $x10407))))
(let (($x10300 (and (= ?x10272 ?x10272) (= (b_S_statusmap$ v_b_S_s$) (b_S_statusmap$ v_b_S_s$)))))
(let (($x10301 (and $x10300 $x10182)))
(let (($x10297 (and $x10295 $x10296)))
(let (($x10205 (and $x10204 $x10097)))
(let (($x10307 (and $x10205 (and $x10291 (and $x10292 (and $x10293 (and $x10294 (and $x10297 $x10301))))))))
(let (($x10283 (forall ((?v0 B_S_ptr$) )(! (let ((?x10280 (b_S_timestamp$ v_b_S_s$ ?v0)))
(<= ?x10280 ?x10280)) :pattern ( (b_S_timestamp$ v_b_S_s$ ?v0) ) :qid k!704))
))
(let (($x10286 (and (<= ?x10111 ?x10111) (and $x10283 $x10284))))
(let (($x10278 (forall ((?v0 B_S_ptr$) )(! (let (($x10260 (b_S_thread_n_local$ v_b_S_s$ ?v0)))
(let ((?x10272 (b_S_typemap$ v_b_S_s$)))
(let ((?x10273 (b_S_select_o_tm$ ?x10272 ?v0)))
(let (($x10275 (and (= ?x10273 ?x10273) $x10260)))
(=> $x10260 $x10275))))) :pattern ( (b_S_select_o_tm$ (b_S_typemap$ v_b_S_s$) ?v0) ) :qid k!704))
))
(let (($x10287 (and $x10278 $x10286)))
(let (($x10271 (forall ((?v0 B_S_ptr$) )(! (let (($x10260 (b_S_thread_n_local$ v_b_S_s$ ?v0)))
(let ((?x10256 (b_S_statusmap$ v_b_S_s$)))
(let ((?x10257 (b_S_select_o_sm$ ?x10256 ?v0)))
(let (($x10269 (and (= ?x10257 ?x10257) $x10260)))
(=> $x10260 $x10269))))) :pattern ( (b_S_select_o_sm$ (b_S_statusmap$ v_b_S_s$) ?v0) ) :qid k!704))
))
(let (($x10288 (and $x10271 $x10287)))
(let (($x10267 (forall ((?v0 B_S_ptr$) )(! (let (($x10260 (b_S_thread_n_local$ v_b_S_s$ ?v0)))
(let ((?x10261 (b_S_memory$ v_b_S_s$)))
(let ((?x10262 (b_S_select_o_mem$ ?x10261 ?v0)))
(let (($x10264 (and (= ?x10262 ?x10262) $x10260)))
(=> $x10260 $x10264))))) :pattern ( (b_S_select_o_mem$ (b_S_memory$ v_b_S_s$) ?v0) ) :qid k!704))
))
(let (($x10289 (and $x10267 $x10288)))
(let (($x10259 (forall ((?v0 B_S_ptr$) )(! (let (($x10253 (= (b_S_kind_n_of$ (b_S_typ$ (b_S_owner$ v_b_S_s$ ?v0))) b_S_kind_n_thread$)))
(=> (not $x10253) (not $x10253))) :pattern ( (b_S_select_o_sm$ (b_S_statusmap$ v_b_S_s$) ?v0) ) :qid k!704))
))
(let (($x10290 (and $x10259 $x10289)))
(let (($x10311 (and true (and $x10182 (and $x10290 (and $x10286 $x10307))))))
(let (($x10313 (and true (and $x10182 $x10311))))
(let (($x10315 (and true (and $x10182 $x10313))))
(let (($x10419 (=> $x10315 (and $x10409 $x10417))))
(let (($x10203 (not true)))
(let (($x10212 (and $x10203 (and $x10182 (and true (and $x10182 (and $x10205 $x10207)))))))
(let (($x10213 (and $x10182 $x10212)))
(let (($x10214 (and true $x10213)))
(let (($x10249 (=> $x10214 $x10248)))
(let (($x10420 (and $x10249 $x10419)))
(let (($x10194 (and (and (< v_b_SL_H_witness_G_0$ v_b_P_H_len$) $x10192) $x10182)))
(let (($x10188 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10186 (<= ?x10163 v_b_L_H_max_G_1$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10185 (and $x3098 (< ?v0 v_b_L_H_p_G_0$))))
(=> $x10185 $x10186))))))) :qid k!704))
))
(let (($x10183 (<= v_b_L_H_p_G_0$ v_b_P_H_len$)))
(let (($x10180 (and (<= 0 v_b_L_H_p_G_0$) (<= v_b_L_H_p_G_0$ b_S_max_o_u4$))))
(let (($x10176 (and $x10174 (<= v_b_SL_H_witness_G_0$ b_S_max_o_u4$))))
(let (($x10172 (and (<= 0 v_b_L_H_max_G_1$) (<= v_b_L_H_max_G_1$ b_S_max_o_u1$))))
(let (($x10200 (and $x10172 (and $x10176 (and $x10180 (and $x10182 (and $x10183 (and $x10188 $x10194))))))))
(let (($x10201 (and true $x10200)))
(let (($x10074 (< 0 v_b_P_H_len$)))
(let (($x10168 (and $x10074 $x10167)))
(let (($x10421 (=> (and $x10168 $x10201) $x10420)))
(let (($x10166 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10164 (<= ?x10163 v_b_L_H_max_G_0$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10161 (and $x3098 (< ?v0 1))))
(=> $x10161 $x10164))))))) :qid k!704))
))
(let (($x10423 (=> $x10166 (and $x10168 $x10421))))
(let (($x10159 (<= 1 v_b_P_H_len$)))
(let (($x10425 (=> $x10159 (and $x10166 $x10423))))
(let (($x10149 (<= 1 1)))
(let (($x10154 (and $x10148 (and $x10149 (and $x10149 (and (<= 0 0) (<= 0 0)))))))
(let (($x10142 (and $x10138 $x10141)))
(let (($x10427 (=> (and $x10142 (and $x10145 (and $x10146 (and $x10147 $x10154)))) (and $x10159 $x10425))))
(let (($x10429 (=> $x10140 (and $x10142 $x10427))))
(let (($x10431 (=> $x10136 (and $x10140 $x10429))))
(let (($x10119 (and (<= 0 v_b_P_H_len$) (<= v_b_P_H_len$ b_S_max_o_u4$))))
(let (($x10116 (forall ((?v0 B_S_ptr$) )(! (let (($x10113 (b_S_in_n_writes_n_at$ v_b_H_wrTime_S_1_T_6_o_1$ ?v0)))
(= $x10113 false)) :pattern ( (b_S_in_n_writes_n_at$ v_b_H_wrTime_S_1_T_6_o_1$ ?v0) ) :qid k!704))
))
(let (($x10108 (and $x10106 $x10107)))
(let (($x10104 (forall ((?v0 B_S_pure_n_function$) )(! (let ((?x10100 (b_S_frame_n_level$ ?v0)))
(< ?x10100 b_S_current_n_frame_n_level$)) :pattern ( (b_S_frame_n_level$ ?v0) ) :qid k!704))
))
(let (($x10098 (and $x10096 $x10097)))
(let (($x10125 (and $x10098 (and $x10104 (and $x10108 (and $x10109 (and $x10112 (and $x10116 $x10119))))))))
(let (($x10127 (and true (and $x10095 $x10125))))
(let (($x10094 (and $x10081 (and $x10083 (and $x10084 (and $x10085 (and $x10088 $x10089)))))))
(let (($x10073 (< v_b_P_H_len$ 1099511627776)))
(let (($x10071 (and (<= 0 v_b_SL_H_witness$) (<= v_b_SL_H_witness$ b_S_max_o_u4$))))
(let (($x10067 (and (<= 0 v_b_L_H_p$) (<= v_b_L_H_p$ b_S_max_o_u4$))))
(let (($x10063 (and (<= 0 v_b_L_H_max$) (<= v_b_L_H_max$ b_S_max_o_u1$))))
(let (($x10133 (and $x10063 (and $x10067 (and $x10071 (and $x10073 (and $x10074 (and $x10094 $x10127))))))))
(let (($x10134 (and true $x10133)))
(let (($x10433 (=> $x10134 (and $x10136 $x10431))))
(let (($x10434 (not $x10433)))
(let (($x10649 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10235 (<= ?x10163 v_b_S_result_G_0$)))
(let (($x10233 (< ?v0 v_b_P_H_len$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10234 (and $x3098 $x10233)))
(or (not $x10234) $x10235)))))))) :qid k!704))
))
(let (($x10665 (or (not $x10649) $x10242)))
(let (($x10670 (and $x10649 $x10665)))
(let (($x10616 (and $x10216 (and $x10218 (and $x10220 $x10222)))))
(let (($x10626 (and $x10182 $x10616)))
(let (($x10629 (and $x10182 $x10626)))
(let (($x10639 (and $x10182 $x10629)))
(let (($x10642 (and b_S_position_n_marker$ $x10639)))
(let (($x10677 (or (not $x10642) $x10670)))
(let (($x10682 (and b_S_position_n_marker$ $x10677)))
(let (($x11134 (or (not (and $x10182 (and $x10410 $x10182))) $x10682)))
(let (($x10931 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10368 (<= ?x10163 v_b_L_H_max_G_3$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10367 (and $x3098 (< ?v0 v_b_L_H_p_G_1$))))
(or (not $x10367) $x10368))))))) :qid k!704))
))
(let (($x10954 (or (not $x10931) $x10375)))
(let (($x10959 (and $x10931 $x10954)))
(let (($x10966 (or (not $x10365) $x10959)))
(let (($x10971 (and $x10365 $x10966)))
(let (($x10918 (and $x10358 $x10360)))
(let ((?x10901 (+ 1 v_b_L_H_p_G_0$)))
(let (($x10913 (= v_b_L_H_p_G_1$ ?x10901)))
(let (($x10921 (and $x10913 $x10918)))
(let (($x10907 (<= ?x10901 b_S_max_o_u4$)))
(let (($x10904 (<= 0 ?x10901)))
(let (($x10910 (and $x10904 $x10907)))
(let (($x10924 (and $x10910 $x10921)))
(let (($x10978 (or (not $x10924) $x10971)))
(let (($x10983 (and $x10910 $x10978)))
(let (($x10342 (and $x10181 $x10341)))
(let (($x11019 (and $x10392 $x10342)))
(let (($x11022 (and $x10391 $x11019)))
(let (($x11032 (and $x10182 $x11022)))
(let (($x11035 (and $x10182 $x11032)))
(let (($x11045 (and $x10182 $x11035)))
(let (($x11048 (and $x10390 $x11045)))
(let (($x11051 (and $x10182 $x11048)))
(let (($x11065 (or (not $x11051) $x10983)))
(let (($x10873 (and $x10340 $x10342)))
(let (($x10876 (and $x10338 $x10873)))
(let (($x10886 (and $x10181 $x10876)))
(let (($x10889 (and $x10335 $x10886)))
(let (($x10892 (and $x10334 $x10889)))
(let (($x10895 (and $x10333 $x10892)))
(let (($x10898 (and $x10325 $x10895)))
(let (($x10990 (or (not $x10898) $x10983)))
(let (($x10995 (and $x10325 $x10990)))
(let (($x11002 (or $x11001 $x10995)))
(let (($x11007 (and $x10323 $x11002)))
(let (($x11014 (or (not (and $x10182 (and (< v_b_L_H_max_G_1$ ?x10327) $x10182))) $x11007)))
(let (($x11070 (and $x11014 $x11065)))
(let (($x11077 (or (not $x10326) $x11070)))
(let (($x11082 (and $x10325 $x11077)))
(let (($x11088 (or $x11001 $x11082)))
(let (($x11093 (and $x10323 $x11088)))
(let (($x11100 (or (not (and $x10182 (and (< v_b_L_H_p_G_0$ v_b_P_H_len$) $x10182))) $x11093)))
(let (($x11139 (and $x11100 $x11134)))
(let (($x10789 (and $x10297 $x10182)))
(let (($x10792 (and $x10294 $x10789)))
(let (($x10795 (and $x10293 $x10792)))
(let (($x10798 (and $x10292 $x10795)))
(let (($x10801 (and $x10291 $x10798)))
(let (($x10804 (and $x10205 $x10801)))
(let (($x10807 (and $x10286 $x10804)))
(let (($x10810 (and $x10286 $x10807)))
(let (($x10813 (and $x10182 $x10810)))
(let (($x10823 (and $x10182 $x10813)))
(let (($x10833 (and $x10182 $x10823)))
(let (($x11146 (or (not $x10833) $x11139)))
(let (($x10529 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10186 (<= ?x10163 v_b_L_H_max_G_1$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10185 (and $x3098 (< ?v0 v_b_L_H_p_G_0$))))
(or (not $x10185) $x10186))))))) :qid k!704))
))
(let (($x10532 (and $x10529 $x10194)))
(let (($x10535 (and $x10183 $x10532)))
(let (($x10538 (and $x10182 $x10535)))
(let (($x10541 (and $x10180 $x10538)))
(let (($x10544 (and $x10176 $x10541)))
(let (($x10547 (and $x10172 $x10544)))
(let (($x10557 (and $x10168 $x10547)))
(let (($x11162 (or (not $x10557) $x11146)))
(let (($x11167 (and $x10168 $x11162)))
(let (($x10522 (forall ((?v0 Int) )(! (let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ (b_S_ptr$ b_T_T_u1$ v_b_P_H_arr$) ?v0 b_T_T_u1$))))
(let (($x10164 (<= ?x10163 v_b_L_H_max_G_0$)))
(let (($x3097 (<= ?v0 b_S_max_o_u4$)))
(let (($x2766 (<= 0 ?v0)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10161 (and $x3098 (< ?v0 1))))
(or (not $x10161) $x10164))))))) :qid k!704))
))
(let (($x11174 (or (not $x10522) $x11167)))
(let (($x11179 (and $x10522 $x11174)))
(let (($x11186 (or (not $x10159) $x11179)))
(let (($x11191 (and $x10159 $x11186)))
(let (($x10150 (<= 0 0)))
(let (($x10497 (and $x10149 $x10150)))
(let (($x10500 (and $x10149 $x10497)))
(let (($x10503 (and $x10148 $x10500)))
(let (($x10506 (and $x10147 $x10503)))
(let (($x10509 (and $x10146 $x10506)))
(let (($x10512 (and $x10145 $x10509)))
(let (($x10515 (and $x10142 $x10512)))
(let (($x11198 (or (not $x10515) $x11191)))
(let (($x11203 (and $x10142 $x11198)))
(let (($x11210 (or $x11209 $x11203)))
(let (($x11215 (and $x10140 $x11210)))
(let (($x11222 (or $x11221 $x11215)))
(let (($x11227 (and $x10136 $x11222)))
(let (($x10442 (and $x10439 $x10119)))
(let (($x10445 (and $x10112 $x10442)))
(let (($x10448 (and $x10109 $x10445)))
(let (($x10451 (and $x10108 $x10448)))
(let (($x10454 (and $x10104 $x10451)))
(let (($x10457 (and $x10098 $x10454)))
(let (($x10460 (and $x10095 $x10457)))
(let (($x10470 (and $x10094 $x10460)))
(let (($x10473 (and $x10074 $x10470)))
(let (($x10476 (and $x10073 $x10473)))
(let (($x10479 (and $x10071 $x10476)))
(let (($x10482 (and $x10067 $x10479)))
(let (($x10485 (and $x10063 $x10482)))
(let (($x11234 (or (not $x10485) $x11227)))
(let ((?x10163 (b_S_read_n_u1$ v_b_S_s$ (b_S_idx$ ?x10078 ?0 b_T_T_u1$))))
(let (($x10238 (= ?x10163 v_b_S_result_G_0$)))
(let (($x11800 (>= (+ ?0 (* (- 1) v_b_P_H_len$)) 0)))
(let (($x11802 (not $x11800)))
(let ((?x3113 (* (- 1) b_S_max_o_u4$)))
(let ((?x3114 (+ ?0 ?x3113)))
(let (($x3115 (<= ?x3114 0)))
(let (($x2815 (>= ?0 0)))
(let (($x11839 (and $x2815 $x3115 $x11802 $x10238)))
(let (($x2766 (<= 0 ?0)))
(let (($x10241 (and $x2766 (and (<= ?0 b_S_max_o_u4$) (and (< ?0 v_b_P_H_len$) $x10238)))))
(let (($x11834 (= (and (<= ?0 b_S_max_o_u4$) (and (< ?0 v_b_P_H_len$) $x10238)) (and $x3115 (and $x11802 $x10238)))))
(let ((@x11832 (monotonicity (rewrite (= (< ?0 v_b_P_H_len$) $x11802)) (= (and (< ?0 v_b_P_H_len$) $x10238) (and $x11802 $x10238)))))
(let ((@x2814 (rewrite (= $x2766 $x2815))))
(let ((@x11838 (monotonicity @x2814 (monotonicity (rewrite (= (<= ?0 b_S_max_o_u4$) $x3115)) @x11832 $x11834) (= $x10241 (and $x2815 (and $x3115 (and $x11802 $x10238)))))))
(let ((@x11843 (trans @x11838 (rewrite (= (and $x2815 (and $x3115 (and $x11802 $x10238))) $x11839)) (= $x10241 $x11839))))
(let (($x11818 (<= (+ ?x10163 (* (- 1) v_b_S_result_G_0$)) 0)))
(let (($x11808 (and $x2815 $x3115 $x11802)))
(let (($x11813 (not $x11808)))
(let (($x11821 (or $x11813 $x11818)))
(let (($x10235 (<= ?x10163 v_b_S_result_G_0$)))
(let (($x10233 (< ?0 v_b_P_H_len$)))
(let (($x3097 (<= ?0 b_S_max_o_u4$)))
(let (($x3098 (and $x2766 $x3097)))
(let (($x10234 (and $x3098 $x10233)))
(let (($x10646 (or (not $x10234) $x10235)))
(let ((@x3124 (monotonicity @x2814 (rewrite (= $x3097 $x3115)) (= $x3098 (and $x2815 $x3115)))))
(let ((@x11807 (monotonicity @x3124 (rewrite (= $x10233 $x11802)) (= $x10234 (and (and $x2815 $x3115) $x11802)))))
(let ((@x11812 (trans @x11807 (rewrite (= (and (and $x2815 $x3115) $x11802) $x11808)) (= $x10234 $x11808))))
(let ((@x11823 (monotonicity (monotonicity @x11812 (= (not $x10234) $x11813)) (rewrite (= $x10235 $x11818)) (= $x10646 $x11821))))
(let ((@x11829 (monotonicity (quant-intro @x11823 (= $x10649 $x11824)) (= (not $x10649) $x11827))))
(let ((@x11852 (monotonicity (quant-intro @x11823 (= $x10649 $x11824)) (monotonicity @x11829 (quant-intro @x11843 (= $x10242 $x11844)) (= $x10665 $x11847)) (= $x10670 $x11850))))
(let (($x11434 (and $x11429 $x11432)))
(let (($x11793 (= (and b_S_position_n_marker$ (and $x11434 (and $x11434 (and $x11434 $x10616)))) $x11792)))
(let (($x11790 (= $x10642 (and b_S_position_n_marker$ (and $x11434 (and $x11434 (and $x11434 $x10616)))))))
(let ((@x11430 (rewrite (= $x10181 $x11429))))
(let ((@x11436 (monotonicity @x11430 (rewrite (= $x10174 $x11432)) (= $x10182 $x11434))))
(let ((@x11785 (monotonicity @x11436 (monotonicity @x11436 (= $x10626 (and $x11434 $x10616))) (= $x10629 (and $x11434 (and $x11434 $x10616))))))
(let ((@x11788 (monotonicity @x11436 @x11785 (= $x10639 (and $x11434 (and $x11434 (and $x11434 $x10616)))))))
(let ((@x11799 (monotonicity (trans (monotonicity @x11788 $x11790) (rewrite $x11793) (= $x10642 $x11792)) (= (not $x10642) $x11797))))
(let ((@x11858 (monotonicity (monotonicity @x11799 @x11852 (= $x10677 $x11853)) (= $x10682 $x11856))))
(let ((@x11768 (monotonicity (rewrite (= $x10410 $x11486)) @x11436 (= (and $x10410 $x10182) (and $x11486 $x11434)))))
(let ((@x11771 (monotonicity @x11436 @x11768 (= (and $x10182 (and $x10410 $x10182)) (and $x11434 (and $x11486 $x11434))))))
(let ((@x11776 (trans @x11771 (rewrite (= (and $x11434 (and $x11486 $x11434)) $x11772)) (= (and $x10182 (and $x10410 $x10182)) $x11772))))
(let ((@x11861 (monotonicity (monotonicity @x11776 (= (not (and $x10182 (and $x10410 $x10182))) $x11777)) @x11858 (= $x11134 $x11859))))
(let ((@x11653 (monotonicity (rewrite (= (< v_b_SL_H_witness_G_1$ v_b_P_H_len$) $x11648)) (= $x10375 $x11651))))
(let (($x11633 (<= (+ ?x10163 (* (- 1) v_b_L_H_max_G_3$)) 0)))
(let (($x11615 (>= (+ ?0 ?x11581) 0)))
(let (($x11617 (not $x11615)))
(let (($x11623 (and $x2815 $x3115 $x11617)))
(let (($x11628 (not $x11623)))
(let (($x11636 (or $x11628 $x11633)))
(let (($x10368 (<= ?x10163 v_b_L_H_max_G_3$)))
(let (($x10928 (or (not (and $x3098 (< ?0 v_b_L_H_p_G_1$))) $x10368)))
(let ((@x11622 (monotonicity @x3124 (rewrite (= (< ?0 v_b_L_H_p_G_1$) $x11617)) (= (and $x3098 (< ?0 v_b_L_H_p_G_1$)) (and (and $x2815 $x3115) $x11617)))))
(let ((@x11627 (trans @x11622 (rewrite (= (and (and $x2815 $x3115) $x11617) $x11623)) (= (and $x3098 (< ?0 v_b_L_H_p_G_1$)) $x11623))))
(let ((@x11630 (monotonicity @x11627 (= (not (and $x3098 (< ?0 v_b_L_H_p_G_1$))) $x11628))))
(let ((@x11641 (quant-intro (monotonicity @x11630 (rewrite (= $x10368 $x11633)) (= $x10928 $x11636)) (= $x10931 $x11639))))
(let ((@x11656 (monotonicity (monotonicity @x11641 (= (not $x10931) $x11642)) @x11653 (= $x10954 $x11654))))
(let ((@x11662 (monotonicity (monotonicity (rewrite (= $x10365 $x11608)) (= (not $x10365) $x11612)) (monotonicity @x11641 @x11656 (= $x10959 $x11657)) (= $x10966 $x11660))))
(let (($x11601 (= (and (and $x11570 $x11573) (and $x11580 (and $x10358 (and $x11578 $x11536)))) $x11600)))
(let (($x11598 (= $x10924 (and (and $x11570 $x11573) (and $x11580 (and $x10358 (and $x11578 $x11536)))))))
(let ((@x11587 (monotonicity (rewrite (= (<= 2 v_b_L_H_p_G_1$) $x11578)) (rewrite (= $x10341 $x11536)) (= $x10360 (and $x11578 $x11536)))))
(let ((@x11593 (monotonicity (rewrite (= $x10913 $x11580)) (monotonicity @x11587 (= $x10918 (and $x10358 (and $x11578 $x11536)))) (= $x10921 (and $x11580 (and $x10358 (and $x11578 $x11536)))))))
(let ((@x11596 (monotonicity (rewrite (= $x10904 $x11570)) (rewrite (= $x10907 $x11573)) (= $x10910 (and $x11570 $x11573)))))
(let ((@x11607 (monotonicity (trans (monotonicity @x11596 @x11593 $x11598) (rewrite $x11601) (= $x10924 $x11600)) (= (not $x10924) $x11605))))
(let ((@x11668 (monotonicity @x11607 (monotonicity (rewrite (= $x10365 $x11608)) @x11662 (= $x10971 $x11663)) (= $x10978 $x11666))))
(let ((@x11676 (trans (monotonicity @x11596 @x11668 (= $x10983 (and (and $x11570 $x11573) $x11666))) (rewrite (= (and (and $x11570 $x11573) $x11666) $x11672)) (= $x10983 $x11672))))
(let (($x11716 (and $x11434 (and $x11434 (and $x11434 (and $x10391 (and $x10392 (and $x11429 $x11536))))))))
(let (($x11714 (= $x11035 (and $x11434 (and $x11434 (and $x10391 (and $x10392 (and $x11429 $x11536))))))))
(let ((@x11540 (monotonicity @x11430 (rewrite (= $x10341 $x11536)) (= $x10342 (and $x11429 $x11536)))))
(let ((@x11709 (monotonicity (monotonicity @x11540 (= $x11019 (and $x10392 (and $x11429 $x11536)))) (= $x11022 (and $x10391 (and $x10392 (and $x11429 $x11536)))))))
(let ((@x11712 (monotonicity @x11436 @x11709 (= $x11032 (and $x11434 (and $x10391 (and $x10392 (and $x11429 $x11536))))))))
(let ((@x11721 (monotonicity (rewrite (= $x10390 $x11516)) (monotonicity @x11436 (monotonicity @x11436 @x11712 $x11714) (= $x11045 $x11716)) (= $x11048 (and $x11516 $x11716)))))
(let ((@x11729 (trans (monotonicity @x11436 @x11721 (= $x11051 (and $x11434 (and $x11516 $x11716)))) (rewrite (= (and $x11434 (and $x11516 $x11716)) $x11725)) (= $x11051 $x11725))))
(let ((@x11735 (monotonicity (monotonicity @x11729 (= (not $x11051) $x11730)) @x11676 (= $x11065 $x11733))))
(let (($x11553 (and $x10334 (and $x10335 (and $x11429 (and $x10338 (and $x10340 (and $x11429 $x11536))))))))
(let (($x11551 (= $x10889 (and $x10335 (and $x11429 (and $x10338 (and $x10340 (and $x11429 $x11536))))))))
(let ((@x11546 (monotonicity (monotonicity @x11540 (= $x10873 (and $x10340 (and $x11429 $x11536)))) (= $x10876 (and $x10338 (and $x10340 (and $x11429 $x11536)))))))
(let ((@x11549 (monotonicity @x11430 @x11546 (= $x10886 (and $x11429 (and $x10338 (and $x10340 (and $x11429 $x11536))))))))
(let ((@x11558 (monotonicity (monotonicity (monotonicity @x11549 $x11551) (= $x10892 $x11553)) (= $x10895 (and $x10333 $x11553)))))
(let ((@x11566 (trans (monotonicity @x11558 (= $x10898 (and $x10325 (and $x10333 $x11553)))) (rewrite (= (and $x10325 (and $x10333 $x11553)) $x11562)) (= $x10898 $x11562))))
(let ((@x11679 (monotonicity (monotonicity @x11566 (= (not $x10898) $x11567)) @x11676 (= $x10990 $x11677))))
(let ((@x11687 (trans (monotonicity @x11679 (= $x10995 (and $x10325 $x11677))) (rewrite (= (and $x10325 $x11677) $x11683)) (= $x10995 $x11683))))
(let ((@x11693 (monotonicity (monotonicity @x11687 (= $x11002 $x11688)) (= $x11007 (and $x10323 $x11688)))))
(let (($x10328 (< v_b_L_H_max_G_1$ ?x10327)))
(let (($x10856 (and $x10328 $x10182)))
(let (($x10859 (and $x10182 $x10856)))
(let ((@x11523 (monotonicity (rewrite (= $x10328 $x11515)) @x11436 (= $x10856 (and $x11515 $x11434)))))
(let ((@x11531 (trans (monotonicity @x11436 @x11523 (= $x10859 (and $x11434 (and $x11515 $x11434)))) (rewrite (= (and $x11434 (and $x11515 $x11434)) $x11527)) (= $x10859 $x11527))))
(let ((@x11701 (monotonicity (monotonicity @x11531 (= (not $x10859) $x11532)) (trans @x11693 (rewrite (= (and $x10323 $x11688) $x11694)) (= $x11007 $x11694)) (= $x11014 $x11699))))
(let ((@x11511 (trans (monotonicity @x11436 (= $x10326 (and $x10325 $x11434))) (rewrite (= (and $x10325 $x11434) $x11507)) (= $x10326 $x11507))))
(let ((@x11741 (monotonicity (monotonicity @x11511 (= (not $x10326) $x11512)) (monotonicity @x11701 @x11735 (= $x11070 $x11736)) (= $x11077 $x11739))))
(let ((@x11749 (trans (monotonicity @x11741 (= $x11082 (and $x10325 $x11739))) (rewrite (= (and $x10325 $x11739) $x11745)) (= $x11082 $x11745))))
(let ((@x11755 (monotonicity (monotonicity @x11749 (= $x11088 $x11750)) (= $x11093 (and $x10323 $x11750)))))
(let (($x11502 (= (not (and $x10182 (and (< v_b_L_H_p_G_0$ v_b_P_H_len$) $x10182))) $x11501)))
(let (($x10316 (< v_b_L_H_p_G_0$ v_b_P_H_len$)))
(let (($x10843 (and $x10316 $x10182)))
(let (($x10846 (and $x10182 $x10843)))
(let ((@x11492 (monotonicity (rewrite (= $x10316 $x11487)) @x11436 (= $x10843 (and $x11487 $x11434)))))
(let ((@x11500 (trans (monotonicity @x11436 @x11492 (= $x10846 (and $x11434 (and $x11487 $x11434)))) (rewrite (= (and $x11434 (and $x11487 $x11434)) $x11496)) (= $x10846 $x11496))))
(let ((@x11763 (monotonicity (monotonicity @x11500 $x11502) (trans @x11755 (rewrite (= (and $x10323 $x11750) $x11756)) (= $x11093 $x11756)) (= $x11100 $x11761))))
(let (($x11452 (and $x10205 (and $x10291 (and $x10292 (and $x10293 (and $x10294 (and $x10297 $x11434))))))))
(let (($x11458 (and true (and true $x10284))))
(let (($x11477 (= (and $x11434 (and $x11434 (and $x11434 (and $x11458 (and $x11458 $x11452))))) $x11476)))
(let (($x11474 (= $x10833 (and $x11434 (and $x11434 (and $x11434 (and $x11458 (and $x11458 $x11452))))))))
(let (($x11450 (= $x10801 (and $x10291 (and $x10292 (and $x10293 (and $x10294 (and $x10297 $x11434))))))))
(let ((@x11442 (monotonicity (monotonicity @x11436 (= $x10789 (and $x10297 $x11434))) (= $x10792 (and $x10294 (and $x10297 $x11434))))))
(let ((@x11448 (monotonicity (monotonicity @x11442 (= $x10795 (and $x10293 (and $x10294 (and $x10297 $x11434))))) (= $x10798 (and $x10292 (and $x10293 (and $x10294 (and $x10297 $x11434))))))))
(let (($x11419 (forall ((?v0 B_S_ptr$) )(! true :pattern ( (b_S_timestamp$ v_b_S_s$ ?v0) ) :qid k!704))
))
(let (($x11417 (= (<= (b_S_timestamp$ v_b_S_s$ ?0) (b_S_timestamp$ v_b_S_s$ ?0)) true)))
(let ((@x11425 (trans (quant-intro (rewrite $x11417) (= $x10283 $x11419)) (elim-unused (= $x11419 true)) (= $x10283 true))))
(let ((@x11460 (monotonicity (rewrite (= (<= ?x10111 ?x10111) true)) (monotonicity @x11425 (= (and $x10283 $x10284) (and true $x10284))) (= $x10286 $x11458))))
(let ((@x11463 (monotonicity @x11460 (monotonicity (monotonicity @x11448 $x11450) (= $x10804 $x11452)) (= $x10807 (and $x11458 $x11452)))))
(let ((@x11469 (monotonicity @x11436 (monotonicity @x11460 @x11463 (= $x10810 (and $x11458 (and $x11458 $x11452)))) (= $x10813 (and $x11434 (and $x11458 (and $x11458 $x11452)))))))
(let ((@x11472 (monotonicity @x11436 @x11469 (= $x10823 (and $x11434 (and $x11434 (and $x11458 (and $x11458 $x11452))))))))
(let ((@x11483 (monotonicity (trans (monotonicity @x11436 @x11472 $x11474) (rewrite $x11477) (= $x10833 $x11476)) (= (not $x10833) $x11481))))
(let ((@x11967 (monotonicity @x11483 (monotonicity @x11763 @x11861 (= $x11139 $x11862)) (= $x11146 (or $x11481 $x11862)))))
(let (($x11936 (and (and $x11901 $x11904) (and $x11434 (and $x11898 (and $x11895 (and (and $x11868 $x10192) $x11434)))))))
(let (($x11951 (and $x11260 $x10167)))
(let (($x11958 (= (and $x11951 (and (and $x11911 $x11914) (and (and $x11432 $x11907) $x11936))) $x11957)))
(let (($x11955 (= $x10557 (and $x11951 (and (and $x11911 $x11914) (and (and $x11432 $x11907) $x11936))))))
(let (($x11931 (= $x10538 (and $x11434 (and $x11898 (and $x11895 (and (and $x11868 $x10192) $x11434)))))))
(let (($x11919 (= (and (< v_b_SL_H_witness_G_0$ v_b_P_H_len$) $x10192) (and $x11868 $x10192))))
(let ((@x11920 (monotonicity (rewrite (= (< v_b_SL_H_witness_G_0$ v_b_P_H_len$) $x11868)) $x11919)))
(let (($x11889 (<= (+ ?x10163 (* (- 1) v_b_L_H_max_G_1$)) 0)))
(let (($x11871 (>= (+ ?0 ?x11484) 0)))
(let (($x11873 (not $x11871)))
(let (($x11879 (and $x2815 $x3115 $x11873)))
(let (($x11884 (not $x11879)))
(let (($x11892 (or $x11884 $x11889)))
(let (($x10186 (<= ?x10163 v_b_L_H_max_G_1$)))
(let (($x10526 (or (not (and $x3098 (< ?0 v_b_L_H_p_G_0$))) $x10186)))
(let ((@x11878 (monotonicity @x3124 (rewrite (= (< ?0 v_b_L_H_p_G_0$) $x11873)) (= (and $x3098 (< ?0 v_b_L_H_p_G_0$)) (and (and $x2815 $x3115) $x11873)))))
(let ((@x11883 (trans @x11878 (rewrite (= (and (and $x2815 $x3115) $x11873) $x11879)) (= (and $x3098 (< ?0 v_b_L_H_p_G_0$)) $x11879))))
(let ((@x11886 (monotonicity @x11883 (= (not (and $x3098 (< ?0 v_b_L_H_p_G_0$))) $x11884))))
(let ((@x11897 (quant-intro (monotonicity @x11886 (rewrite (= $x10186 $x11889)) (= $x10526 $x11892)) (= $x10529 $x11895))))
(let ((@x11926 (monotonicity @x11897 (monotonicity @x11920 @x11436 (= $x10194 (and (and $x11868 $x10192) $x11434))) (= $x10532 (and $x11895 (and (and $x11868 $x10192) $x11434))))))
(let ((@x11929 (monotonicity (rewrite (= $x10183 $x11898)) @x11926 (= $x10535 (and $x11898 (and $x11895 (and (and $x11868 $x10192) $x11434)))))))
(let ((@x11935 (monotonicity (rewrite (= (<= 0 v_b_L_H_p_G_0$) $x11901)) (rewrite (= (<= v_b_L_H_p_G_0$ b_S_max_o_u4$) $x11904)) (= $x10180 (and $x11901 $x11904)))))
(let ((@x11941 (monotonicity (rewrite (= $x10174 $x11432)) (rewrite (= (<= v_b_SL_H_witness_G_0$ b_S_max_o_u4$) $x11907)) (= $x10176 (and $x11432 $x11907)))))
(let ((@x11944 (monotonicity @x11941 (monotonicity @x11935 (monotonicity @x11436 @x11929 $x11931) (= $x10541 $x11936)) (= $x10544 (and (and $x11432 $x11907) $x11936)))))
(let ((@x11947 (monotonicity (rewrite (= (<= 0 v_b_L_H_max_G_1$) $x11911)) (rewrite (= (<= v_b_L_H_max_G_1$ b_S_max_o_u1$) $x11914)) (= $x10172 (and $x11911 $x11914)))))
(let ((@x11950 (monotonicity @x11947 @x11944 (= $x10547 (and (and $x11911 $x11914) (and (and $x11432 $x11907) $x11936))))))
(let ((@x11956 (monotonicity (monotonicity (rewrite (= $x10074 $x11260)) (= $x10168 $x11951)) @x11950 $x11955)))
(let ((@x11964 (monotonicity (trans @x11956 (rewrite $x11958) (= $x10557 $x11957)) (= (not $x10557) $x11962))))
(let ((@x11975 (trans (monotonicity @x11964 @x11967 (= $x11162 (or $x11962 (or $x11481 $x11862)))) (rewrite (= (or $x11962 (or $x11481 $x11862)) $x11971)) (= $x11162 $x11971))))
(let ((@x11978 (monotonicity (monotonicity (rewrite (= $x10074 $x11260)) (= $x10168 $x11951)) @x11975 (= $x11167 (and $x11951 $x11971)))))
(let (($x11404 (>= (+ v_b_L_H_max_G_0$ (* (- 1) ?x10163)) 0)))
(let (($x11388 (>= ?0 1)))
(let (($x11389 (not $x11388)))
(let (($x11395 (and $x2815 $x3115 $x11389)))
(let (($x11400 (not $x11395)))
(let (($x11408 (or $x11400 $x11404)))
(let (($x10164 (<= ?x10163 v_b_L_H_max_G_0$)))
(let (($x10519 (or (not (and $x3098 (< ?0 1))) $x10164)))
(let ((@x11394 (monotonicity @x3124 (rewrite (= (< ?0 1) $x11389)) (= (and $x3098 (< ?0 1)) (and (and $x2815 $x3115) $x11389)))))
(let ((@x11399 (trans @x11394 (rewrite (= (and (and $x2815 $x3115) $x11389) $x11395)) (= (and $x3098 (< ?0 1)) $x11395))))
(let ((@x11410 (monotonicity (monotonicity @x11399 (= (not (and $x3098 (< ?0 1))) $x11400)) (rewrite (= $x10164 $x11404)) (= $x10519 $x11408))))
(let ((@x11416 (monotonicity (quant-intro @x11410 (= $x10522 $x11411)) (= (not $x10522) $x11414))))
(let ((@x11986 (monotonicity @x11416 (trans @x11978 (rewrite (= (and $x11951 $x11971) $x11979)) (= $x11167 $x11979)) (= $x11174 $x11984))))
(let ((@x11992 (monotonicity (monotonicity (rewrite (= $x10159 $x11382)) (= (not $x10159) $x11385)) (monotonicity (quant-intro @x11410 (= $x10522 $x11411)) @x11986 (= $x11179 $x11987)) (= $x11186 $x11990))))
(let (($x11368 (and $x10145 (and $x10146 (and $x10147 (and $x10148 (and true (and true true))))))))
(let (($x11366 (= $x10509 (and $x10146 (and $x10147 (and $x10148 (and true (and true true))))))))
(let ((@x11355 (monotonicity (rewrite (= $x10149 true)) (rewrite (= $x10150 true)) (= $x10497 (and true true)))))
(let ((@x11358 (monotonicity (rewrite (= $x10149 true)) @x11355 (= $x10500 (and true (and true true))))))
(let ((@x11361 (monotonicity @x11358 (= $x10503 (and $x10148 (and true (and true true)))))))
(let ((@x11364 (monotonicity @x11361 (= $x10506 (and $x10147 (and $x10148 (and true (and true true))))))))
(let ((@x11373 (monotonicity (monotonicity (monotonicity @x11364 $x11366) (= $x10512 $x11368)) (= $x10515 (and $x10142 $x11368)))))
(let ((@x11381 (monotonicity (trans @x11373 (rewrite (= (and $x10142 $x11368) $x11374)) (= $x10515 $x11374)) (= (not $x10515) $x11379))))
(let ((@x11998 (monotonicity @x11381 (monotonicity (rewrite (= $x10159 $x11382)) @x11992 (= $x11191 $x11993)) (= $x11198 $x11996))))
(let ((@x12006 (trans (monotonicity @x11998 (= $x11203 (and $x10142 $x11996))) (rewrite (= (and $x10142 $x11996) $x12002)) (= $x11203 $x12002))))
(let ((@x12012 (monotonicity (monotonicity @x12006 (= $x11210 $x12007)) (= $x11215 (and $x10140 $x12007)))))
(let ((@x12020 (monotonicity (trans @x12012 (rewrite (= (and $x10140 $x12007) $x12013)) (= $x11215 $x12013)) (= $x11222 $x12018))))
(let (($x11306 (and $x11256 (and $x10108 (and $x10109 (and $x10112 (and $x10439 (and $x11243 $x11245))))))))
(let (($x11327 (and (and $x11268 $x11270) (and $x11264 (and $x11260 (and $x10094 (and $x10095 (and $x10098 $x11306))))))))
(let ((@x11344 (rewrite (= (and (and $x11284 $x11286) (and (and $x11276 $x11278) $x11327)) $x11342))))
(let (($x11322 (= $x10476 (and $x11264 (and $x11260 (and $x10094 (and $x10095 (and $x10098 $x11306))))))))
(let (($x11304 (= $x10451 (and $x10108 (and $x10109 (and $x10112 (and $x10439 (and $x11243 $x11245))))))))
(let ((@x11293 (monotonicity (rewrite (= (<= 0 v_b_P_H_len$) $x11243)) (rewrite (= (<= v_b_P_H_len$ b_S_max_o_u4$) $x11245)) (= $x10119 (and $x11243 $x11245)))))
(let ((@x11299 (monotonicity (monotonicity @x11293 (= $x10442 (and $x10439 (and $x11243 $x11245)))) (= $x10445 (and $x10112 (and $x10439 (and $x11243 $x11245)))))))
(let ((@x11302 (monotonicity @x11299 (= $x10448 (and $x10109 (and $x10112 (and $x10439 (and $x11243 $x11245))))))))
(let (($x11251 (>= (+ (b_S_frame_n_level$ ?0) (* (- 1) b_S_current_n_frame_n_level$)) 0)))
(let (($x11250 (not $x11251)))
(let ((@x11255 (rewrite (= (< (b_S_frame_n_level$ ?0) b_S_current_n_frame_n_level$) $x11250))))
(let ((@x11308 (monotonicity (quant-intro @x11255 (= $x10104 $x11256)) (monotonicity @x11302 $x11304) (= $x10454 $x11306))))
(let ((@x11314 (monotonicity (monotonicity @x11308 (= $x10457 (and $x10098 $x11306))) (= $x10460 (and $x10095 (and $x10098 $x11306))))))
(let ((@x11320 (monotonicity (rewrite (= $x10074 $x11260)) (monotonicity @x11314 (= $x10470 (and $x10094 (and $x10095 (and $x10098 $x11306))))) (= $x10473 (and $x11260 (and $x10094 (and $x10095 (and $x10098 $x11306))))))))
(let ((@x11326 (monotonicity (rewrite (= (<= 0 v_b_SL_H_witness$) $x11268)) (rewrite (= (<= v_b_SL_H_witness$ b_S_max_o_u4$) $x11270)) (= $x10071 (and $x11268 $x11270)))))
(let ((@x11329 (monotonicity @x11326 (monotonicity (rewrite (= $x10073 $x11264)) @x11320 $x11322) (= $x10479 $x11327))))
(let ((@x11332 (monotonicity (rewrite (= (<= 0 v_b_L_H_p$) $x11276)) (rewrite (= (<= v_b_L_H_p$ b_S_max_o_u4$) $x11278)) (= $x10067 (and $x11276 $x11278)))))
(let ((@x11338 (monotonicity (rewrite (= (<= 0 v_b_L_H_max$) $x11284)) (rewrite (= (<= v_b_L_H_max$ b_S_max_o_u1$) $x11286)) (= $x10063 (and $x11284 $x11286)))))
(let ((@x11341 (monotonicity @x11338 (monotonicity @x11332 @x11329 (= $x10482 (and (and $x11276 $x11278) $x11327))) (= $x10485 (and (and $x11284 $x11286) (and (and $x11276 $x11278) $x11327))))))
(let ((@x11349 (monotonicity (trans @x11341 @x11344 (= $x10485 $x11342)) (= (not $x10485) (not $x11342)))))
(let ((@x12026 (monotonicity @x11349 (monotonicity @x12020 (= $x11227 $x12021)) (= $x11234 (or (not $x11342) $x12021)))))
(let ((@x10656 (monotonicity (rewrite (= (=> $x10242 true) true)) (= $x10244 (and $x10242 true)))))
(let ((@x10663 (monotonicity (quant-intro (rewrite (= (=> $x10234 $x10235) $x10646)) (= $x10237 $x10649)) (trans @x10656 (rewrite (= (and $x10242 true) $x10242)) (= $x10244 $x10242)) (= $x10245 (=> $x10649 $x10242)))))
(let ((@x10672 (monotonicity (quant-intro (rewrite (= (=> $x10234 $x10235) $x10646)) (= $x10237 $x10649)) (trans @x10663 (rewrite (= (=> $x10649 $x10242) $x10665)) (= $x10245 $x10665)) (= (and $x10237 $x10245) $x10670))))
(let (($x10614 (= (and $x10218 (and $x10220 (and $x10222 true))) (and $x10218 (and $x10220 $x10222)))))
(let ((@x10612 (monotonicity (rewrite (= (and $x10222 true) $x10222)) (= (and $x10220 (and $x10222 true)) (and $x10220 $x10222)))))
(let ((@x10618 (monotonicity (monotonicity @x10612 $x10614) (= (and $x10216 (and $x10218 (and $x10220 (and $x10222 true)))) $x10616))))
(let ((@x10625 (trans (monotonicity @x10618 (= $x10227 (and true $x10616))) (rewrite (= (and true $x10616) $x10616)) (= $x10227 $x10616))))
(let ((@x10631 (monotonicity (monotonicity @x10625 (= (and $x10182 $x10227) $x10626)) (= (and $x10182 (and $x10182 $x10227)) $x10629))))
(let ((@x10638 (trans (monotonicity @x10631 (= $x10230 (and true $x10629))) (rewrite (= (and true $x10629) $x10629)) (= $x10230 $x10629))))
(let ((@x10644 (monotonicity (monotonicity @x10638 (= (and $x10182 $x10230) $x10639)) (= (and b_S_position_n_marker$ (and $x10182 $x10230)) $x10642))))
(let ((@x10681 (trans (monotonicity @x10644 @x10672 (= $x10247 (=> $x10642 $x10670))) (rewrite (= (=> $x10642 $x10670) $x10677)) (= $x10247 $x10677))))
(let (($x11117 (and $x10410 $x10182)))
(let (($x11120 (and $x10182 $x11117)))
(let ((@x10568 (rewrite (= (and $x10182 $x10182) $x10182))))
(let ((@x10563 (rewrite (= $x10206 $x10182))))
(let ((@x10570 (trans (monotonicity @x10563 (= $x10207 (and $x10182 $x10182))) @x10568 (= $x10207 $x10182))))
(let ((@x11108 (trans (monotonicity @x10570 (= $x10411 (and $x10182 $x10182))) @x10568 (= $x10411 $x10182))))
(let ((@x11114 (monotonicity (trans (monotonicity @x11108 (= $x10412 $x10206)) @x10563 (= $x10412 $x10182)) (= $x10413 (and $x10182 $x10182)))))
(let ((@x11119 (monotonicity (trans @x11114 @x10568 (= $x10413 $x10182)) (= (and $x10410 $x10413) $x11117))))
(let ((@x11125 (monotonicity (monotonicity @x11119 (= (and $x10182 (and $x10410 $x10413)) $x11120)) (= $x10416 (and true $x11120)))))
(let ((@x11132 (monotonicity (trans @x11125 (rewrite (= (and true $x11120) $x11120)) (= $x10416 $x11120)) (monotonicity @x10681 (= $x10248 $x10682)) (= $x10417 (=> $x11120 $x10682)))))
(let ((@x10938 (monotonicity (rewrite (= (and $x10375 false) false)) (= $x10377 (=> false true)))))
(let ((@x10942 (trans @x10938 (rewrite (= (=> false true) true)) (= $x10377 true))))
(let ((@x10949 (trans (monotonicity @x10942 (= $x10378 (and $x10375 true))) (rewrite (= (and $x10375 true) $x10375)) (= $x10378 $x10375))))
(let ((@x10933 (quant-intro (rewrite (= (=> (and $x3098 (< ?0 v_b_L_H_p_G_1$)) $x10368) $x10928)) (= $x10370 $x10931))))
(let ((@x10958 (trans (monotonicity @x10933 @x10949 (= $x10379 (=> $x10931 $x10375))) (rewrite (= (=> $x10931 $x10375) $x10954)) (= $x10379 $x10954))))
(let ((@x10964 (monotonicity (monotonicity @x10933 @x10958 (= (and $x10370 $x10379) $x10959)) (= $x10381 (=> $x10365 $x10959)))))
(let ((@x10973 (monotonicity (trans @x10964 (rewrite (= (=> $x10365 $x10959) $x10966)) (= $x10381 $x10966)) (= (and $x10365 $x10381) $x10971))))
(let ((@x10920 (monotonicity (rewrite (= (and $x10360 true) $x10360)) (= (and $x10358 (and $x10360 true)) $x10918))))
(let ((@x10903 (rewrite (= (+ v_b_L_H_p_G_0$ 1) ?x10901))))
(let ((@x10915 (monotonicity @x10903 (= (= v_b_L_H_p_G_1$ (+ v_b_L_H_p_G_0$ 1)) $x10913))))
(let ((@x10909 (monotonicity @x10903 (= (<= (+ v_b_L_H_p_G_0$ 1) b_S_max_o_u4$) $x10907))))
(let ((@x10912 (monotonicity (monotonicity @x10903 (= (<= 0 (+ v_b_L_H_p_G_0$ 1)) $x10904)) @x10909 (= $x10355 $x10910))))
(let ((@x10926 (monotonicity @x10912 (monotonicity @x10915 @x10920 (= $x10363 $x10921)) (= (and $x10355 $x10363) $x10924))))
(let ((@x10982 (trans (monotonicity @x10926 @x10973 (= $x10383 (=> $x10924 $x10971))) (rewrite (= (=> $x10924 $x10971) $x10978)) (= $x10383 $x10978))))
(let ((@x11021 (monotonicity (rewrite (= (and true $x10342) $x10342)) (= (and $x10392 (and true $x10342)) $x11019))))
(let ((@x11024 (monotonicity @x11021 (= (and $x10391 (and $x10392 (and true $x10342))) $x11022))))
(let ((@x11031 (trans (monotonicity @x11024 (= $x10395 (and true $x11022))) (rewrite (= (and true $x11022) $x11022)) (= $x10395 $x11022))))
(let ((@x11037 (monotonicity (monotonicity @x11031 (= (and $x10182 $x10395) $x11032)) (= (and $x10182 (and $x10182 $x10395)) $x11035))))
(let ((@x11044 (trans (monotonicity @x11037 (= $x10398 (and true $x11035))) (rewrite (= (and true $x11035) $x11035)) (= $x10398 $x11035))))
(let ((@x11050 (monotonicity (monotonicity @x11044 (= (and $x10182 $x10398) $x11045)) (= (and $x10390 (and $x10182 $x10398)) $x11048))))
(let ((@x11056 (monotonicity (monotonicity @x11050 (= (and $x10182 (and $x10390 (and $x10182 $x10398))) $x11051)) (= $x10402 (and true $x11051)))))
(let ((@x11063 (monotonicity (trans @x11056 (rewrite (= (and true $x11051) $x11051)) (= $x10402 $x11051)) (monotonicity @x10912 @x10982 (= $x10384 $x10983)) (= $x10403 (=> $x11051 $x10983)))))
(let (($x10896 (= (and $x10333 (and $x10334 (and $x10335 (and (and $x10181 $x10181) $x10346)))) $x10895)))
(let ((@x10875 (monotonicity (rewrite (= (and true $x10342) $x10342)) (= (and $x10340 (and true $x10342)) $x10873))))
(let ((@x10878 (monotonicity @x10875 (= (and $x10338 (and $x10340 (and true $x10342))) $x10876))))
(let ((@x10885 (trans (monotonicity @x10878 (= $x10346 (and true $x10876))) (rewrite (= (and true $x10876) $x10876)) (= $x10346 $x10876))))
(let ((@x10888 (monotonicity (rewrite (= (and $x10181 $x10181) $x10181)) @x10885 (= (and (and $x10181 $x10181) $x10346) $x10886))))
(let ((@x10894 (monotonicity (monotonicity @x10888 (= (and $x10335 (and (and $x10181 $x10181) $x10346)) $x10889)) (= (and $x10334 (and $x10335 (and (and $x10181 $x10181) $x10346))) $x10892))))
--> --------------------
--> maximum size reached
--> --------------------
[ Verzeichnis aufwärts0.405unsichere Verbindung
]
