// Testfile dumped by Ultimate at 2015/06/08 22:53:13 // // print(loopComplexity(Abstraction1)); NestedWordAutomaton Abstraction1 = ( callAlphabet = {}, internalAlphabet = {"assume ssl3_connect_~ret~3 <= 0;" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4528;ssl3_connect_~s__init_num~3 := 0;ssl3_connect_~s__session__cipher~3 := ssl3_connect_~s__s3__tmp__new_cipher~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__new_compression~3 == 0;ssl3_connect_~s__session__compress_meth~3 := 0;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__new_compression~3 == 0);ssl3_connect_~s__session__compress_meth~3 := ssl3_connect_~s__s3__tmp__new_compression__id~3;}EndParallelComposition" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__state~3 := 4512;ParallelCodeBlock1: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__state~3 := 3;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "assume ssl3_connect_~s__state~3 == 4352;ssl3_connect_~__cil_tmp61~3 := ssl3_connect_~num1~3;" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__state~3 := 4560;ParallelCodeBlock1: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__state~3 := 4400;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~l~3 := ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__cert_req~3 == 1;ssl3_connect_~s__state~3 := 4496;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__cert_req~3 == 1);ssl3_connect_~s__state~3 := 4512;ssl3_connect_~s__s3__change_cipher_spec~3 := 0;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "assume ssl3_connect_~ret~3 <= 0;" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet35;havoc ssl3_connect_#t~nondet35;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 3;ssl3_connect_~blastFlag~3 := 4;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 3);}EndParallelComposition" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__cert_req~3 != 0;ssl3_connect_~s__state~3 := 4464;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__cert_req~3 != 0);ssl3_connect_~s__state~3 := 4480;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet33;havoc ssl3_connect_#t~nondet33;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 1;ssl3_connect_~blastFlag~3 := 2;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 1);}EndParallelComposition" "assume true;" "assume !(ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3 - 256 != 0);ssl3_connect_~ret~3 := ssl3_connect_#t~nondet34;havoc ssl3_connect_#t~nondet34;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 2;ssl3_connect_~blastFlag~3 := 3;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 2);}EndParallelComposition" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4384;ssl3_connect_~s__init_num~3 := 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__bbio~3 != ssl3_connect_~s__wbio~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__bbio~3 != ssl3_connect_~s__wbio~3);}EndParallelComposition" "assume !!(ssl3_connect_~skip~3 != 0);" "assume !!(ssl3_connect_~s__s3__tmp__reuse_message~3 != 0);" "assume !true;" "assume !(ssl3_connect_~s__state~3 == 12292);" "assume ssl3_connect_~s__state~3 == 12292;" "assume ssl3_connect_~ret~3 <= 0;" "assume !(ssl3_connect_~s__state~3 == 16384);" "ssl3_connect_~skip~3 := 0;" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4432;ssl3_connect_~s__init_num~3 := 0;" "assume !(ssl3_connect_~tmp___6~3 != 0);ssl3_connect_~ret~3 := -1;" "assume !true;" "assume ssl3_connect_~s__state~3 == 16384;" "assume ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3 - 256 != 0;ssl3_connect_~skip~3 := 1;" "assume ssl3_connect_~s__state~3 == 4096;" "assume true;ssl3_connect_#res := -1;" "assume !false;" "assume ssl3_connect_~s__state~3 == 20480;" "assume !(ssl3_connect_~s__state~3 == 4096);" "assume !(ssl3_connect_~s__state~3 == 20480);" "main_#t~ret48 := ssl3_connect_#res;havoc main_#t~ret48;main_#res := 0;#t~ret49 := main_#res;assume true;" "assume !!true;ssl3_connect_~state~3 := ssl3_connect_~s__state~3;" "assume ssl3_connect_~ret~3 <= 0;" "assume !(ssl3_connect_~ret~3 <= 0);" "assume !(ssl3_connect_~s__state~3 == 4099);" "ssl3_connect_~s__state~3 := 4416;ssl3_connect_~s__init_num~3 := 0;" "assume ssl3_connect_~s__state~3 == 4099;" "#NULL.base, #NULL.offset := 0, 0;havoc main_#res;havoc main_#t~ret48, main_~s~142;havoc main_~s~142;main_~s~142 := 12292;ssl3_connect_#in~initial_state := 12292;havoc ssl3_connect_#res;havoc ssl3_connect_#t~nondet0, ssl3_connect_#t~nondet1, ssl3_connect_#t~nondet2, ssl3_connect_#t~nondet3, ssl3_connect_#t~nondet4, ssl3_connect_#t~nondet5, ssl3_connect_#t~nondet6, ssl3_connect_#t~nondet7, ssl3_connect_#t~nondet8, ssl3_connect_#t~nondet9, ssl3_connect_#t~nondet10, ssl3_connect_#t~nondet11, ssl3_connect_#t~nondet12, ssl3_connect_#t~nondet13, ssl3_connect_#t~nondet14, ssl3_connect_#t~nondet15, ssl3_connect_#t~nondet16, ssl3_connect_#t~nondet17, ssl3_connect_#t~nondet18, ssl3_connect_#t~nondet19, ssl3_connect_#t~nondet20, ssl3_connect_#t~nondet21, ssl3_connect_#t~nondet22, ssl3_connect_#t~nondet23, ssl3_connect_#t~nondet24, ssl3_connect_#t~nondet25, ssl3_connect_#t~nondet26, ssl3_connect_#t~nondet27, ssl3_connect_#t~post28, ssl3_connect_#t~post29, ssl3_connect_#t~nondet30, ssl3_connect_#t~post31, ssl3_connect_#t~nondet32, ssl3_connect_#t~nondet33, ssl3_connect_#t~nondet34, ssl3_connect_#t~nondet35, ssl3_connect_#t~nondet36, ssl3_connect_#t~nondet37, ssl3_connect_#t~nondet38, ssl3_connect_#t~nondet39, ssl3_connect_#t~nondet40, ssl3_connect_#t~nondet41, ssl3_connect_#t~nondet42, ssl3_connect_#t~nondet43, ssl3_connect_#t~post44, ssl3_connect_#t~post45, ssl3_connect_#t~nondet46, ssl3_connect_#t~post47, ssl3_connect_~initial_state, ssl3_connect_~s__info_callback~3, ssl3_connect_~s__in_handshake~3, ssl3_connect_~s__state~3, ssl3_connect_~s__new_session~3, ssl3_connect_~s__server~3, ssl3_connect_~s__version~3, ssl3_connect_~s__type~3, ssl3_connect_~s__init_num~3, ssl3_connect_~s__bbio~3, ssl3_connect_~s__wbio~3, ssl3_connect_~s__hit~3, ssl3_connect_~s__rwstate~3, ssl3_connect_~s__init_buf___0~3, ssl3_connect_~s__debug~3, ssl3_connect_~s__shutdown~3, ssl3_connect_~s__ctx__info_callback~3, ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3, ssl3_connect_~s__ctx__stats__sess_connect~3, ssl3_connect_~s__ctx__stats__sess_hit~3, ssl3_connect_~s__ctx__stats__sess_connect_good~3, ssl3_connect_~s__s3__change_cipher_spec~3, ssl3_connect_~s__s3__flags~3, ssl3_connect_~s__s3__delay_buf_pop_ret~3, ssl3_connect_~s__s3__tmp__cert_req~3, ssl3_connect_~s__s3__tmp__new_compression~3, ssl3_connect_~s__s3__tmp__reuse_message~3, ssl3_connect_~s__s3__tmp__new_cipher~3, ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3, ssl3_connect_~s__s3__tmp__next_state___0~3, ssl3_connect_~s__s3__tmp__new_compression__id~3, ssl3_connect_~s__session__cipher~3, ssl3_connect_~s__session__compress_meth~3, ssl3_connect_~buf~3, ssl3_connect_~tmp~3, ssl3_connect_~l~3, ssl3_connect_~num1~3, ssl3_connect_~cb~3, ssl3_connect_~ret~3, ssl3_connect_~new_state~3, ssl3_connect_~state~3, ssl3_connect_~skip~3, ssl3_connect_~tmp___0~3, ssl3_connect_~tmp___1~3, ssl3_connect_~tmp___2~3, ssl3_connect_~tmp___3~3, ssl3_connect_~tmp___4~3, ssl3_connect_~tmp___5~3, ssl3_connect_~tmp___6~3, ssl3_connect_~tmp___7~3, ssl3_connect_~tmp___8~3, ssl3_connect_~tmp___9~3, ssl3_connect_~blastFlag~3, ssl3_connect_~__cil_tmp55~3, ssl3_connect_~__cil_tmp56~3, ssl3_connect_~__cil_tmp57~3, ssl3_connect_~__cil_tmp58~3, ssl3_connect_~__cil_tmp59~3, ssl3_connect_~__cil_tmp60~3, ssl3_connect_~__cil_tmp61~3, ssl3_connect_~__cil_tmp62~3, ssl3_connect_~__cil_tmp63~3, ssl3_connect_~__cil_tmp64~3;ssl3_connect_~initial_state := ssl3_connect_#in~initial_state;ssl3_connect_~s__info_callback~3 := ssl3_connect_#t~nondet0;havoc ssl3_connect_#t~nondet0;ssl3_connect_~s__in_handshake~3 := ssl3_connect_#t~nondet1;havoc ssl3_connect_#t~nondet1;havoc ssl3_connect_~s__state~3;havoc ssl3_connect_~s__new_session~3;havoc ssl3_connect_~s__server~3;ssl3_connect_~s__version~3 := ssl3_connect_#t~nondet2;havoc ssl3_connect_#t~nondet2;havoc ssl3_connect_~s__type~3;havoc ssl3_connect_~s__init_num~3;ssl3_connect_~s__bbio~3 := ssl3_connect_#t~nondet3;havoc ssl3_connect_#t~nondet3;ssl3_connect_~s__wbio~3 := ssl3_connect_#t~nondet4;havoc ssl3_connect_#t~nondet4;ssl3_connect_~s__hit~3 := ssl3_connect_#t~nondet5;havoc ssl3_connect_#t~nondet5;havoc ssl3_connect_~s__rwstate~3;havoc ssl3_connect_~s__init_buf___0~3;ssl3_connect_~s__debug~3 := ssl3_connect_#t~nondet6;havoc ssl3_connect_#t~nondet6;havoc ssl3_connect_~s__shutdown~3;ssl3_connect_~s__ctx__info_callback~3 := ssl3_connect_#t~nondet7;havoc ssl3_connect_#t~nondet7;ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3 := ssl3_connect_#t~nondet8;havoc ssl3_connect_#t~nondet8;ssl3_connect_~s__ctx__stats__sess_connect~3 := ssl3_connect_#t~nondet9;havoc ssl3_connect_#t~nondet9;ssl3_connect_~s__ctx__stats__sess_hit~3 := ssl3_connect_#t~nondet10;havoc ssl3_connect_#t~nondet10;ssl3_connect_~s__ctx__stats__sess_connect_good~3 := ssl3_connect_#t~nondet11;havoc ssl3_connect_#t~nondet11;havoc ssl3_connect_~s__s3__change_cipher_spec~3;havoc ssl3_connect_~s__s3__flags~3;havoc ssl3_connect_~s__s3__delay_buf_pop_ret~3;ssl3_connect_~s__s3__tmp__cert_req~3 := ssl3_connect_#t~nondet12;havoc ssl3_connect_#t~nondet12;ssl3_connect_~s__s3__tmp__new_compression~3 := ssl3_connect_#t~nondet13;havoc ssl3_connect_#t~nondet13;ssl3_connect_~s__s3__tmp__reuse_message~3 := ssl3_connect_#t~nondet14;havoc ssl3_connect_#t~nondet14;ssl3_connect_~s__s3__tmp__new_cipher~3 := ssl3_connect_#t~nondet15;havoc ssl3_connect_#t~nondet15;ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3 := ssl3_connect_#t~nondet16;havoc ssl3_connect_#t~nondet16;havoc ssl3_connect_~s__s3__tmp__next_state___0~3;ssl3_connect_~s__s3__tmp__new_compression__id~3 := ssl3_connect_#t~nondet17;havoc ssl3_connect_#t~nondet17;havoc ssl3_connect_~s__session__cipher~3;havoc ssl3_connect_~s__session__compress_meth~3;havoc ssl3_connect_~buf~3;havoc ssl3_connect_~tmp~3;havoc ssl3_connect_~l~3;havoc ssl3_connect_~num1~3;havoc ssl3_connect_~cb~3;havoc ssl3_connect_~ret~3;havoc ssl3_connect_~new_state~3;havoc ssl3_connect_~state~3;havoc ssl3_connect_~skip~3;havoc ssl3_connect_~tmp___0~3;ssl3_connect_~tmp___1~3 := ssl3_connect_#t~nondet18;havoc ssl3_connect_#t~nondet18;ssl3_connect_~tmp___2~3 := ssl3_connect_#t~nondet19;havoc ssl3_connect_#t~nondet19;ssl3_connect_~tmp___3~3 := ssl3_connect_#t~nondet20;havoc ssl3_connect_#t~nondet20;ssl3_connect_~tmp___4~3 := ssl3_connect_#t~nondet21;havoc ssl3_connect_#t~nondet21;ssl3_connect_~tmp___5~3 := ssl3_connect_#t~nondet22;havoc ssl3_connect_#t~nondet22;ssl3_connect_~tmp___6~3 := ssl3_connect_#t~nondet23;havoc ssl3_connect_#t~nondet23;ssl3_connect_~tmp___7~3 := ssl3_connect_#t~nondet24;havoc ssl3_connect_#t~nondet24;ssl3_connect_~tmp___8~3 := ssl3_connect_#t~nondet25;havoc ssl3_connect_#t~nondet25;ssl3_connect_~tmp___9~3 := ssl3_connect_#t~nondet26;havoc ssl3_connect_#t~nondet26;havoc ssl3_connect_~blastFlag~3;havoc ssl3_connect_~__cil_tmp55~3;havoc ssl3_connect_~__cil_tmp56~3;havoc ssl3_connect_~__cil_tmp57~3;havoc ssl3_connect_~__cil_tmp58~3;havoc ssl3_connect_~__cil_tmp59~3;havoc ssl3_connect_~__cil_tmp60~3;havoc ssl3_connect_~__cil_tmp61~3;havoc ssl3_connect_~__cil_tmp62~3;havoc ssl3_connect_~__cil_tmp63~3;havoc ssl3_connect_~__cil_tmp64~3;ssl3_connect_~s__state~3 := ssl3_connect_~initial_state;ssl3_connect_~blastFlag~3 := 0;ssl3_connect_~tmp~3 := ssl3_connect_#t~nondet27;havoc ssl3_connect_#t~nondet27;ssl3_connect_~cb~3 := 0;ssl3_connect_~ret~3 := -1;ssl3_connect_~skip~3 := 0;ssl3_connect_~tmp___0~3 := 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__info_callback~3 != 0;ssl3_connect_~cb~3 := ssl3_connect_~s__info_callback~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__info_callback~3 != 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__ctx__info_callback~3 != 0;ssl3_connect_~cb~3 := ssl3_connect_~s__ctx__info_callback~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__ctx__info_callback~3 != 0);}EndParallelComposition}EndParallelCompositionssl3_connect_#t~post28 := ssl3_connect_~s__in_handshake~3;ssl3_connect_~s__in_handshake~3 := ssl3_connect_#t~post28 + 1;havoc ssl3_connect_#t~post28;BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~tmp___1~3 - 12288 != 0);ParallelCodeBlock1: assume ssl3_connect_~tmp___1~3 - 12288 != 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~tmp___2~3 - 16384 != 0;ParallelCodeBlock1: assume !(ssl3_connect_~tmp___2~3 - 16384 != 0);}EndParallelComposition}EndParallelComposition" "assume ssl3_connect_~s__state~3 == 4369;" "assume ssl3_connect_~s__state~3 == 4368;" "assume !(ssl3_connect_~s__state~3 == 4368);" "assume !(ssl3_connect_~s__state~3 == 4384);" "assume !(ssl3_connect_~s__state~3 == 4369);" "assume ssl3_connect_~s__state~3 == 4384;" "assume ssl3_connect_~ret~3 <= 0;" "assume ssl3_connect_~blastFlag~3 == 5;" "assume ssl3_connect_~s__state~3 == 4400;" "assume !(ssl3_connect_~s__state~3 == 4400);" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet36;havoc ssl3_connect_#t~nondet36;" "assume ssl3_connect_~s__state~3 == 4385;" "assume !!(ssl3_connect_~tmp___6~3 != 0);" "assume !(ssl3_connect_~s__state~3 == 4385);" "assume !(ssl3_connect_~s__state~3 == 4401);" "assume ssl3_connect_~s__state~3 == 4416;" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4448;ssl3_connect_~s__init_num~3 := 0;" "assume ssl3_connect_~ret~3 <= 0;" "assume !(ssl3_connect_~blastFlag~3 == 5);" "assume ssl3_connect_~s__state~3 == 4401;" "assume !(ssl3_connect_~s__state~3 == 4417);" "assume ssl3_connect_~s__state~3 == 4417;" "BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~cb~3 != 0);ParallelCodeBlock1: assume ssl3_connect_~cb~3 != 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__state~3 != ssl3_connect_~state~3;ssl3_connect_~new_state~3 := ssl3_connect_~s__state~3;ssl3_connect_~s__state~3 := ssl3_connect_~state~3;ssl3_connect_~s__state~3 := ssl3_connect_~new_state~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__state~3 != ssl3_connect_~state~3);}EndParallelComposition}EndParallelComposition" "assume !(ssl3_connect_~s__state~3 == 4416);" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4512;ssl3_connect_~s__init_num~3 := 0;ssl3_connect_~s__s3__change_cipher_spec~3 := 0;" "ssl3_connect_~s__server~3 := 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~cb~3 != 0;ParallelCodeBlock1: assume !(ssl3_connect_~cb~3 != 0);}EndParallelCompositionssl3_connect_~__cil_tmp55~3 := ssl3_connect_~s__version~3 - 65280;" "assume ssl3_connect_~s__state~3 == 4433;" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet41;havoc ssl3_connect_#t~nondet41;" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4352;ssl3_connect_~__cil_tmp56~3 := ssl3_connect_~s__s3__flags~3;ssl3_connect_~__cil_tmp57~3 := ssl3_connect_~__cil_tmp56~3 + 5;ssl3_connect_~s__s3__flags~3 := ssl3_connect_~__cil_tmp57~3;BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__s3__tmp__next_state___0~3 := 4560;ParallelCodeBlock1: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__s3__tmp__next_state___0~3 := 3;ssl3_connect_~__cil_tmp58~3 := ssl3_connect_~s__s3__flags~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~__cil_tmp58~3 - 2 != 0;ssl3_connect_~s__state~3 := 3;ssl3_connect_~__cil_tmp59~3 := ssl3_connect_~s__s3__flags~3;ssl3_connect_~__cil_tmp60~3 := ssl3_connect_~__cil_tmp59~3 + 4;ssl3_connect_~s__s3__flags~3 := ssl3_connect_~__cil_tmp60~3;ssl3_connect_~s__s3__delay_buf_pop_ret~3 := 0;ParallelCodeBlock1: assume !(ssl3_connect_~__cil_tmp58~3 - 2 != 0);}EndParallelComposition}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "ssl3_connect_~s__shutdown~3 := 0;ssl3_connect_~ret~3 := ssl3_connect_#t~nondet32;havoc ssl3_connect_#t~nondet32;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 0;ssl3_connect_~blastFlag~3 := 1;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 0);}EndParallelComposition" "assume !(ssl3_connect_~s__state~3 == 4432);" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet40;havoc ssl3_connect_#t~nondet40;" "assume ssl3_connect_~ret~3 <= 0;" "assume ssl3_connect_~s__state~3 == 4432;" "assume ssl3_connect_~ret~3 <= 0;" "assume !(ssl3_connect_~s__state~3 == 4448);" "assume ssl3_connect_~s__state~3 == 4448;" "ssl3_connect_#t~post47 := ssl3_connect_~s__in_handshake~3;ssl3_connect_~s__in_handshake~3 := ssl3_connect_#t~post47 - 1;havoc ssl3_connect_#t~post47;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~cb~3 != 0;ParallelCodeBlock1: assume !(ssl3_connect_~cb~3 != 0);}EndParallelCompositionssl3_connect_#res := ssl3_connect_~ret~3;" "assume !(ssl3_connect_~s__state~3 == 4433);" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet37;havoc ssl3_connect_#t~nondet37;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 4;ssl3_connect_~blastFlag~3 := 5;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 4);}EndParallelComposition" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet38;havoc ssl3_connect_#t~nondet38;" "assume !(ssl3_connect_~s__state~3 == 4464);" "assume ssl3_connect_~ret~3 <= 0;" "assume ssl3_connect_~s__state~3 == 4464;" "assume !(ssl3_connect_~s__state~3 == 4352);BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~s__state~3 == 3);ssl3_connect_~ret~3 := -1;ParallelCodeBlock1: assume ssl3_connect_~s__state~3 == 3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__init_buf___0~3 != 0;ssl3_connect_~s__init_buf___0~3 := 0;ParallelCodeBlock1: assume !(ssl3_connect_~s__init_buf___0~3 != 0);}EndParallelCompositionssl3_connect_~__cil_tmp63~3 := ssl3_connect_~s__s3__flags~3;ssl3_connect_~__cil_tmp64~3 := ssl3_connect_~__cil_tmp63~3 - 4;BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~__cil_tmp64~3 != 0);ParallelCodeBlock1: assume !!(ssl3_connect_~__cil_tmp64~3 != 0);}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;ssl3_connect_~s__new_session~3 := 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_#t~post44 := ssl3_connect_~s__ctx__stats__sess_hit~3;ssl3_connect_~s__ctx__stats__sess_hit~3 := ssl3_connect_#t~post44 + 1;havoc ssl3_connect_#t~post44;ParallelCodeBlock1: assume !(ssl3_connect_~s__hit~3 != 0);}EndParallelCompositionssl3_connect_~ret~3 := 1;ssl3_connect_#t~post45 := ssl3_connect_~s__ctx__stats__sess_connect_good~3;ssl3_connect_~s__ctx__stats__sess_connect_good~3 := ssl3_connect_#t~post45 + 1;havoc ssl3_connect_#t~post45;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~cb~3 != 0;ParallelCodeBlock1: assume !(ssl3_connect_~cb~3 != 0);}EndParallelComposition}EndParallelComposition" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4480;ssl3_connect_~s__init_num~3 := 0;" "assume !(ssl3_connect_~s__state~3 == 4449);" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet39;havoc ssl3_connect_#t~nondet39;" "assume ssl3_connect_~s__state~3 == 4449;" "assume !(ssl3_connect_~s__state~3 == 4466);" "assume ssl3_connect_~ret~3 <= 0;" "assume ssl3_connect_~s__state~3 == 4467;" "assume !(ssl3_connect_~s__state~3 == 4467);" "assume !(ssl3_connect_~tmp___8~3 != 0);ssl3_connect_~ret~3 := -1;" "assume ssl3_connect_~s__state~3 == 4465;" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet42;havoc ssl3_connect_#t~nondet42;" "assume !(ssl3_connect_~s__state~3 == 4465);" "assume !!(ssl3_connect_~tmp___8~3 != 0);" "assume ssl3_connect_~s__state~3 == 4466;" "assume !(ssl3_connect_~s__state~3 == 4481);" "assume ssl3_connect_~s__state~3 == 4496;" "assume !!(ssl3_connect_~tmp___7~3 != 0);" "assume !(ssl3_connect_~s__state~3 == 4496);" "assume !(ssl3_connect_~tmp___7~3 != 0);ssl3_connect_~ret~3 := -1;" "assume ssl3_connect_~s__state~3 == 4480;" "assume ssl3_connect_~ret~3 <= 0;" "assume !(ssl3_connect_~s__state~3 == 4480);" "assume ssl3_connect_~s__state~3 == 4481;" "assume ssl3_connect_~s__state~3 == 4513;" "assume ssl3_connect_~__cil_tmp61~3 > 0;ssl3_connect_~s__rwstate~3 := 2;ssl3_connect_~num1~3 := ssl3_connect_~tmp___9~3;ssl3_connect_~__cil_tmp62~3 := ssl3_connect_~num1~3;" "assume ssl3_connect_~s__state~3 == 4528;" "assume ssl3_connect_~__cil_tmp62~3 <= 0;ssl3_connect_~ret~3 := -1;" "assume !(ssl3_connect_~s__state~3 == 4513);" "assume !(ssl3_connect_~s__state~3 == 4497);" "assume ssl3_connect_~s__state~3 == 4497;" "assume !(ssl3_connect_~s__state~3 == 4512);" "assume ssl3_connect_~s__state~3 == 4512;" "assume !(ssl3_connect_~s__state~3 == 4560);" "assume ssl3_connect_~s__state~3 == 4560;" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet43;havoc ssl3_connect_#t~nondet43;" "assume ssl3_connect_~ret~3 <= 0;" "assume ssl3_connect_~s__state~3 == 4561;" "assume !(ssl3_connect_~s__state~3 == 4528);" "assume !(ssl3_connect_~s__state~3 == 4529);" "assume ssl3_connect_~s__state~3 == 4529;" "ssl3_connect_~s__new_session~3 := 1;ssl3_connect_~s__state~3 := 4096;ssl3_connect_#t~post29 := ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3;ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3 := ssl3_connect_#t~post29 + 1;havoc ssl3_connect_#t~post29;" "assume !(ssl3_connect_~s__state~3 == 4561);" "assume ssl3_connect_~s__init_buf___0~3 == 0;ssl3_connect_~buf~3 := ssl3_connect_#t~nondet30;havoc ssl3_connect_#t~nondet30;" "assume ssl3_connect_~__cil_tmp55~3 != 768;ssl3_connect_~ret~3 := -1;" "assume !(ssl3_connect_~__cil_tmp55~3 != 768);ssl3_connect_~s__type~3 := 4096;" "ssl3_connect_~s__state~3 := ssl3_connect_~s__s3__tmp__next_state___0~3;" "assume !(ssl3_connect_~__cil_tmp61~3 > 0);" "assume !(ssl3_connect_~__cil_tmp62~3 <= 0);ssl3_connect_~s__rwstate~3 := 1;" "assume !(ssl3_connect_~tmp___4~3 != 0);ssl3_connect_~ret~3 := -1;" "assume !(ssl3_connect_~s__init_buf___0~3 == 0);" "assume !!(ssl3_connect_~tmp___3~3 != 0);ssl3_connect_~s__init_buf___0~3 := ssl3_connect_~buf~3;" "assume !(ssl3_connect_~tmp___3~3 != 0);ssl3_connect_~ret~3 := -1;" "assume !(ssl3_connect_~s__debug~3 != 0);" "assume !(ssl3_connect_~buf~3 == 0);" "assume ssl3_connect_~ret~3 <= 0;" "assume ssl3_connect_~buf~3 == 0;ssl3_connect_~ret~3 := -1;" "assume !(ssl3_connect_~ret~3 <= 0);" "assume ssl3_connect_~s__debug~3 != 0;ssl3_connect_~ret~3 := ssl3_connect_#t~nondet46;havoc ssl3_connect_#t~nondet46;" "assume !(ssl3_connect_~s__s3__tmp__reuse_message~3 != 0);" "assume !(ssl3_connect_~skip~3 != 0);" "assume !!(ssl3_connect_~tmp___5~3 != 0);ssl3_connect_~s__state~3 := 4368;ssl3_connect_#t~post31 := ssl3_connect_~s__ctx__stats__sess_connect~3;ssl3_connect_~s__ctx__stats__sess_connect~3 := ssl3_connect_#t~post31 + 1;havoc ssl3_connect_#t~post31;ssl3_connect_~s__init_num~3 := 0;" "assume !(ssl3_connect_~tmp___5~3 != 0);ssl3_connect_~ret~3 := -1;" "assume !!(ssl3_connect_~tmp___4~3 != 0);" }, returnAlphabet = {}, states = {"550#L348''" "551#L549" "548#L499" "549#L437''" "546#L593" "547#L409" "544#L713" "545#L717" "558#L370'" "559#L239" "556#L463" "557#L538" "554#L424" "555#L476" "552#L612''" "553#L307" "567#L218" "566#L222" "565#L226" "564#L167" "563#L230" "562#L396''" "561#L238" "560#L234" "575#L186" "574#L190" "573#L194" "572#L198" "571#L202" "570#L206" "569#L210" "568#L214" "516#L134" "517#L463" "518#L348''" "519#L409" "512#L194" "513#L239" "514#L499" "515#L207" "524#L170" "525#L166" "526#L162" "527#L158" "520#L162" "521#L420" "522#L175" "523#L174" "533#L134" "532#L138" "535#L126" "534#L130" "529#L150" "528#L154" "531#L142" "530#L146" "541#L711" "540#L709" "543#L713''" "542#L673" "537#L118" "536#L122" "539#L113''" "538#L113" "576#L182" "577#L178" "578#L524''" "579#L514" "580#L223" "581#L199" "582#L207" "583#L282''" "584#L282" "585#L292" "586#L286" "587#L273" "588#L215" "589#L259" "590#L119" "591#L231" "593#L377''" "592#L159" "595#L621" "594#L612" "597#L242" "596#L183" "598#L151" "440#L150" "441#L222" "442#L421" "443#L420" "444#L113" "445#L166" "446#L514" "447#L259" "438#L223" "439#L151" "478#L182" "479#L210" "476#L621" "477#L154" "474#L292" "475#L183" "472#L282''" "473#L713" "470#L326''" "471#L186" "468#L713''" "469#L158" "466#L612" "467#L113''" "464#ULTIMATE.startErr0AssertViolation" "465#L159" "463#L612''" "462#L437''" "461#L377''" "460#ULTIMATE.startENTRY" "459#L215" "458#L538" "457#L122" "456#L214" "455#L118" "454#L709" "453#L476" "452#L226" "451#L282" "450#L424" "449#L307" "448#L167" "508#L119" "509#L593" "510#L231" "511#L238" "504#L230" "505#L175" "506#L286" "507#L273" "500#L524''" "501#L234" "502#L190" "503#L138" "496#L170" "497#L143" "498#L370'" "499#L178" "493#L711" "492#L174" "495#L673" "494#L142" "489#L549" "488#L130" "491#L146" "490#L218" "485#L202" "484#L206" "487#L396''" "486#L198" "481#L126" "480#L717" "483#L242" "482#L199" }, initialStates = {"460#ULTIMATE.startENTRY" }, finalStates = {"464#ULTIMATE.startErr0AssertViolation" }, callTransitions = { }, internalTransitions = { ("550#L348''" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__state~3 := 4560;ParallelCodeBlock1: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__state~3 := 4400;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "542#L673") ("551#L549" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4352;ssl3_connect_~__cil_tmp56~3 := ssl3_connect_~s__s3__flags~3;ssl3_connect_~__cil_tmp57~3 := ssl3_connect_~__cil_tmp56~3 + 5;ssl3_connect_~s__s3__flags~3 := ssl3_connect_~__cil_tmp57~3;BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__s3__tmp__next_state___0~3 := 4560;ParallelCodeBlock1: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__s3__tmp__next_state___0~3 := 3;ssl3_connect_~__cil_tmp58~3 := ssl3_connect_~s__s3__flags~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~__cil_tmp58~3 - 2 != 0;ssl3_connect_~s__state~3 := 3;ssl3_connect_~__cil_tmp59~3 := ssl3_connect_~s__s3__flags~3;ssl3_connect_~__cil_tmp60~3 := ssl3_connect_~__cil_tmp59~3 + 4;ssl3_connect_~s__s3__flags~3 := ssl3_connect_~__cil_tmp60~3;ssl3_connect_~s__s3__delay_buf_pop_ret~3 := 0;ParallelCodeBlock1: assume !(ssl3_connect_~__cil_tmp58~3 - 2 != 0);}EndParallelComposition}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "542#L673") ("548#L499" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4512;ssl3_connect_~s__init_num~3 := 0;ssl3_connect_~s__s3__change_cipher_spec~3 := 0;" "542#L673") ("549#L437''" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__cert_req~3 != 0;ssl3_connect_~s__state~3 := 4464;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__cert_req~3 != 0);ssl3_connect_~s__state~3 := 4480;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "542#L673") ("546#L593" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__state~3 := 4512;ParallelCodeBlock1: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__state~3 := 3;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "542#L673") ("547#L409" "assume !!(ssl3_connect_~tmp___6~3 != 0);" "542#L673") ("544#L713" "assume ssl3_connect_~s__debug~3 != 0;ssl3_connect_~ret~3 := ssl3_connect_#t~nondet46;havoc ssl3_connect_#t~nondet46;" "545#L717") ("544#L713" "assume !(ssl3_connect_~s__debug~3 != 0);" "543#L713''") ("545#L717" "assume !(ssl3_connect_~ret~3 <= 0);" "543#L713''") ("558#L370'" "ssl3_connect_~s__state~3 := 4416;ssl3_connect_~s__init_num~3 := 0;" "542#L673") ("559#L239" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet43;havoc ssl3_connect_#t~nondet43;" "509#L593") ("556#L463" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4480;ssl3_connect_~s__init_num~3 := 0;" "542#L673") ("557#L538" "assume !!(ssl3_connect_~tmp___8~3 != 0);" "542#L673") ("554#L424" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4448;ssl3_connect_~s__init_num~3 := 0;" "542#L673") ("555#L476" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~l~3 := ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__cert_req~3 == 1;ssl3_connect_~s__state~3 := 4496;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__cert_req~3 == 1);ssl3_connect_~s__state~3 := 4512;ssl3_connect_~s__s3__change_cipher_spec~3 := 0;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "542#L673") ("552#L612''" "ssl3_connect_~s__state~3 := ssl3_connect_~s__s3__tmp__next_state___0~3;" "542#L673") ("553#L307" "assume !!(ssl3_connect_~tmp___5~3 != 0);ssl3_connect_~s__state~3 := 4368;ssl3_connect_#t~post31 := ssl3_connect_~s__ctx__stats__sess_connect~3;ssl3_connect_~s__ctx__stats__sess_connect~3 := ssl3_connect_#t~post31 + 1;havoc ssl3_connect_#t~post31;ssl3_connect_~s__init_num~3 := 0;" "542#L673") ("567#L218" "assume !(ssl3_connect_~s__state~3 == 4512);" "566#L222") ("567#L218" "assume ssl3_connect_~s__state~3 == 4512;" "438#L223") ("566#L222" "assume ssl3_connect_~s__state~3 == 4513;" "438#L223") ("566#L222" "assume !(ssl3_connect_~s__state~3 == 4513);" "565#L226") ("565#L226" "assume ssl3_connect_~s__state~3 == 4528;" "591#L231") ("565#L226" "assume !(ssl3_connect_~s__state~3 == 4528);" "563#L230") ("564#L167" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet35;havoc ssl3_connect_#t~nondet35;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 3;ssl3_connect_~blastFlag~3 := 4;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 3);}EndParallelComposition" "562#L396''") ("563#L230" "assume !(ssl3_connect_~s__state~3 == 4529);" "560#L234") ("563#L230" "assume ssl3_connect_~s__state~3 == 4529;" "591#L231") ("562#L396''" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4432;ssl3_connect_~s__init_num~3 := 0;" "547#L409") ("561#L238" "assume ssl3_connect_~s__state~3 == 4561;" "559#L239") ("561#L238" "assume !(ssl3_connect_~s__state~3 == 4561);" "597#L242") ("560#L234" "assume !(ssl3_connect_~s__state~3 == 4560);" "561#L238") ("560#L234" "assume ssl3_connect_~s__state~3 == 4560;" "559#L239") ("575#L186" "assume !(ssl3_connect_~s__state~3 == 4464);" "574#L190") ("575#L186" "assume ssl3_connect_~s__state~3 == 4464;" "482#L199") ("574#L190" "assume ssl3_connect_~s__state~3 == 4465;" "482#L199") ("574#L190" "assume !(ssl3_connect_~s__state~3 == 4465);" "573#L194") ("573#L194" "assume !(ssl3_connect_~s__state~3 == 4466);" "572#L198") ("573#L194" "assume ssl3_connect_~s__state~3 == 4466;" "482#L199") ("572#L198" "assume ssl3_connect_~s__state~3 == 4467;" "482#L199") ("572#L198" "assume !(ssl3_connect_~s__state~3 == 4467);" "571#L202") ("571#L202" "assume ssl3_connect_~s__state~3 == 4480;" "515#L207") ("571#L202" "assume !(ssl3_connect_~s__state~3 == 4480);" "570#L206") ("570#L206" "assume !(ssl3_connect_~s__state~3 == 4481);" "569#L210") ("570#L206" "assume ssl3_connect_~s__state~3 == 4481;" "515#L207") ("569#L210" "assume ssl3_connect_~s__state~3 == 4496;" "588#L215") ("569#L210" "assume !(ssl3_connect_~s__state~3 == 4496);" "568#L214") ("568#L214" "assume !(ssl3_connect_~s__state~3 == 4497);" "567#L218") ("568#L214" "assume ssl3_connect_~s__state~3 == 4497;" "588#L215") ("516#L134" "assume !(ssl3_connect_~s__state~3 == 4099);" "503#L138") ("516#L134" "assume ssl3_connect_~s__state~3 == 4099;" "447#L259") ("517#L463" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4480;ssl3_connect_~s__init_num~3 := 0;" "495#L673") ("518#L348''" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__state~3 := 4560;ParallelCodeBlock1: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__state~3 := 4400;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "495#L673") ("519#L409" "assume !!(ssl3_connect_~tmp___6~3 != 0);" "495#L673") ("512#L194" "assume !(ssl3_connect_~s__state~3 == 4466);" "486#L198") ("512#L194" "assume ssl3_connect_~s__state~3 == 4466;" "581#L199") ("513#L239" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet43;havoc ssl3_connect_#t~nondet43;" "546#L593") ("514#L499" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4512;ssl3_connect_~s__init_num~3 := 0;ssl3_connect_~s__s3__change_cipher_spec~3 := 0;" "495#L673") ("515#L207" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet39;havoc ssl3_connect_#t~nondet39;" "453#L476") ("524#L170" "assume !(ssl3_connect_~s__state~3 == 4432);" "523#L174") ("524#L170" "assume ssl3_connect_~s__state~3 == 4432;" "522#L175") ("525#L166" "assume !(ssl3_connect_~s__state~3 == 4417);" "524#L170") ("525#L166" "assume ssl3_connect_~s__state~3 == 4417;" "448#L167") ("526#L162" "assume !(ssl3_connect_~s__state~3 == 4416);" "525#L166") ("526#L162" "assume ssl3_connect_~s__state~3 == 4416;" "448#L167") ("527#L158" "assume !(ssl3_connect_~s__state~3 == 4401);" "526#L162") ("527#L158" "assume ssl3_connect_~s__state~3 == 4401;" "465#L159") ("520#L162" "assume !(ssl3_connect_~s__state~3 == 4416);" "445#L166") ("520#L162" "assume ssl3_connect_~s__state~3 == 4416;" "564#L167") ("521#L420" "assume ssl3_connect_~blastFlag~3 == 5;" "442#L421") ("521#L420" "assume !(ssl3_connect_~blastFlag~3 == 5);" "450#L424") ("522#L175" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet36;havoc ssl3_connect_#t~nondet36;" "521#L420") ("523#L174" "assume !(ssl3_connect_~s__state~3 == 4433);" "577#L178") ("523#L174" "assume ssl3_connect_~s__state~3 == 4433;" "522#L175") ("533#L134" "assume !(ssl3_connect_~s__state~3 == 4099);" "532#L138") ("533#L134" "assume ssl3_connect_~s__state~3 == 4099;" "589#L259") ("532#L138" "assume ssl3_connect_~s__state~3 == 4368;" "497#L143") ("532#L138" "assume !(ssl3_connect_~s__state~3 == 4368);" "531#L142") ("535#L126" "assume ssl3_connect_~s__state~3 == 4096;" "589#L259") ("535#L126" "assume !(ssl3_connect_~s__state~3 == 4096);" "534#L130") ("534#L130" "assume ssl3_connect_~s__state~3 == 20480;" "589#L259") ("534#L130" "assume !(ssl3_connect_~s__state~3 == 20480);" "533#L134") ("529#L150" "assume ssl3_connect_~s__state~3 == 4385;" "598#L151") ("529#L150" "assume !(ssl3_connect_~s__state~3 == 4385);" "477#L154") ("528#L154" "assume ssl3_connect_~s__state~3 == 4400;" "465#L159") ("528#L154" "assume !(ssl3_connect_~s__state~3 == 4400);" "527#L158") ("531#L142" "assume ssl3_connect_~s__state~3 == 4369;" "497#L143") ("531#L142" "assume !(ssl3_connect_~s__state~3 == 4369);" "530#L146") ("530#L146" "assume !(ssl3_connect_~s__state~3 == 4384);" "529#L150") ("530#L146" "assume ssl3_connect_~s__state~3 == 4384;" "598#L151") ("541#L711" "assume !!(ssl3_connect_~skip~3 != 0);" "540#L709") ("541#L711" "assume !(ssl3_connect_~skip~3 != 0);" "544#L713") ("540#L709" "ssl3_connect_~skip~3 := 0;" "539#L113''") ("543#L713''" "BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~cb~3 != 0);ParallelCodeBlock1: assume ssl3_connect_~cb~3 != 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__state~3 != ssl3_connect_~state~3;ssl3_connect_~new_state~3 := ssl3_connect_~s__state~3;ssl3_connect_~s__state~3 := ssl3_connect_~state~3;ssl3_connect_~s__state~3 := ssl3_connect_~new_state~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__state~3 != ssl3_connect_~state~3);}EndParallelComposition}EndParallelComposition" "540#L709") ("542#L673" "assume !!(ssl3_connect_~s__s3__tmp__reuse_message~3 != 0);" "540#L709") ("542#L673" "assume !(ssl3_connect_~s__s3__tmp__reuse_message~3 != 0);" "541#L711") ("537#L118" "assume !(ssl3_connect_~s__state~3 == 12292);" "536#L122") ("537#L118" "assume ssl3_connect_~s__state~3 == 12292;" "590#L119") ("536#L122" "assume !(ssl3_connect_~s__state~3 == 16384);" "535#L126") ("536#L122" "assume ssl3_connect_~s__state~3 == 16384;" "589#L259") ("539#L113''" "assume true;" "538#L113") ("538#L113" "assume !!true;ssl3_connect_~state~3 := ssl3_connect_~s__state~3;" "537#L118") ("576#L182" "assume !(ssl3_connect_~s__state~3 == 4449);" "575#L186") ("576#L182" "assume ssl3_connect_~s__state~3 == 4449;" "596#L183") ("577#L178" "assume !(ssl3_connect_~s__state~3 == 4448);" "576#L182") ("577#L178" "assume ssl3_connect_~s__state~3 == 4448;" "596#L183") ("578#L524''" "assume !!(ssl3_connect_~tmp___7~3 != 0);" "557#L538") ("579#L514" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4528;ssl3_connect_~s__init_num~3 := 0;ssl3_connect_~s__session__cipher~3 := ssl3_connect_~s__s3__tmp__new_cipher~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__new_compression~3 == 0;ssl3_connect_~s__session__compress_meth~3 := 0;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__new_compression~3 == 0);ssl3_connect_~s__session__compress_meth~3 := ssl3_connect_~s__s3__tmp__new_compression__id~3;}EndParallelComposition" "578#L524''") ("580#L223" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet41;havoc ssl3_connect_#t~nondet41;" "579#L514") ("581#L199" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet38;havoc ssl3_connect_#t~nondet38;" "556#L463") ("582#L207" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet39;havoc ssl3_connect_#t~nondet39;" "555#L476") ("583#L282''" "assume !!(ssl3_connect_~tmp___4~3 != 0);" "553#L307") ("584#L282" "assume ssl3_connect_~s__init_buf___0~3 == 0;ssl3_connect_~buf~3 := ssl3_connect_#t~nondet30;havoc ssl3_connect_#t~nondet30;" "586#L286") ("584#L282" "assume !(ssl3_connect_~s__init_buf___0~3 == 0);" "583#L282''") ("585#L292" "assume !!(ssl3_connect_~tmp___3~3 != 0);ssl3_connect_~s__init_buf___0~3 := ssl3_connect_~buf~3;" "583#L282''") ("586#L286" "assume !(ssl3_connect_~buf~3 == 0);" "585#L292") ("587#L273" "assume !(ssl3_connect_~__cil_tmp55~3 != 768);ssl3_connect_~s__type~3 := 4096;" "584#L282") ("588#L215" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet40;havoc ssl3_connect_#t~nondet40;" "514#L499") ("589#L259" "ssl3_connect_~s__server~3 := 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~cb~3 != 0;ParallelCodeBlock1: assume !(ssl3_connect_~cb~3 != 0);}EndParallelCompositionssl3_connect_~__cil_tmp55~3 := ssl3_connect_~s__version~3 - 65280;" "587#L273") ("590#L119" "ssl3_connect_~s__new_session~3 := 1;ssl3_connect_~s__state~3 := 4096;ssl3_connect_#t~post29 := ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3;ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3 := ssl3_connect_#t~post29 + 1;havoc ssl3_connect_#t~post29;" "589#L259") ("591#L231" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet42;havoc ssl3_connect_#t~nondet42;" "489#L549") ("593#L377''" "assume !(ssl3_connect_~ret~3 <= 0);" "558#L370'") ("592#L159" "assume ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3 - 256 != 0;ssl3_connect_~skip~3 := 1;" "558#L370'") ("592#L159" "assume !(ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3 - 256 != 0);ssl3_connect_~ret~3 := ssl3_connect_#t~nondet34;havoc ssl3_connect_#t~nondet34;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 2;ssl3_connect_~blastFlag~3 := 3;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 2);}EndParallelComposition" "593#L377''") ("595#L621" "assume !(ssl3_connect_~__cil_tmp62~3 <= 0);ssl3_connect_~s__rwstate~3 := 1;" "463#L612''") ("594#L612" "assume ssl3_connect_~__cil_tmp61~3 > 0;ssl3_connect_~s__rwstate~3 := 2;ssl3_connect_~num1~3 := ssl3_connect_~tmp___9~3;ssl3_connect_~__cil_tmp62~3 := ssl3_connect_~num1~3;" "595#L621") ("594#L612" "assume !(ssl3_connect_~__cil_tmp61~3 > 0);" "463#L612''") ("597#L242" "assume ssl3_connect_~s__state~3 == 4352;ssl3_connect_~__cil_tmp61~3 := ssl3_connect_~num1~3;" "594#L612") ("596#L183" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet37;havoc ssl3_connect_#t~nondet37;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 4;ssl3_connect_~blastFlag~3 := 5;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 4);}EndParallelComposition" "462#L437''") ("598#L151" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet33;havoc ssl3_connect_#t~nondet33;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 1;ssl3_connect_~blastFlag~3 := 2;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 1);}EndParallelComposition" "550#L348''") ("440#L150" "assume ssl3_connect_~s__state~3 == 4385;" "439#L151") ("440#L150" "assume !(ssl3_connect_~s__state~3 == 4385);" "528#L154") ("441#L222" "assume ssl3_connect_~s__state~3 == 4513;" "580#L223") ("441#L222" "assume !(ssl3_connect_~s__state~3 == 4513);" "452#L226") ("442#L421" "assume !false;" "464#ULTIMATE.startErr0AssertViolation") ("443#L420" "assume !(ssl3_connect_~blastFlag~3 == 5);" "554#L424") ("444#L113" "assume !!true;ssl3_connect_~state~3 := ssl3_connect_~s__state~3;" "455#L118") ("445#L166" "assume !(ssl3_connect_~s__state~3 == 4417);" "496#L170") ("445#L166" "assume ssl3_connect_~s__state~3 == 4417;" "564#L167") ("446#L514" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4528;ssl3_connect_~s__init_num~3 := 0;ssl3_connect_~s__session__cipher~3 := ssl3_connect_~s__s3__tmp__new_cipher~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__new_compression~3 == 0;ssl3_connect_~s__session__compress_meth~3 := 0;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__new_compression~3 == 0);ssl3_connect_~s__session__compress_meth~3 := ssl3_connect_~s__s3__tmp__new_compression__id~3;}EndParallelComposition" "500#L524''") ("447#L259" "ssl3_connect_~s__server~3 := 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~cb~3 != 0;ParallelCodeBlock1: assume !(ssl3_connect_~cb~3 != 0);}EndParallelCompositionssl3_connect_~__cil_tmp55~3 := ssl3_connect_~s__version~3 - 65280;" "507#L273") ("438#L223" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet41;havoc ssl3_connect_#t~nondet41;" "446#L514") ("439#L151" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet33;havoc ssl3_connect_#t~nondet33;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 1;ssl3_connect_~blastFlag~3 := 2;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 1);}EndParallelComposition" "518#L348''") ("478#L182" "assume !(ssl3_connect_~s__state~3 == 4449);" "471#L186") ("478#L182" "assume ssl3_connect_~s__state~3 == 4449;" "475#L183") ("479#L210" "assume ssl3_connect_~s__state~3 == 4496;" "459#L215") ("479#L210" "assume !(ssl3_connect_~s__state~3 == 4496);" "456#L214") ("476#L621" "assume !(ssl3_connect_~__cil_tmp62~3 <= 0);ssl3_connect_~s__rwstate~3 := 1;" "552#L612''") ("477#L154" "assume ssl3_connect_~s__state~3 == 4400;" "592#L159") ("477#L154" "assume !(ssl3_connect_~s__state~3 == 4400);" "469#L158") ("474#L292" "assume !!(ssl3_connect_~tmp___3~3 != 0);ssl3_connect_~s__init_buf___0~3 := ssl3_connect_~buf~3;" "472#L282''") ("475#L183" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet37;havoc ssl3_connect_#t~nondet37;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 4;ssl3_connect_~blastFlag~3 := 5;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 4);}EndParallelComposition" "549#L437''") ("472#L282''" "assume !!(ssl3_connect_~tmp___4~3 != 0);" "449#L307") ("473#L713" "assume ssl3_connect_~s__debug~3 != 0;ssl3_connect_~ret~3 := ssl3_connect_#t~nondet46;havoc ssl3_connect_#t~nondet46;" "480#L717") ("473#L713" "assume !(ssl3_connect_~s__debug~3 != 0);" "468#L713''") ("470#L326''" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4384;ssl3_connect_~s__init_num~3 := 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__bbio~3 != ssl3_connect_~s__wbio~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__bbio~3 != ssl3_connect_~s__wbio~3);}EndParallelComposition" "495#L673") ("471#L186" "assume !(ssl3_connect_~s__state~3 == 4464);" "502#L190") ("471#L186" "assume ssl3_connect_~s__state~3 == 4464;" "581#L199") ("468#L713''" "BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~cb~3 != 0);ParallelCodeBlock1: assume ssl3_connect_~cb~3 != 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__state~3 != ssl3_connect_~state~3;ssl3_connect_~new_state~3 := ssl3_connect_~s__state~3;ssl3_connect_~s__state~3 := ssl3_connect_~state~3;ssl3_connect_~s__state~3 := ssl3_connect_~new_state~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__state~3 != ssl3_connect_~state~3);}EndParallelComposition}EndParallelComposition" "454#L709") ("469#L158" "assume !(ssl3_connect_~s__state~3 == 4401);" "520#L162") ("469#L158" "assume ssl3_connect_~s__state~3 == 4401;" "592#L159") ("466#L612" "assume ssl3_connect_~__cil_tmp61~3 > 0;ssl3_connect_~s__rwstate~3 := 2;ssl3_connect_~num1~3 := ssl3_connect_~tmp___9~3;ssl3_connect_~__cil_tmp62~3 := ssl3_connect_~num1~3;" "476#L621") ("466#L612" "assume !(ssl3_connect_~__cil_tmp61~3 > 0);" "552#L612''") ("467#L113''" "assume true;" "444#L113") ("465#L159" "assume ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3 - 256 != 0;ssl3_connect_~skip~3 := 1;" "498#L370'") ("465#L159" "assume !(ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3 - 256 != 0);ssl3_connect_~ret~3 := ssl3_connect_#t~nondet34;havoc ssl3_connect_#t~nondet34;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 2;ssl3_connect_~blastFlag~3 := 3;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 2);}EndParallelComposition" "461#L377''") ("463#L612''" "ssl3_connect_~s__state~3 := ssl3_connect_~s__s3__tmp__next_state___0~3;" "495#L673") ("462#L437''" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__cert_req~3 != 0;ssl3_connect_~s__state~3 := 4464;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__cert_req~3 != 0);ssl3_connect_~s__state~3 := 4480;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "495#L673") ("461#L377''" "assume !(ssl3_connect_~ret~3 <= 0);" "498#L370'") ("460#ULTIMATE.startENTRY" "#NULL.base, #NULL.offset := 0, 0;havoc main_#res;havoc main_#t~ret48, main_~s~142;havoc main_~s~142;main_~s~142 := 12292;ssl3_connect_#in~initial_state := 12292;havoc ssl3_connect_#res;havoc ssl3_connect_#t~nondet0, ssl3_connect_#t~nondet1, ssl3_connect_#t~nondet2, ssl3_connect_#t~nondet3, ssl3_connect_#t~nondet4, ssl3_connect_#t~nondet5, ssl3_connect_#t~nondet6, ssl3_connect_#t~nondet7, ssl3_connect_#t~nondet8, ssl3_connect_#t~nondet9, ssl3_connect_#t~nondet10, ssl3_connect_#t~nondet11, ssl3_connect_#t~nondet12, ssl3_connect_#t~nondet13, ssl3_connect_#t~nondet14, ssl3_connect_#t~nondet15, ssl3_connect_#t~nondet16, ssl3_connect_#t~nondet17, ssl3_connect_#t~nondet18, ssl3_connect_#t~nondet19, ssl3_connect_#t~nondet20, ssl3_connect_#t~nondet21, ssl3_connect_#t~nondet22, ssl3_connect_#t~nondet23, ssl3_connect_#t~nondet24, ssl3_connect_#t~nondet25, ssl3_connect_#t~nondet26, ssl3_connect_#t~nondet27, ssl3_connect_#t~post28, ssl3_connect_#t~post29, ssl3_connect_#t~nondet30, ssl3_connect_#t~post31, ssl3_connect_#t~nondet32, ssl3_connect_#t~nondet33, ssl3_connect_#t~nondet34, ssl3_connect_#t~nondet35, ssl3_connect_#t~nondet36, ssl3_connect_#t~nondet37, ssl3_connect_#t~nondet38, ssl3_connect_#t~nondet39, ssl3_connect_#t~nondet40, ssl3_connect_#t~nondet41, ssl3_connect_#t~nondet42, ssl3_connect_#t~nondet43, ssl3_connect_#t~post44, ssl3_connect_#t~post45, ssl3_connect_#t~nondet46, ssl3_connect_#t~post47, ssl3_connect_~initial_state, ssl3_connect_~s__info_callback~3, ssl3_connect_~s__in_handshake~3, ssl3_connect_~s__state~3, ssl3_connect_~s__new_session~3, ssl3_connect_~s__server~3, ssl3_connect_~s__version~3, ssl3_connect_~s__type~3, ssl3_connect_~s__init_num~3, ssl3_connect_~s__bbio~3, ssl3_connect_~s__wbio~3, ssl3_connect_~s__hit~3, ssl3_connect_~s__rwstate~3, ssl3_connect_~s__init_buf___0~3, ssl3_connect_~s__debug~3, ssl3_connect_~s__shutdown~3, ssl3_connect_~s__ctx__info_callback~3, ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3, ssl3_connect_~s__ctx__stats__sess_connect~3, ssl3_connect_~s__ctx__stats__sess_hit~3, ssl3_connect_~s__ctx__stats__sess_connect_good~3, ssl3_connect_~s__s3__change_cipher_spec~3, ssl3_connect_~s__s3__flags~3, ssl3_connect_~s__s3__delay_buf_pop_ret~3, ssl3_connect_~s__s3__tmp__cert_req~3, ssl3_connect_~s__s3__tmp__new_compression~3, ssl3_connect_~s__s3__tmp__reuse_message~3, ssl3_connect_~s__s3__tmp__new_cipher~3, ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3, ssl3_connect_~s__s3__tmp__next_state___0~3, ssl3_connect_~s__s3__tmp__new_compression__id~3, ssl3_connect_~s__session__cipher~3, ssl3_connect_~s__session__compress_meth~3, ssl3_connect_~buf~3, ssl3_connect_~tmp~3, ssl3_connect_~l~3, ssl3_connect_~num1~3, ssl3_connect_~cb~3, ssl3_connect_~ret~3, ssl3_connect_~new_state~3, ssl3_connect_~state~3, ssl3_connect_~skip~3, ssl3_connect_~tmp___0~3, ssl3_connect_~tmp___1~3, ssl3_connect_~tmp___2~3, ssl3_connect_~tmp___3~3, ssl3_connect_~tmp___4~3, ssl3_connect_~tmp___5~3, ssl3_connect_~tmp___6~3, ssl3_connect_~tmp___7~3, ssl3_connect_~tmp___8~3, ssl3_connect_~tmp___9~3, ssl3_connect_~blastFlag~3, ssl3_connect_~__cil_tmp55~3, ssl3_connect_~__cil_tmp56~3, ssl3_connect_~__cil_tmp57~3, ssl3_connect_~__cil_tmp58~3, ssl3_connect_~__cil_tmp59~3, ssl3_connect_~__cil_tmp60~3, ssl3_connect_~__cil_tmp61~3, ssl3_connect_~__cil_tmp62~3, ssl3_connect_~__cil_tmp63~3, ssl3_connect_~__cil_tmp64~3;ssl3_connect_~initial_state := ssl3_connect_#in~initial_state;ssl3_connect_~s__info_callback~3 := ssl3_connect_#t~nondet0;havoc ssl3_connect_#t~nondet0;ssl3_connect_~s__in_handshake~3 := ssl3_connect_#t~nondet1;havoc ssl3_connect_#t~nondet1;havoc ssl3_connect_~s__state~3;havoc ssl3_connect_~s__new_session~3;havoc ssl3_connect_~s__server~3;ssl3_connect_~s__version~3 := ssl3_connect_#t~nondet2;havoc ssl3_connect_#t~nondet2;havoc ssl3_connect_~s__type~3;havoc ssl3_connect_~s__init_num~3;ssl3_connect_~s__bbio~3 := ssl3_connect_#t~nondet3;havoc ssl3_connect_#t~nondet3;ssl3_connect_~s__wbio~3 := ssl3_connect_#t~nondet4;havoc ssl3_connect_#t~nondet4;ssl3_connect_~s__hit~3 := ssl3_connect_#t~nondet5;havoc ssl3_connect_#t~nondet5;havoc ssl3_connect_~s__rwstate~3;havoc ssl3_connect_~s__init_buf___0~3;ssl3_connect_~s__debug~3 := ssl3_connect_#t~nondet6;havoc ssl3_connect_#t~nondet6;havoc ssl3_connect_~s__shutdown~3;ssl3_connect_~s__ctx__info_callback~3 := ssl3_connect_#t~nondet7;havoc ssl3_connect_#t~nondet7;ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3 := ssl3_connect_#t~nondet8;havoc ssl3_connect_#t~nondet8;ssl3_connect_~s__ctx__stats__sess_connect~3 := ssl3_connect_#t~nondet9;havoc ssl3_connect_#t~nondet9;ssl3_connect_~s__ctx__stats__sess_hit~3 := ssl3_connect_#t~nondet10;havoc ssl3_connect_#t~nondet10;ssl3_connect_~s__ctx__stats__sess_connect_good~3 := ssl3_connect_#t~nondet11;havoc ssl3_connect_#t~nondet11;havoc ssl3_connect_~s__s3__change_cipher_spec~3;havoc ssl3_connect_~s__s3__flags~3;havoc ssl3_connect_~s__s3__delay_buf_pop_ret~3;ssl3_connect_~s__s3__tmp__cert_req~3 := ssl3_connect_#t~nondet12;havoc ssl3_connect_#t~nondet12;ssl3_connect_~s__s3__tmp__new_compression~3 := ssl3_connect_#t~nondet13;havoc ssl3_connect_#t~nondet13;ssl3_connect_~s__s3__tmp__reuse_message~3 := ssl3_connect_#t~nondet14;havoc ssl3_connect_#t~nondet14;ssl3_connect_~s__s3__tmp__new_cipher~3 := ssl3_connect_#t~nondet15;havoc ssl3_connect_#t~nondet15;ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3 := ssl3_connect_#t~nondet16;havoc ssl3_connect_#t~nondet16;havoc ssl3_connect_~s__s3__tmp__next_state___0~3;ssl3_connect_~s__s3__tmp__new_compression__id~3 := ssl3_connect_#t~nondet17;havoc ssl3_connect_#t~nondet17;havoc ssl3_connect_~s__session__cipher~3;havoc ssl3_connect_~s__session__compress_meth~3;havoc ssl3_connect_~buf~3;havoc ssl3_connect_~tmp~3;havoc ssl3_connect_~l~3;havoc ssl3_connect_~num1~3;havoc ssl3_connect_~cb~3;havoc ssl3_connect_~ret~3;havoc ssl3_connect_~new_state~3;havoc ssl3_connect_~state~3;havoc ssl3_connect_~skip~3;havoc ssl3_connect_~tmp___0~3;ssl3_connect_~tmp___1~3 := ssl3_connect_#t~nondet18;havoc ssl3_connect_#t~nondet18;ssl3_connect_~tmp___2~3 := ssl3_connect_#t~nondet19;havoc ssl3_connect_#t~nondet19;ssl3_connect_~tmp___3~3 := ssl3_connect_#t~nondet20;havoc ssl3_connect_#t~nondet20;ssl3_connect_~tmp___4~3 := ssl3_connect_#t~nondet21;havoc ssl3_connect_#t~nondet21;ssl3_connect_~tmp___5~3 := ssl3_connect_#t~nondet22;havoc ssl3_connect_#t~nondet22;ssl3_connect_~tmp___6~3 := ssl3_connect_#t~nondet23;havoc ssl3_connect_#t~nondet23;ssl3_connect_~tmp___7~3 := ssl3_connect_#t~nondet24;havoc ssl3_connect_#t~nondet24;ssl3_connect_~tmp___8~3 := ssl3_connect_#t~nondet25;havoc ssl3_connect_#t~nondet25;ssl3_connect_~tmp___9~3 := ssl3_connect_#t~nondet26;havoc ssl3_connect_#t~nondet26;havoc ssl3_connect_~blastFlag~3;havoc ssl3_connect_~__cil_tmp55~3;havoc ssl3_connect_~__cil_tmp56~3;havoc ssl3_connect_~__cil_tmp57~3;havoc ssl3_connect_~__cil_tmp58~3;havoc ssl3_connect_~__cil_tmp59~3;havoc ssl3_connect_~__cil_tmp60~3;havoc ssl3_connect_~__cil_tmp61~3;havoc ssl3_connect_~__cil_tmp62~3;havoc ssl3_connect_~__cil_tmp63~3;havoc ssl3_connect_~__cil_tmp64~3;ssl3_connect_~s__state~3 := ssl3_connect_~initial_state;ssl3_connect_~blastFlag~3 := 0;ssl3_connect_~tmp~3 := ssl3_connect_#t~nondet27;havoc ssl3_connect_#t~nondet27;ssl3_connect_~cb~3 := 0;ssl3_connect_~ret~3 := -1;ssl3_connect_~skip~3 := 0;ssl3_connect_~tmp___0~3 := 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__info_callback~3 != 0;ssl3_connect_~cb~3 := ssl3_connect_~s__info_callback~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__info_callback~3 != 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__ctx__info_callback~3 != 0;ssl3_connect_~cb~3 := ssl3_connect_~s__ctx__info_callback~3;ParallelCodeBlock1: assume !(ssl3_connect_~s__ctx__info_callback~3 != 0);}EndParallelComposition}EndParallelCompositionssl3_connect_#t~post28 := ssl3_connect_~s__in_handshake~3;ssl3_connect_~s__in_handshake~3 := ssl3_connect_#t~post28 + 1;havoc ssl3_connect_#t~post28;BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~tmp___1~3 - 12288 != 0);ParallelCodeBlock1: assume ssl3_connect_~tmp___1~3 - 12288 != 0;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~tmp___2~3 - 16384 != 0;ParallelCodeBlock1: assume !(ssl3_connect_~tmp___2~3 - 16384 != 0);}EndParallelComposition}EndParallelComposition" "539#L113''") ("459#L215" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet40;havoc ssl3_connect_#t~nondet40;" "548#L499") ("458#L538" "assume !!(ssl3_connect_~tmp___8~3 != 0);" "495#L673") ("457#L122" "assume !(ssl3_connect_~s__state~3 == 16384);" "481#L126") ("457#L122" "assume ssl3_connect_~s__state~3 == 16384;" "447#L259") ("456#L214" "assume !(ssl3_connect_~s__state~3 == 4497);" "490#L218") ("456#L214" "assume ssl3_connect_~s__state~3 == 4497;" "459#L215") ("455#L118" "assume !(ssl3_connect_~s__state~3 == 12292);" "457#L122") ("455#L118" "assume ssl3_connect_~s__state~3 == 12292;" "508#L119") ("454#L709" "ssl3_connect_~skip~3 := 0;" "467#L113''") ("453#L476" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~l~3 := ssl3_connect_~s__s3__tmp__new_cipher__algorithms~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__s3__tmp__cert_req~3 == 1;ssl3_connect_~s__state~3 := 4496;ParallelCodeBlock1: assume !(ssl3_connect_~s__s3__tmp__cert_req~3 == 1);ssl3_connect_~s__state~3 := 4512;ssl3_connect_~s__s3__change_cipher_spec~3 := 0;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "495#L673") ("452#L226" "assume ssl3_connect_~s__state~3 == 4528;" "510#L231") ("452#L226" "assume !(ssl3_connect_~s__state~3 == 4528);" "504#L230") ("451#L282" "assume ssl3_connect_~s__init_buf___0~3 == 0;ssl3_connect_~buf~3 := ssl3_connect_#t~nondet30;havoc ssl3_connect_#t~nondet30;" "506#L286") ("451#L282" "assume !(ssl3_connect_~s__init_buf___0~3 == 0);" "472#L282''") ("450#L424" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4448;ssl3_connect_~s__init_num~3 := 0;" "495#L673") ("449#L307" "assume !!(ssl3_connect_~tmp___5~3 != 0);ssl3_connect_~s__state~3 := 4368;ssl3_connect_#t~post31 := ssl3_connect_~s__ctx__stats__sess_connect~3;ssl3_connect_~s__ctx__stats__sess_connect~3 := ssl3_connect_#t~post31 + 1;havoc ssl3_connect_#t~post31;ssl3_connect_~s__init_num~3 := 0;" "495#L673") ("448#L167" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet35;havoc ssl3_connect_#t~nondet35;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 3;ssl3_connect_~blastFlag~3 := 4;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 3);}EndParallelComposition" "487#L396''") ("508#L119" "ssl3_connect_~s__new_session~3 := 1;ssl3_connect_~s__state~3 := 4096;ssl3_connect_#t~post29 := ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3;ssl3_connect_~s__ctx__stats__sess_connect_renegotiate~3 := ssl3_connect_#t~post29 + 1;havoc ssl3_connect_#t~post29;" "447#L259") ("509#L593" "assume !(ssl3_connect_~ret~3 <= 0);BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__state~3 := 4512;ParallelCodeBlock1: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__state~3 := 3;}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "495#L673") ("510#L231" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet42;havoc ssl3_connect_#t~nondet42;" "551#L549") ("511#L238" "assume ssl3_connect_~s__state~3 == 4561;" "513#L239") ("511#L238" "assume !(ssl3_connect_~s__state~3 == 4561);" "483#L242") ("504#L230" "assume !(ssl3_connect_~s__state~3 == 4529);" "501#L234") ("504#L230" "assume ssl3_connect_~s__state~3 == 4529;" "510#L231") ("505#L175" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet36;havoc ssl3_connect_#t~nondet36;" "443#L420") ("506#L286" "assume !(ssl3_connect_~buf~3 == 0);" "474#L292") ("507#L273" "assume !(ssl3_connect_~__cil_tmp55~3 != 768);ssl3_connect_~s__type~3 := 4096;" "451#L282") ("500#L524''" "assume !!(ssl3_connect_~tmp___7~3 != 0);" "458#L538") ("501#L234" "assume !(ssl3_connect_~s__state~3 == 4560);" "511#L238") ("501#L234" "assume ssl3_connect_~s__state~3 == 4560;" "513#L239") ("502#L190" "assume ssl3_connect_~s__state~3 == 4465;" "581#L199") ("502#L190" "assume !(ssl3_connect_~s__state~3 == 4465);" "512#L194") ("503#L138" "assume ssl3_connect_~s__state~3 == 4368;" "497#L143") ("503#L138" "assume !(ssl3_connect_~s__state~3 == 4368);" "494#L142") ("496#L170" "assume !(ssl3_connect_~s__state~3 == 4432);" "492#L174") ("496#L170" "assume ssl3_connect_~s__state~3 == 4432;" "505#L175") ("497#L143" "ssl3_connect_~s__shutdown~3 := 0;ssl3_connect_~ret~3 := ssl3_connect_#t~nondet32;havoc ssl3_connect_#t~nondet32;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~blastFlag~3 == 0;ssl3_connect_~blastFlag~3 := 1;ParallelCodeBlock1: assume !(ssl3_connect_~blastFlag~3 == 0);}EndParallelComposition" "470#L326''") ("498#L370'" "ssl3_connect_~s__state~3 := 4416;ssl3_connect_~s__init_num~3 := 0;" "495#L673") ("499#L178" "assume !(ssl3_connect_~s__state~3 == 4448);" "478#L182") ("499#L178" "assume ssl3_connect_~s__state~3 == 4448;" "475#L183") ("493#L711" "assume !!(ssl3_connect_~skip~3 != 0);" "454#L709") ("493#L711" "assume !(ssl3_connect_~skip~3 != 0);" "473#L713") ("492#L174" "assume !(ssl3_connect_~s__state~3 == 4433);" "499#L178") ("492#L174" "assume ssl3_connect_~s__state~3 == 4433;" "505#L175") ("495#L673" "assume !!(ssl3_connect_~s__s3__tmp__reuse_message~3 != 0);" "454#L709") ("495#L673" "assume !(ssl3_connect_~s__s3__tmp__reuse_message~3 != 0);" "493#L711") ("494#L142" "assume ssl3_connect_~s__state~3 == 4369;" "497#L143") ("494#L142" "assume !(ssl3_connect_~s__state~3 == 4369);" "491#L146") ("489#L549" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4352;ssl3_connect_~__cil_tmp56~3 := ssl3_connect_~s__s3__flags~3;ssl3_connect_~__cil_tmp57~3 := ssl3_connect_~__cil_tmp56~3 + 5;ssl3_connect_~s__s3__flags~3 := ssl3_connect_~__cil_tmp57~3;BeginParallelComposition{ParallelCodeBlock0: assume !(ssl3_connect_~s__hit~3 != 0);ssl3_connect_~s__s3__tmp__next_state___0~3 := 4560;ParallelCodeBlock1: assume ssl3_connect_~s__hit~3 != 0;ssl3_connect_~s__s3__tmp__next_state___0~3 := 3;ssl3_connect_~__cil_tmp58~3 := ssl3_connect_~s__s3__flags~3;BeginParallelComposition{ParallelCodeBlock0: assume ssl3_connect_~__cil_tmp58~3 - 2 != 0;ssl3_connect_~s__state~3 := 3;ssl3_connect_~__cil_tmp59~3 := ssl3_connect_~s__s3__flags~3;ssl3_connect_~__cil_tmp60~3 := ssl3_connect_~__cil_tmp59~3 + 4;ssl3_connect_~s__s3__flags~3 := ssl3_connect_~__cil_tmp60~3;ssl3_connect_~s__s3__delay_buf_pop_ret~3 := 0;ParallelCodeBlock1: assume !(ssl3_connect_~__cil_tmp58~3 - 2 != 0);}EndParallelComposition}EndParallelCompositionssl3_connect_~s__init_num~3 := 0;" "495#L673") ("488#L130" "assume ssl3_connect_~s__state~3 == 20480;" "447#L259") ("488#L130" "assume !(ssl3_connect_~s__state~3 == 20480);" "516#L134") ("491#L146" "assume !(ssl3_connect_~s__state~3 == 4384);" "440#L150") ("491#L146" "assume ssl3_connect_~s__state~3 == 4384;" "439#L151") ("490#L218" "assume !(ssl3_connect_~s__state~3 == 4512);" "441#L222") ("490#L218" "assume ssl3_connect_~s__state~3 == 4512;" "580#L223") ("485#L202" "assume ssl3_connect_~s__state~3 == 4480;" "582#L207") ("485#L202" "assume !(ssl3_connect_~s__state~3 == 4480);" "484#L206") ("484#L206" "assume !(ssl3_connect_~s__state~3 == 4481);" "479#L210") ("484#L206" "assume ssl3_connect_~s__state~3 == 4481;" "582#L207") ("487#L396''" "assume !(ssl3_connect_~ret~3 <= 0);ssl3_connect_~s__state~3 := 4432;ssl3_connect_~s__init_num~3 := 0;" "519#L409") ("486#L198" "assume ssl3_connect_~s__state~3 == 4467;" "581#L199") ("486#L198" "assume !(ssl3_connect_~s__state~3 == 4467);" "485#L202") ("481#L126" "assume ssl3_connect_~s__state~3 == 4096;" "447#L259") ("481#L126" "assume !(ssl3_connect_~s__state~3 == 4096);" "488#L130") ("480#L717" "assume !(ssl3_connect_~ret~3 <= 0);" "468#L713''") ("483#L242" "assume ssl3_connect_~s__state~3 == 4352;ssl3_connect_~__cil_tmp61~3 := ssl3_connect_~num1~3;" "466#L612") ("482#L199" "ssl3_connect_~ret~3 := ssl3_connect_#t~nondet38;havoc ssl3_connect_#t~nondet38;" "517#L463") }, returnTransitions = { } );