path false false /hard-disk/dangl/base/sv-benchmarks/c/ssh-simplified/s3_clnt_1_false-unreach-call.cil.c C true true int s ; 758 758 s = 12292 763 763 s==12292; ssl3_connect(12292) 765 765 int s__info_callback = __VERIFIER_nondet_int() ; 13 13 int s__in_handshake = __VERIFIER_nondet_int() ; 14 14 int s__state ; 15 15 int s__new_session ; 16 16 int s__server ; 17 17 int s__version = __VERIFIER_nondet_int() ; 18 18 int s__type ; 19 19 int s__init_num ; 20 20 int s__bbio = __VERIFIER_nondet_int() ; 21 21 int s__wbio = __VERIFIER_nondet_int() ; 22 22 int s__hit = __VERIFIER_nondet_int() ; 23 23 int s__rwstate ; 24 24 int s__init_buf___0 ; 25 25 int s__debug = __VERIFIER_nondet_int() ; 26 26 int s__shutdown ; 27 27 int s__ctx__info_callback = __VERIFIER_nondet_int() ; 28 28 int s__ctx__stats__sess_connect_renegotiate = __VERIFIER_nondet_int() ; 29 29 int s__ctx__stats__sess_connect = __VERIFIER_nondet_int() ; 30 30 int s__ctx__stats__sess_hit = __VERIFIER_nondet_int() ; 31 31 int s__ctx__stats__sess_connect_good = __VERIFIER_nondet_int() ; 32 32 int s__s3__change_cipher_spec ; 33 33 int s__s3__flags ; 34 34 int s__s3__delay_buf_pop_ret ; 35 35 int s__s3__tmp__cert_req = __VERIFIER_nondet_int() ; 36 36 int s__s3__tmp__new_compression = __VERIFIER_nondet_int() ; 37 37 int s__s3__tmp__reuse_message = __VERIFIER_nondet_int() ; 38 38 int s__s3__tmp__new_cipher = __VERIFIER_nondet_int() ; 39 39 int s__s3__tmp__new_cipher__algorithms = __VERIFIER_nondet_int() ; 40 40 int s__s3__tmp__next_state___0 ; 41 41 int s__s3__tmp__new_compression__id = __VERIFIER_nondet_int() ; 42 42 int s__session__cipher ; 43 43 int s__session__compress_meth ; 44 44 int buf ; 45 45 unsigned long tmp ; 46 46 unsigned long l ; 47 47 int num1 ; 48 48 int cb ; 49 49 int ret ; 50 50 int new_state ; 51 51 int state ; 52 52 int skip ; 53 53 int tmp___0 ; 54 54 int tmp___1 = __VERIFIER_nondet_int() ; 55 55 int tmp___2 = __VERIFIER_nondet_int() ; 56 56 int tmp___3 = __VERIFIER_nondet_int() ; 57 57 int tmp___4 = __VERIFIER_nondet_int() ; 58 58 int tmp___5 = __VERIFIER_nondet_int() ; 59 59 int tmp___6 = __VERIFIER_nondet_int() ; 60 60 int tmp___7 = __VERIFIER_nondet_int() ; 61 61 int tmp___8 = __VERIFIER_nondet_int() ; 62 62 int tmp___9 = __VERIFIER_nondet_int() ; 63 63 int blastFlag ; 64 64 int __cil_tmp55 ; 65 65 long __cil_tmp56 ; 66 66 long __cil_tmp57 ; 67 67 long __cil_tmp58 ; 68 68 long __cil_tmp59 ; 69 69 long __cil_tmp60 ; 70 70 long __cil_tmp61 ; 71 71 long __cil_tmp62 ; 72 72 long __cil_tmp63 ; 73 73 long __cil_tmp64 ; 74 74 s__state = initial_state 79 79 blastFlag = 0 81 81 tmp = __VERIFIER_nondet_int() 83 83 cb = 0 85 85 ret = -1 87 87 skip = 0 89 89 tmp___0 = 0 91 91 tmp___9==0;s__wbio==0;blastFlag==0;tmp___6==1;s__s3__tmp__reuse_message==-1;s__debug==0;tmp___4==1;s__state==12292;tmp___5==1;s__s3__tmp__cert_req==0;tmp___2==0;tmp___1==12288;tmp___8==0;tmp___3==1;cb==0;s__ctx__stats__sess_connect==0;tmp___7==0;skip==0;s__info_callback==0;s__s3__tmp__new_cipher==0;initial_state==12292;s__ctx__stats__sess_hit==0;s__s3__tmp__new_compression__id==0;s__version==66048;tmp==0;s__ctx__stats__sess_connect_renegotiate==0;tmp___0==0;s__bbio==1;s__s3__tmp__new_cipher__algorithms==256;s__ctx__stats__sess_connect_good==0;s__hit==0;s__s3__tmp__new_compression==0;ret==-1;s__in_handshake==0;s__ctx__info_callback==-1; condition-false [!(s__info_callback != 0)] 93 93 s__info_callback==0;s__ctx__stats__sess_hit==0;s__debug==0;s__ctx__stats__sess_connect_good==0;tmp___4==1;tmp==0;s__ctx__info_callback==-1;tmp___7==0;ret==-1;cb==0;s__s3__tmp__new_cipher__algorithms==256;tmp___9==0;s__state==12292;s__in_handshake==0;tmp___5==1;tmp___6==1;tmp___8==0;s__s3__tmp__new_cipher==0;initial_state==12292;tmp___1==12288;s__s3__tmp__new_compression==0;s__hit==0;s__bbio==1;s__wbio==0;tmp___0==0;s__ctx__stats__sess_connect_renegotiate==0;s__ctx__stats__sess_connect==0;skip==0;s__version==66048;blastFlag==0;s__s3__tmp__new_compression__id==0;s__s3__tmp__cert_req==0;tmp___2==0;s__s3__tmp__reuse_message==-1;tmp___3==1; [s__ctx__info_callback != 0] 98 98 cb = s__ctx__info_callback 100 100 s__state==12292;s__debug==0;tmp___1==12288;cb==-1;ret==-1;s__ctx__info_callback==-1;tmp___8==0;s__info_callback==0;s__ctx__stats__sess_connect==0;tmp___6==1;tmp___0==0;s__s3__tmp__new_compression==0;tmp___7==0;tmp___9==0;blastFlag==0;initial_state==12292;s__version==66048;s__ctx__stats__sess_connect_renegotiate==0;s__in_handshake==0;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_hit==0;s__s3__tmp__new_cipher__algorithms==256;s__bbio==1;skip==0;tmp___2==0;tmp___3==1;s__s3__tmp__cert_req==0;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_connect_good==0;tmp___4==1;tmp==0;s__hit==0;s__wbio==0;tmp___5==1;s__s3__tmp__new_cipher==0; s__in_handshake ++ 104 104 tmp___8==0;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect_good==0;s__version==66048;s__s3__tmp__new_compression__id==0;tmp___6==1;skip==0;s__s3__tmp__new_cipher__algorithms==256;tmp___1==12288;tmp___4==1;s__state==12292;s__ctx__stats__sess_hit==0;tmp___5==1;tmp___2==0;s__s3__tmp__new_compression==0;tmp___7==0;tmp___3==1;s__info_callback==0;s__hit==0;s__debug==0;s__bbio==1;s__s3__tmp__new_cipher==0;s__wbio==0;s__ctx__info_callback==-1;ret==-1;tmp___9==0;tmp___0==0;s__ctx__stats__sess_connect_renegotiate==0;cb==-1;tmp==0;s__in_handshake==1;blastFlag==0;initial_state==12292;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_connect==0; condition-false [!(tmp___1 - 12288)] 106 106 tmp___5==1;tmp___4==1;s__debug==0;s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect==0;tmp___6==1;initial_state==12292;s__state==12292;ret==-1;s__in_handshake==1;s__info_callback==0;s__s3__tmp__new_cipher__algorithms==256;tmp___1==12288;s__ctx__stats__sess_hit==0;s__hit==0;s__ctx__stats__sess_connect_good==0;tmp___7==0;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect_renegotiate==0;tmp___0==0;s__wbio==0;s__s3__tmp__reuse_message==-1;tmp==0;s__s3__tmp__new_cipher==0;s__s3__tmp__new_compression__id==0;s__version==66048;s__bbio==1;skip==0;cb==-1;tmp___8==0;tmp___9==0;tmp___2==0;s__ctx__info_callback==-1;tmp___3==1;blastFlag==0; [1] 114 114 tmp___2==0;tmp___7==0;s__s3__tmp__reuse_message==-1;tmp___8==0;tmp___5==1;s__state==12292;s__in_handshake==1;blastFlag==0;s__bbio==1;skip==0;s__s3__tmp__new_compression==0;s__version==66048;tmp___3==1;s__s3__tmp__new_cipher==0;tmp___6==1;initial_state==12292;s__debug==0;tmp___4==1;tmp___1==12288;ret==-1;s__ctx__stats__sess_connect==0;cb==-1;s__wbio==0;s__info_callback==0;s__ctx__stats__sess_connect_good==0;tmp==0;s__ctx__stats__sess_connect_renegotiate==0;s__hit==0;s__s3__tmp__new_compression__id==0;s__s3__tmp__new_cipher__algorithms==256;tmp___9==0;tmp___0==0;s__s3__tmp__cert_req==0;s__ctx__info_callback==-1;s__ctx__stats__sess_hit==0; state = s__state 117 117 s__s3__tmp__cert_req==0;s__ctx__stats__sess_hit==0;tmp___8==0;s__ctx__stats__sess_connect==0;s__ctx__stats__sess_connect_good==0;s__wbio==0;s__bbio==1;tmp___0==0;s__debug==0;s__ctx__stats__sess_connect_renegotiate==0;tmp___7==0;s__info_callback==0;state==12292;tmp___6==1;tmp___1==12288;skip==0;initial_state==12292;s__s3__tmp__new_compression==0;ret==-1;tmp___9==0;s__in_handshake==1;s__s3__tmp__reuse_message==-1;cb==-1;s__version==66048;s__ctx__info_callback==-1;tmp___2==0;tmp___3==1;tmp==0;s__s3__tmp__new_cipher__algorithms==256;s__state==12292;s__hit==0;blastFlag==0;tmp___5==1;s__s3__tmp__new_cipher==0;s__s3__tmp__new_compression__id==0;tmp___4==1; [s__state == 12292] 119 119 s__s3__tmp__cert_req==0;tmp___5==1;blastFlag==0;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_hit==0;s__wbio==0;tmp___0==0;s__ctx__info_callback==-1;s__version==66048;s__s3__tmp__new_compression==0;tmp___9==0;s__state==12292;tmp___8==0;s__bbio==1;s__s3__tmp__new_cipher__algorithms==256;tmp___3==1;tmp___2==0;tmp==0;tmp___7==0;s__ctx__stats__sess_connect_renegotiate==0;s__s3__tmp__new_compression__id==0;state==12292;s__s3__tmp__reuse_message==-1;s__in_handshake==1;tmp___4==1;tmp___6==1;skip==0;initial_state==12292;s__info_callback==0;ret==-1;cb==-1;s__hit==0;s__debug==0;tmp___1==12288;s__ctx__stats__sess_connect_good==0;s__ctx__stats__sess_connect==0; s__new_session = 1 255 255 s__state = 4096 257 257 s__ctx__stats__sess_connect_renegotiate ++ 259 259 skip==0;tmp___2==0;initial_state==12292;s__ctx__stats__sess_connect==0;s__state==4096;tmp___8==0;s__ctx__stats__sess_hit==0;tmp___3==1;blastFlag==0;s__ctx__info_callback==-1;tmp___5==1;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__reuse_message==-1;s__info_callback==0;s__in_handshake==1;tmp___1==12288;ret==-1;s__bbio==1;s__s3__tmp__new_cipher==0;state==12292;s__s3__tmp__new_compression__id==0;s__wbio==0;s__hit==0;s__debug==0;tmp___0==0;s__version==66048;s__s3__tmp__new_compression==0;tmp___4==1;s__ctx__stats__sess_connect_good==0;tmp___7==0;s__s3__tmp__new_cipher__algorithms==256;tmp==0;s__new_session==1;tmp___6==1;cb==-1;s__s3__tmp__cert_req==0;tmp___9==0; s__server = 0 265 265 s__new_session==1;tmp___1==12288;s__s3__tmp__new_compression==0;tmp___9==0;s__wbio==0;tmp___2==0;s__s3__tmp__reuse_message==-1;s__s3__tmp__cert_req==0;initial_state==12292;s__hit==0;tmp==0;s__in_handshake==1;s__bbio==1;s__ctx__stats__sess_connect_good==0;s__ctx__stats__sess_hit==0;s__s3__tmp__new_cipher__algorithms==256;cb==-1;s__s3__tmp__new_compression__id==0;tmp___6==1;tmp___8==0;s__state==4096;s__debug==0;tmp___3==1;s__ctx__stats__sess_connect_renegotiate==1;s__info_callback==0;state==12292;tmp___0==0;s__ctx__info_callback==-1;ret==-1;blastFlag==0;tmp___4==1;tmp___5==1;s__s3__tmp__new_cipher==0;s__version==66048;s__server==0;tmp___7==0;s__ctx__stats__sess_connect==0;skip==0; [cb != 0] 267 267 ret==-1;s__new_session==1;tmp___6==1;s__in_handshake==1;blastFlag==0;s__debug==0;s__hit==0;cb==-1;s__info_callback==0;s__ctx__stats__sess_connect_good==0;skip==0;tmp___4==1;tmp___0==0;tmp___7==0;s__ctx__stats__sess_connect==0;tmp___3==1;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__new_compression__id==0;tmp___5==1;s__s3__tmp__cert_req==0;s__wbio==0;tmp___8==0;tmp___1==12288;s__bbio==1;tmp==0;s__state==4096;s__s3__tmp__new_cipher==0;tmp___2==0;tmp___9==0;s__s3__tmp__new_compression==0;state==12292;s__ctx__stats__sess_hit==0;initial_state==12292;s__ctx__info_callback==-1;s__version==66048;s__s3__tmp__reuse_message==-1;s__server==0; __cil_tmp55 = s__version - 65280 272 272 s__in_handshake==1;skip==0;s__s3__tmp__new_compression__id==0;tmp___4==1;tmp___5==1;s__bbio==1;s__ctx__stats__sess_connect==0;s__wbio==0;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__reuse_message==-1;s__s3__tmp__new_compression==0;s__s3__tmp__new_cipher__algorithms==256;ret==-1;tmp___9==0;s__ctx__stats__sess_connect_good==0;s__ctx__info_callback==-1;s__s3__tmp__cert_req==0;tmp___7==0;tmp==0;tmp___2==0;cb==-1;s__info_callback==0;__cil_tmp55==768;state==12292;s__ctx__stats__sess_hit==0;tmp___8==0;initial_state==12292;tmp___0==0;tmp___3==1;s__state==4096;s__debug==0;tmp___1==12288;blastFlag==0;tmp___6==1;s__hit==0;s__new_session==1;s__server==0;s__s3__tmp__new_cipher==0;s__version==66048; condition-false [!(__cil_tmp55 != 768)] 274 274 s__type = 4096 281 281 tmp___0==0;s__ctx__stats__sess_connect_good==0;s__type==4096;s__new_session==1;tmp___1==12288;state==12292;tmp___3==1;s__hit==0;s__ctx__stats__sess_hit==0;s__s3__tmp__new_compression==0;s__wbio==0;tmp___2==0;tmp___6==1;s__in_handshake==1;s__s3__tmp__new_cipher==0;s__debug==0;tmp___8==0;skip==0;tmp==0;tmp___5==1;s__s3__tmp__new_compression__id==0;s__ctx__info_callback==-1;s__state==4096;cb==-1;s__version==66048;s__ctx__stats__sess_connect==0;s__s3__tmp__new_cipher__algorithms==256;tmp___9==0;s__s3__tmp__reuse_message==-1;ret==-1;blastFlag==0;s__ctx__stats__sess_connect_renegotiate==1;__cil_tmp55==768;s__info_callback==0;s__server==0;initial_state==12292;s__bbio==1;s__s3__tmp__cert_req==0;tmp___7==0;tmp___4==1; [s__init_buf___0 == 0] 283 283 buf = __VERIFIER_nondet_int() 285 285 condition-false [!(buf == 0)] 287 287 tmp___6==1;s__s3__tmp__new_cipher==0;s__new_session==1;buf==1;s__type==4096;s__bbio==1;s__s3__tmp__reuse_message==-1;tmp___5==1;skip==0;s__info_callback==0;tmp___1==12288;s__wbio==0;tmp___2==0;ret==-1;s__debug==0;cb==-1;s__ctx__stats__sess_hit==0;tmp___8==0;s__ctx__info_callback==-1;s__ctx__stats__sess_connect_renegotiate==1;s__version==66048;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__new_compression==0;s__init_buf___0==0;s__s3__tmp__new_compression__id==0;initial_state==12292;s__server==0;s__s3__tmp__cert_req==0;state==12292;s__in_handshake==1;__cil_tmp55==768;s__ctx__stats__sess_connect_good==0;blastFlag==0;tmp___3==1;s__hit==0;s__ctx__stats__sess_connect==0;tmp___0==0;tmp==0;tmp___9==0;tmp___4==1;s__state==4096;tmp___7==0; condition-false [!(! tmp___3)] 293 293 s__init_buf___0 = buf 299 299 state==12292;tmp___7==0;tmp==0;s__s3__tmp__new_compression==0;tmp___6==1;tmp___8==0;ret==-1;s__version==66048;tmp___1==12288;s__s3__tmp__reuse_message==-1;cb==-1;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_connect_good==0;s__server==0;s__s3__tmp__new_cipher__algorithms==256;s__state==4096;s__s3__tmp__new_cipher==0;s__debug==0;s__in_handshake==1;initial_state==12292;tmp___5==1;tmp___9==0;s__s3__tmp__cert_req==0;s__info_callback==0;s__ctx__stats__sess_hit==0;s__wbio==0;s__ctx__info_callback==-1;buf==1;s__new_session==1;tmp___3==1;__cil_tmp55==768;s__ctx__stats__sess_connect_renegotiate==1;s__bbio==1;blastFlag==0;s__init_buf___0==1;s__hit==0;tmp___2==0;s__type==4096;skip==0;s__ctx__stats__sess_connect==0;tmp___4==1;tmp___0==0; condition-false [!(! tmp___4)] 302 302 s__type==4096;tmp___9==0;s__wbio==0;s__s3__tmp__new_compression==0;buf==1;s__s3__tmp__cert_req==0;state==12292;s__s3__tmp__reuse_message==-1;s__s3__tmp__new_cipher__algorithms==256;cb==-1;tmp==0;s__info_callback==0;s__hit==0;tmp___2==0;tmp___5==1;s__debug==0;s__ctx__stats__sess_connect_renegotiate==1;s__init_buf___0==1;s__s3__tmp__new_cipher==0;ret==-1;s__ctx__stats__sess_connect_good==0;tmp___4==1;s__state==4096;blastFlag==0;s__s3__tmp__new_compression__id==0;tmp___3==1;tmp___0==0;s__new_session==1;tmp___7==0;s__server==0;s__version==66048;tmp___8==0;skip==0;s__bbio==1;s__in_handshake==1;s__ctx__stats__sess_hit==0;s__ctx__stats__sess_connect==0;initial_state==12292;s__ctx__info_callback==-1;tmp___6==1;__cil_tmp55==768;tmp___1==12288; condition-false [!(! tmp___5)] 308 308 s__state = 4368 314 314 s__ctx__stats__sess_connect ++ 316 316 s__init_num = 0 318 318 s__s3__tmp__cert_req==0;tmp___7==0;tmp___1==12288;s__s3__tmp__new_compression__id==0;tmp___4==1;s__wbio==0;tmp___8==0;cb==-1;buf==1;s__bbio==1;s__ctx__stats__sess_connect_renegotiate==1;state==12292;s__s3__tmp__new_cipher==0;__cil_tmp55==768;s__in_handshake==1;s__info_callback==0;s__ctx__info_callback==-1;s__init_num==0;skip==0;s__s3__tmp__new_cipher__algorithms==256;s__init_buf___0==1;s__debug==0;tmp___9==0;s__s3__tmp__new_compression==0;tmp___0==0;s__ctx__stats__sess_hit==0;s__type==4096;s__version==66048;ret==-1;tmp==0;tmp___6==1;s__server==0;s__state==4368;tmp___3==1;s__hit==0;s__ctx__stats__sess_connect==1;tmp___2==0;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_connect_good==0;tmp___5==1;s__new_session==1;blastFlag==0;initial_state==12292; condition-false [!(! s__s3__tmp__reuse_message)] 710 710 s__s3__tmp__new_cipher__algorithms==256;buf==1;s__ctx__stats__sess_connect_good==0;s__info_callback==0;s__wbio==0;s__ctx__info_callback==-1;s__init_buf___0==1;s__ctx__stats__sess_connect==1;state==12292;blastFlag==0;s__in_handshake==1;tmp___5==1;tmp___0==0;s__init_num==0;s__server==0;s__version==66048;__cil_tmp55==768;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___4==1;s__s3__tmp__new_compression__id==0;tmp___3==1;tmp___7==0;ret==-1;tmp___8==0;s__new_session==1;tmp___9==0;tmp___2==0;s__s3__tmp__cert_req==0;s__debug==0;s__hit==0;s__state==4368;s__bbio==1;tmp___6==1;s__type==4096;cb==-1;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_hit==0;tmp==0;initial_state==12292;tmp___1==12288;s__s3__tmp__new_compression==0;skip==0; skip = 0 737 737 tmp___3==1;ret==-1;s__ctx__stats__sess_connect==1;s__s3__tmp__new_cipher==0;s__version==66048;s__hit==0;blastFlag==0;s__init_num==0;s__debug==0;tmp___1==12288;s__s3__tmp__reuse_message==-1;state==12292;s__type==4096;tmp___5==1;tmp___6==1;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_compression__id==0;s__s3__tmp__new_compression==0;s__server==0;tmp___2==0;tmp___4==1;s__ctx__stats__sess_hit==0;s__state==4368;s__ctx__stats__sess_connect_good==0;s__bbio==1;s__new_session==1;s__info_callback==0;s__wbio==0;initial_state==12292;s__s3__tmp__new_cipher__algorithms==256;s__ctx__info_callback==-1;s__in_handshake==1;s__s3__tmp__cert_req==0;tmp___8==0;s__init_buf___0==1;tmp___9==0;__cil_tmp55==768;tmp___0==0;buf==1;skip==0;tmp==0;tmp___7==0;cb==-1; [1] 114 114 s__s3__tmp__new_cipher==0;skip==0;s__new_session==1;tmp==0;tmp___3==1;s__s3__tmp__new_compression__id==0;s__bbio==1;s__hit==0;s__type==4096;tmp___8==0;tmp___1==12288;s__ctx__info_callback==-1;tmp___6==1;buf==1;__cil_tmp55==768;s__ctx__stats__sess_connect_renegotiate==1;tmp___7==0;initial_state==12292;s__server==0;s__s3__tmp__reuse_message==-1;tmp___0==0;tmp___9==0;blastFlag==0;s__s3__tmp__cert_req==0;s__debug==0;s__in_handshake==1;s__wbio==0;tmp___2==0;s__state==4368;tmp___5==1;ret==-1;s__info_callback==0;tmp___4==1;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__new_compression==0;state==12292;s__init_num==0;s__ctx__stats__sess_hit==0;cb==-1;s__ctx__stats__sess_connect==1;s__version==66048;s__ctx__stats__sess_connect_good==0;s__init_buf___0==1; state = s__state 117 117 tmp___8==0;s__hit==0;tmp___6==1;tmp___1==12288;tmp___9==0;s__debug==0;blastFlag==0;s__s3__tmp__new_compression==0;tmp___4==1;s__bbio==1;s__init_buf___0==1;s__new_session==1;s__wbio==0;s__version==66048;s__ctx__info_callback==-1;skip==0;ret==-1;state==4368;s__s3__tmp__cert_req==0;s__state==4368;s__server==0;s__s3__tmp__new_compression__id==0;tmp___3==1;s__ctx__stats__sess_connect_good==0;s__s3__tmp__reuse_message==-1;buf==1;s__s3__tmp__new_cipher==0;tmp___7==0;s__s3__tmp__new_cipher__algorithms==256;tmp==0;s__in_handshake==1;tmp___2==0;tmp___5==1;s__type==4096;__cil_tmp55==768;s__ctx__stats__sess_connect_renegotiate==1;cb==-1;s__info_callback==0;s__ctx__stats__sess_connect==1;tmp___0==0;s__ctx__stats__sess_hit==0;initial_state==12292;s__init_num==0; condition-false [!(s__state == 12292)] 119 119 tmp___9==0;blastFlag==0;s__in_handshake==1;tmp==0;__cil_tmp55==768;s__ctx__stats__sess_connect==1;buf==1;s__ctx__info_callback==-1;s__info_callback==0;skip==0;s__wbio==0;s__s3__tmp__new_cipher==0;s__s3__tmp__new_compression==0;tmp___6==1;s__ctx__stats__sess_connect_good==0;s__s3__tmp__reuse_message==-1;tmp___3==1;s__s3__tmp__cert_req==0;state==4368;s__type==4096;s__debug==0;s__state==4368;s__s3__tmp__new_cipher__algorithms==256;initial_state==12292;tmp___0==0;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_hit==0;s__init_buf___0==1;s__ctx__stats__sess_connect_renegotiate==1;tmp___5==1;s__server==0;tmp___1==12288;cb==-1;s__init_num==0;tmp___4==1;s__new_session==1;s__bbio==1;s__version==66048;tmp___8==0;tmp___2==0;tmp___7==0;s__hit==0;ret==-1; condition-false [!(s__state == 16384)] 123 123 s__s3__tmp__reuse_message==-1;ret==-1;tmp___4==1;s__s3__tmp__new_compression==0;tmp___7==0;cb==-1;tmp___9==0;tmp___3==1;s__state==4368;s__debug==0;s__ctx__stats__sess_connect_good==0;s__s3__tmp__cert_req==0;s__hit==0;s__init_num==0;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_cipher__algorithms==256;tmp___8==0;s__server==0;s__version==66048;state==4368;initial_state==12292;__cil_tmp55==768;s__in_handshake==1;tmp___1==12288;s__init_buf___0==1;tmp==0;s__ctx__stats__sess_connect==1;s__s3__tmp__new_compression__id==0;skip==0;s__wbio==0;blastFlag==0;tmp___5==1;s__info_callback==0;s__new_session==1;s__ctx__stats__sess_hit==0;tmp___2==0;s__ctx__info_callback==-1;s__s3__tmp__new_cipher==0;tmp___0==0;s__bbio==1;s__type==4096;buf==1;tmp___6==1; condition-false [!(s__state == 4096)] 127 127 tmp___2==0;s__new_session==1;tmp___8==0;skip==0;tmp___7==0;s__s3__tmp__new_compression==0;s__ctx__stats__sess_hit==0;tmp___6==1;blastFlag==0;tmp___4==1;tmp==0;state==4368;s__init_num==0;tmp___5==1;initial_state==12292;__cil_tmp55==768;s__init_buf___0==1;s__s3__tmp__cert_req==0;s__info_callback==0;s__s3__tmp__new_cipher__algorithms==256;cb==-1;s__type==4096;s__ctx__info_callback==-1;s__s3__tmp__new_cipher==0;s__bbio==1;s__version==66048;tmp___0==0;s__ctx__stats__sess_connect==1;s__wbio==0;s__state==4368;s__hit==0;ret==-1;s__debug==0;tmp___9==0;s__in_handshake==1;tmp___1==12288;s__s3__tmp__reuse_message==-1;s__server==0;tmp___3==1;s__ctx__stats__sess_connect_good==0;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_compression__id==0;buf==1; condition-false [!(s__state == 20480)] 131 131 tmp___8==0;s__server==0;s__ctx__stats__sess_connect==1;s__in_handshake==1;s__type==4096;s__hit==0;s__ctx__info_callback==-1;state==4368;ret==-1;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_hit==0;s__version==66048;s__s3__tmp__new_cipher__algorithms==256;initial_state==12292;tmp___9==0;__cil_tmp55==768;s__s3__tmp__new_compression==0;s__init_buf___0==1;tmp==0;s__info_callback==0;buf==1;cb==-1;tmp___4==1;s__wbio==0;s__debug==0;s__s3__tmp__reuse_message==-1;s__s3__tmp__new_compression__id==0;tmp___1==12288;s__s3__tmp__cert_req==0;s__init_num==0;s__new_session==1;tmp___3==1;skip==0;tmp___5==1;blastFlag==0;tmp___7==0;tmp___2==0;s__s3__tmp__new_cipher==0;s__state==4368;s__ctx__stats__sess_connect_good==0;tmp___6==1;tmp___0==0;s__bbio==1; condition-false [!(s__state == 4099)] 135 135 cb==-1;s__debug==0;s__ctx__stats__sess_connect==1;s__s3__tmp__new_cipher==0;s__init_buf___0==1;ret==-1;s__init_num==0;state==4368;s__s3__tmp__new_compression==0;s__version==66048;s__in_handshake==1;s__wbio==0;tmp==0;tmp___1==12288;s__s3__tmp__new_compression__id==0;s__state==4368;tmp___8==0;skip==0;tmp___7==0;s__ctx__stats__sess_connect_renegotiate==1;blastFlag==0;tmp___3==1;s__s3__tmp__reuse_message==-1;s__hit==0;s__info_callback==0;s__type==4096;tmp___0==0;initial_state==12292;s__s3__tmp__new_cipher__algorithms==256;__cil_tmp55==768;s__bbio==1;tmp___4==1;tmp___5==1;s__s3__tmp__cert_req==0;s__new_session==1;tmp___9==0;buf==1;s__server==0;s__ctx__info_callback==-1;s__ctx__stats__sess_hit==0;tmp___2==0;s__ctx__stats__sess_connect_good==0;tmp___6==1; [s__state == 4368] 139 139 tmp___7==0;initial_state==12292;s__s3__tmp__reuse_message==-1;ret==-1;tmp___2==0;tmp___4==1;s__new_session==1;s__s3__tmp__new_compression__id==0;s__state==4368;s__s3__tmp__new_compression==0;tmp___6==1;tmp==0;s__type==4096;tmp___1==12288;tmp___3==1;s__in_handshake==1;__cil_tmp55==768;s__wbio==0;s__ctx__stats__sess_connect==1;tmp___5==1;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_hit==0;s__init_buf___0==1;s__bbio==1;blastFlag==0;tmp___8==0;s__init_num==0;s__info_callback==0;s__debug==0;s__s3__tmp__new_cipher==0;state==4368;s__ctx__info_callback==-1;skip==0;s__ctx__stats__sess_connect_good==0;cb==-1;s__s3__tmp__cert_req==0;s__hit==0;s__version==66048;tmp___0==0;s__server==0;s__s3__tmp__new_cipher__algorithms==256;buf==1;tmp___9==0; s__shutdown = 0 323 323 ret = __VERIFIER_nondet_int() 325 325 [blastFlag == 0] 327 327 blastFlag = 1 329 329 tmp___7==0;tmp___5==1;s__s3__tmp__cert_req==0;tmp___0==0;s__type==4096;state==4368;s__shutdown==0;s__new_session==1;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_connect_good==0;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__new_cipher==0;__cil_tmp55==768;s__state==4368;s__ctx__info_callback==-1;s__hit==0;cb==-1;blastFlag==1;tmp___8==0;tmp___3==1;s__info_callback==0;tmp___1==12288;ret==1;buf==1;tmp___2==0;s__wbio==0;s__bbio==1;s__ctx__stats__sess_connect_renegotiate==1;skip==0;s__server==0;s__init_buf___0==1;initial_state==12292;tmp==0;s__ctx__stats__sess_hit==0;s__in_handshake==1;s__s3__tmp__new_compression==0;tmp___6==1;s__s3__tmp__reuse_message==-1;tmp___4==1;s__debug==0;s__ctx__stats__sess_connect==1;s__init_num==0;s__version==66048;tmp___9==0; condition-false [!(ret <= 0)] 332 332 s__state = 4384 336 336 s__init_num = 0 338 338 tmp___6==1;s__ctx__stats__sess_connect_good==0;s__init_num==0;s__new_session==1;tmp___0==0;s__version==66048;tmp___7==0;tmp___1==12288;s__s3__tmp__new_compression__id==0;s__ctx__info_callback==-1;s__s3__tmp__new_compression==0;blastFlag==1;s__s3__tmp__cert_req==0;tmp___2==0;s__s3__tmp__new_cipher__algorithms==256;state==4368;tmp___4==1;s__init_buf___0==1;tmp___8==0;s__type==4096;s__s3__tmp__new_cipher==0;skip==0;cb==-1;s__ctx__stats__sess_connect_renegotiate==1;s__bbio==1;s__shutdown==0;tmp___3==1;s__ctx__stats__sess_connect==1;s__wbio==0;tmp___5==1;s__state==4384;tmp___9==0;s__server==0;initial_state==12292;s__in_handshake==1;ret==1;s__hit==0;s__s3__tmp__reuse_message==-1;buf==1;__cil_tmp55==768;s__debug==0;s__info_callback==0;tmp==0;s__ctx__stats__sess_hit==0; [s__bbio != s__wbio] 340 340 s__ctx__stats__sess_connect==1;s__s3__tmp__new_cipher==0;ret==1;s__ctx__stats__sess_connect_good==0;tmp___2==0;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__cert_req==0;tmp___8==0;tmp==0;s__s3__tmp__reuse_message==-1;tmp___5==1;s__server==0;s__version==66048;s__s3__tmp__new_compression__id==0;tmp___4==1;initial_state==12292;tmp___9==0;blastFlag==1;s__hit==0;s__state==4384;s__init_num==0;s__debug==0;tmp___1==12288;tmp___7==0;s__init_buf___0==1;skip==0;s__info_callback==0;s__bbio==1;state==4368;s__ctx__stats__sess_hit==0;tmp___3==1;buf==1;s__type==4096;s__ctx__info_callback==-1;s__s3__tmp__new_compression==0;cb==-1;s__in_handshake==1;__cil_tmp55==768;tmp___6==1;s__shutdown==0;s__wbio==0;tmp___0==0;s__s3__tmp__new_cipher__algorithms==256;s__new_session==1; condition-false [!(! s__s3__tmp__reuse_message)] 710 710 s__bbio==1;s__ctx__stats__sess_connect_renegotiate==1;s__version==66048;tmp___4==1;tmp___2==0;buf==1;s__info_callback==0;__cil_tmp55==768;s__s3__tmp__new_compression==0;tmp___8==0;tmp___9==0;state==4368;skip==0;s__ctx__stats__sess_connect==1;s__state==4384;s__init_num==0;s__init_buf___0==1;s__hit==0;s__s3__tmp__new_cipher==0;s__type==4096;s__in_handshake==1;tmp___5==1;s__ctx__info_callback==-1;initial_state==12292;s__ctx__stats__sess_hit==0;tmp___7==0;s__s3__tmp__reuse_message==-1;s__debug==0;tmp___6==1;s__new_session==1;s__ctx__stats__sess_connect_good==0;s__s3__tmp__cert_req==0;cb==-1;tmp___3==1;s__server==0;tmp___0==0;s__s3__tmp__new_compression__id==0;tmp==0;s__shutdown==0;s__s3__tmp__new_cipher__algorithms==256;s__wbio==0;ret==1;tmp___1==12288;blastFlag==1; skip = 0 737 737 tmp___5==1;s__new_session==1;s__ctx__stats__sess_hit==0;s__wbio==0;tmp___2==0;s__debug==0;tmp___4==1;s__ctx__info_callback==-1;blastFlag==1;tmp___8==0;ret==1;s__version==66048;s__hit==0;buf==1;tmp___7==0;s__info_callback==0;s__in_handshake==1;s__type==4096;s__s3__tmp__new_cipher==0;s__state==4384;skip==0;state==4368;s__s3__tmp__reuse_message==-1;tmp___0==0;s__server==0;tmp==0;s__s3__tmp__new_compression__id==0;s__init_num==0;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect_renegotiate==1;cb==-1;tmp___1==12288;s__s3__tmp__new_compression==0;initial_state==12292;s__ctx__stats__sess_connect_good==0;s__init_buf___0==1;tmp___3==1;__cil_tmp55==768;s__ctx__stats__sess_connect==1;tmp___6==1;s__bbio==1;tmp___9==0;s__shutdown==0; [1] 114 114 s__ctx__stats__sess_hit==0;s__info_callback==0;tmp___9==0;s__bbio==1;skip==0;tmp___2==0;tmp___6==1;tmp___1==12288;tmp___0==0;tmp___5==1;ret==1;s__debug==0;s__init_buf___0==1;s__ctx__stats__sess_connect==1;tmp___7==0;blastFlag==1;__cil_tmp55==768;s__s3__tmp__new_cipher==0;s__new_session==1;tmp___4==1;cb==-1;initial_state==12292;buf==1;s__hit==0;s__type==4096;s__wbio==0;s__s3__tmp__cert_req==0;s__s3__tmp__reuse_message==-1;tmp==0;s__s3__tmp__new_compression==0;s__version==66048;s__ctx__stats__sess_connect_good==0;s__s3__tmp__new_compression__id==0;s__server==0;s__ctx__stats__sess_connect_renegotiate==1;s__state==4384;s__init_num==0;tmp___8==0;s__in_handshake==1;state==4368;s__ctx__info_callback==-1;s__s3__tmp__new_cipher__algorithms==256;tmp___3==1;s__shutdown==0; state = s__state 117 117 s__state==4384;s__init_num==0;cb==-1;s__ctx__stats__sess_hit==0;tmp==0;s__version==66048;s__shutdown==0;tmp___3==1;s__ctx__info_callback==-1;s__wbio==0;s__hit==0;tmp___4==1;s__new_session==1;s__s3__tmp__new_cipher__algorithms==256;__cil_tmp55==768;s__init_buf___0==1;s__info_callback==0;s__s3__tmp__reuse_message==-1;s__server==0;tmp___8==0;initial_state==12292;state==4384;s__s3__tmp__new_compression==0;tmp___6==1;ret==1;tmp___0==0;s__s3__tmp__new_compression__id==0;tmp___7==0;s__bbio==1;tmp___5==1;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_connect_good==0;s__s3__tmp__new_cipher==0;s__type==4096;s__s3__tmp__cert_req==0;buf==1;s__debug==0;tmp___1==12288;s__in_handshake==1;s__ctx__stats__sess_connect==1;tmp___2==0;skip==0;tmp___9==0;blastFlag==1; condition-false [!(s__state == 12292)] 119 119 s__ctx__info_callback==-1;tmp___6==1;s__init_num==0;cb==-1;blastFlag==1;tmp___3==1;s__type==4096;s__info_callback==0;buf==1;s__debug==0;s__in_handshake==1;s__s3__tmp__reuse_message==-1;tmp___5==1;__cil_tmp55==768;s__init_buf___0==1;s__hit==0;s__ctx__stats__sess_connect_good==0;ret==1;tmp___9==0;tmp___1==12288;s__shutdown==0;s__s3__tmp__new_cipher==0;s__s3__tmp__cert_req==0;tmp___7==0;tmp==0;s__bbio==1;s__server==0;state==4384;s__version==66048;initial_state==12292;s__s3__tmp__new_compression==0;tmp___4==1;s__s3__tmp__new_cipher__algorithms==256;skip==0;tmp___0==0;tmp___8==0;s__wbio==0;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_connect==1;s__ctx__stats__sess_hit==0;s__state==4384;tmp___2==0;s__new_session==1; condition-false [!(s__state == 16384)] 123 123 s__ctx__stats__sess_connect==1;initial_state==12292;s__s3__tmp__new_compression__id==0;s__in_handshake==1;s__hit==0;tmp___3==1;tmp___2==0;s__init_buf___0==1;s__init_num==0;s__s3__tmp__new_compression==0;s__ctx__info_callback==-1;ret==1;s__server==0;tmp___5==1;__cil_tmp55==768;blastFlag==1;s__bbio==1;tmp___6==1;state==4384;tmp==0;s__info_callback==0;cb==-1;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_connect_good==0;tmp___7==0;s__s3__tmp__new_cipher__algorithms==256;s__shutdown==0;s__ctx__stats__sess_connect_renegotiate==1;s__type==4096;s__new_session==1;tmp___0==0;s__s3__tmp__cert_req==0;s__debug==0;tmp___4==1;tmp___9==0;tmp___1==12288;s__wbio==0;s__state==4384;s__s3__tmp__new_cipher==0;tmp___8==0;s__version==66048;skip==0;s__ctx__stats__sess_hit==0;buf==1; condition-false [!(s__state == 4096)] 127 127 tmp___5==1;skip==0;s__s3__tmp__cert_req==0;state==4384;tmp___2==0;s__ctx__stats__sess_connect_good==0;initial_state==12292;tmp___9==0;s__init_buf___0==1;s__s3__tmp__new_compression__id==0;s__type==4096;s__state==4384;tmp___1==12288;tmp___6==1;tmp___8==0;s__new_session==1;s__info_callback==0;s__s3__tmp__reuse_message==-1;tmp___7==0;s__ctx__info_callback==-1;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_hit==0;s__init_num==0;s__wbio==0;s__debug==0;s__s3__tmp__new_cipher__algorithms==256;s__ctx__stats__sess_connect_renegotiate==1;s__shutdown==0;__cil_tmp55==768;buf==1;s__hit==0;blastFlag==1;cb==-1;s__ctx__stats__sess_connect==1;s__server==0;tmp==0;s__s3__tmp__new_compression==0;tmp___3==1;s__version==66048;ret==1;s__in_handshake==1;tmp___0==0;tmp___4==1;s__bbio==1; condition-false [!(s__state == 20480)] 131 131 s__state==4384;tmp==0;s__type==4096;tmp___0==0;s__s3__tmp__new_compression==0;s__hit==0;s__s3__tmp__cert_req==0;skip==0;s__init_num==0;ret==1;s__s3__tmp__new_cipher==0;s__server==0;s__init_buf___0==1;initial_state==12292;s__ctx__stats__sess_connect_renegotiate==1;tmp___8==0;__cil_tmp55==768;buf==1;s__s3__tmp__reuse_message==-1;blastFlag==1;s__ctx__stats__sess_hit==0;s__new_session==1;s__s3__tmp__new_compression__id==0;tmp___2==0;s__shutdown==0;s__in_handshake==1;cb==-1;tmp___5==1;state==4384;s__version==66048;tmp___7==0;tmp___1==12288;tmp___9==0;s__s3__tmp__new_cipher__algorithms==256;tmp___3==1;s__ctx__stats__sess_connect==1;s__wbio==0;s__info_callback==0;s__ctx__info_callback==-1;tmp___4==1;tmp___6==1;s__ctx__stats__sess_connect_good==0;s__bbio==1;s__debug==0; condition-false [!(s__state == 4099)] 135 135 tmp___2==0;s__init_num==0;buf==1;s__shutdown==0;s__s3__tmp__new_compression__id==0;cb==-1;s__wbio==0;s__hit==0;tmp___6==1;s__ctx__info_callback==-1;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_hit==0;s__init_buf___0==1;s__s3__tmp__reuse_message==-1;tmp==0;s__ctx__stats__sess_connect_good==0;blastFlag==1;s__info_callback==0;state==4384;s__bbio==1;skip==0;s__ctx__stats__sess_connect==1;s__server==0;tmp___7==0;tmp___1==12288;tmp___3==1;s__s3__tmp__new_compression==0;s__in_handshake==1;s__new_session==1;s__debug==0;__cil_tmp55==768;tmp___5==1;s__s3__tmp__new_cipher__algorithms==256;tmp___9==0;tmp___0==0;s__state==4384;tmp___4==1;s__version==66048;s__s3__tmp__new_cipher==0;ret==1;initial_state==12292;s__s3__tmp__cert_req==0;tmp___8==0;s__type==4096; condition-false [!(s__state == 4368)] 139 139 s__wbio==0;s__info_callback==0;s__type==4096;tmp___6==1;s__s3__tmp__cert_req==0;tmp___9==0;tmp___3==1;s__server==0;s__ctx__stats__sess_hit==0;tmp___2==0;s__s3__tmp__new_compression==0;s__init_buf___0==1;tmp___5==1;tmp___7==0;tmp___4==1;s__hit==0;s__s3__tmp__new_cipher==0;initial_state==12292;s__ctx__info_callback==-1;s__debug==0;cb==-1;blastFlag==1;s__new_session==1;s__ctx__stats__sess_connect==1;s__ctx__stats__sess_connect_renegotiate==1;s__version==66048;s__bbio==1;s__s3__tmp__new_cipher__algorithms==256;s__state==4384;tmp___8==0;tmp==0;tmp___1==12288;s__ctx__stats__sess_connect_good==0;ret==1;__cil_tmp55==768;skip==0;s__s3__tmp__new_compression__id==0;s__shutdown==0;s__in_handshake==1;tmp___0==0;buf==1;s__init_num==0;s__s3__tmp__reuse_message==-1;state==4384; condition-false [!(s__state == 4369)] 143 143 __cil_tmp55==768;s__s3__tmp__cert_req==0;s__s3__tmp__reuse_message==-1;s__bbio==1;s__new_session==1;s__hit==0;tmp___1==12288;tmp___7==0;s__ctx__stats__sess_hit==0;tmp___5==1;s__s3__tmp__new_cipher__algorithms==256;buf==1;s__init_buf___0==1;ret==1;s__ctx__stats__sess_connect==1;s__info_callback==0;s__init_num==0;state==4384;tmp___6==1;tmp___4==1;s__in_handshake==1;s__s3__tmp__new_compression__id==0;cb==-1;s__ctx__info_callback==-1;s__shutdown==0;s__state==4384;s__server==0;s__debug==0;s__s3__tmp__new_cipher==0;initial_state==12292;skip==0;tmp___3==1;s__s3__tmp__new_compression==0;s__type==4096;blastFlag==1;tmp___0==0;tmp___8==0;tmp___2==0;s__ctx__stats__sess_connect_renegotiate==1;s__wbio==0;s__ctx__stats__sess_connect_good==0;tmp___9==0;tmp==0;s__version==66048; [s__state == 4384] 147 147 s__wbio==0;tmp___7==0;initial_state==12292;skip==0;s__init_buf___0==1;s__new_session==1;tmp___8==0;s__s3__tmp__cert_req==0;__cil_tmp55==768;tmp___6==1;s__debug==0;s__s3__tmp__new_cipher==0;buf==1;s__init_num==0;s__type==4096;tmp___2==0;tmp==0;tmp___1==12288;s__ctx__stats__sess_connect_renegotiate==1;ret==1;tmp___3==1;s__ctx__stats__sess_hit==0;state==4384;s__state==4384;tmp___0==0;s__bbio==1;tmp___9==0;s__hit==0;s__s3__tmp__new_compression__id==0;s__version==66048;tmp___5==1;s__in_handshake==1;s__ctx__info_callback==-1;s__info_callback==0;tmp___4==1;s__ctx__stats__sess_connect==1;s__s3__tmp__new_cipher__algorithms==256;s__ctx__stats__sess_connect_good==0;s__shutdown==0;s__s3__tmp__reuse_message==-1;s__s3__tmp__new_compression==0;s__server==0;blastFlag==1;cb==-1; ret = __VERIFIER_nondet_int() 347 347 [blastFlag == 1] 349 349 blastFlag = 2 351 351 tmp___5==1;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_connect==1;s__info_callback==0;tmp==0;s__s3__tmp__new_cipher__algorithms==256;tmp___6==1;s__new_session==1;s__init_num==0;tmp___4==1;s__state==4384;s__ctx__stats__sess_hit==0;skip==0;s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect_good==0;tmp___8==0;s__debug==0;tmp___1==12288;tmp___3==1;s__version==66048;s__in_handshake==1;cb==-1;blastFlag==2;s__bbio==1;s__shutdown==0;s__s3__tmp__new_compression__id==0;buf==1;ret==1;initial_state==12292;__cil_tmp55==768;tmp___7==0;s__init_buf___0==1;s__hit==0;s__wbio==0;tmp___0==0;s__s3__tmp__new_cipher==0;s__server==0;state==4384;s__ctx__info_callback==-1;s__s3__tmp__reuse_message==-1;s__s3__tmp__cert_req==0;tmp___9==0;s__type==4096;tmp___2==0; condition-false [!(ret <= 0)] 354 354 s__init_buf___0==1;tmp___8==0;s__ctx__stats__sess_hit==0;__cil_tmp55==768;ret==1;s__info_callback==0;s__s3__tmp__new_compression__id==0;tmp___3==1;s__s3__tmp__reuse_message==-1;tmp___5==1;s__init_num==0;tmp___1==12288;initial_state==12292;s__in_handshake==1;buf==1;state==4384;blastFlag==2;s__ctx__info_callback==-1;s__state==4384;s__ctx__stats__sess_connect==1;s__new_session==1;s__server==0;s__bbio==1;tmp___4==1;tmp___2==0;s__wbio==0;tmp___0==0;s__s3__tmp__new_cipher==0;cb==-1;tmp___7==0;tmp___9==0;s__s3__tmp__cert_req==0;s__shutdown==0;s__type==4096;s__hit==0;s__s3__tmp__new_cipher__algorithms==256;skip==0;s__s3__tmp__new_compression==0;tmp==0;tmp___6==1;s__debug==0;s__ctx__stats__sess_connect_good==0;s__ctx__stats__sess_connect_renegotiate==1;s__version==66048; condition-false [!(\read(s__hit))] 358 358 s__state = 4400 363 363 tmp___4==1;s__debug==0;buf==1;tmp___6==1;skip==0;s__in_handshake==1;s__s3__tmp__new_cipher__algorithms==256;s__type==4096;tmp___7==0;s__s3__tmp__cert_req==0;s__server==0;cb==-1;s__init_buf___0==1;tmp___1==12288;s__wbio==0;tmp___3==1;s__version==66048;tmp___8==0;s__s3__tmp__reuse_message==-1;initial_state==12292;s__ctx__stats__sess_hit==0;s__s3__tmp__new_compression==0;s__shutdown==0;s__s3__tmp__new_compression__id==0;s__hit==0;s__init_num==0;tmp==0;blastFlag==2;s__ctx__stats__sess_connect_good==0;s__state==4400;s__info_callback==0;tmp___5==1;__cil_tmp55==768;s__bbio==1;s__ctx__info_callback==-1;ret==1;s__s3__tmp__new_cipher==0;tmp___9==0;tmp___2==0;s__new_session==1;s__ctx__stats__sess_connect==1;state==4384;tmp___0==0;s__ctx__stats__sess_connect_renegotiate==1; s__init_num = 0 366 366 s__state==4400;s__wbio==0;__cil_tmp55==768;tmp==0;s__shutdown==0;s__ctx__stats__sess_hit==0;blastFlag==2;tmp___2==0;s__ctx__stats__sess_connect==1;s__bbio==1;s__s3__tmp__new_cipher__algorithms==256;tmp___7==0;s__version==66048;tmp___1==12288;tmp___4==1;s__ctx__stats__sess_connect_renegotiate==1;tmp___8==0;s__server==0;s__s3__tmp__new_cipher==0;s__s3__tmp__reuse_message==-1;s__s3__tmp__cert_req==0;tmp___9==0;s__init_buf___0==1;s__info_callback==0;s__ctx__stats__sess_connect_good==0;s__hit==0;tmp___6==1;skip==0;s__debug==0;ret==1;s__init_num==0;buf==1;tmp___5==1;tmp___3==1;tmp___0==0;s__new_session==1;cb==-1;initial_state==12292;s__s3__tmp__new_compression==0;s__type==4096;s__in_handshake==1;s__s3__tmp__new_compression__id==0;s__ctx__info_callback==-1;state==4384; condition-false [!(! s__s3__tmp__reuse_message)] 710 710 s__s3__tmp__reuse_message==-1;s__debug==0;__cil_tmp55==768;s__new_session==1;s__bbio==1;s__s3__tmp__cert_req==0;s__shutdown==0;tmp___3==1;s__init_num==0;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_connect==1;s__s3__tmp__new_compression__id==0;state==4384;buf==1;s__s3__tmp__new_cipher__algorithms==256;tmp___7==0;tmp___8==0;tmp___5==1;ret==1;s__in_handshake==1;tmp==0;initial_state==12292;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect_good==0;s__type==4096;tmp___9==0;skip==0;tmp___2==0;s__state==4400;s__init_buf___0==1;cb==-1;tmp___4==1;blastFlag==2;s__version==66048;tmp___6==1;s__wbio==0;s__info_callback==0;s__hit==0;s__server==0;tmp___1==12288;s__ctx__stats__sess_hit==0;tmp___0==0;s__ctx__info_callback==-1; skip = 0 737 737 s__s3__tmp__reuse_message==-1;s__init_buf___0==1;s__s3__tmp__cert_req==0;s__s3__tmp__new_compression__id==0;s__state==4400;cb==-1;s__s3__tmp__new_cipher==0;s__hit==0;s__init_num==0;s__ctx__stats__sess_connect==1;initial_state==12292;tmp___1==12288;tmp___7==0;blastFlag==2;s__server==0;s__info_callback==0;s__ctx__stats__sess_connect_good==0;s__s3__tmp__new_compression==0;tmp==0;buf==1;s__s3__tmp__new_cipher__algorithms==256;s__ctx__stats__sess_connect_renegotiate==1;s__in_handshake==1;tmp___8==0;ret==1;s__new_session==1;__cil_tmp55==768;s__wbio==0;tmp___9==0;tmp___0==0;s__type==4096;s__ctx__stats__sess_hit==0;state==4384;tmp___3==1;tmp___4==1;tmp___6==1;s__version==66048;s__shutdown==0;skip==0;s__bbio==1;s__debug==0;tmp___2==0;tmp___5==1;s__ctx__info_callback==-1; [1] 114 114 buf==1;tmp___9==0;s__in_handshake==1;s__ctx__stats__sess_hit==0;s__ctx__stats__sess_connect==1;__cil_tmp55==768;state==4384;tmp___5==1;s__s3__tmp__new_cipher==0;tmp___8==0;tmp___1==12288;s__ctx__stats__sess_connect_good==0;s__wbio==0;s__info_callback==0;s__init_buf___0==1;s__shutdown==0;blastFlag==2;s__ctx__info_callback==-1;s__s3__tmp__reuse_message==-1;ret==1;tmp==0;s__type==4096;tmp___3==1;cb==-1;skip==0;s__s3__tmp__new_compression__id==0;initial_state==12292;tmp___2==0;s__init_num==0;tmp___0==0;tmp___4==1;s__s3__tmp__new_compression==0;s__s3__tmp__cert_req==0;s__version==66048;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_cipher__algorithms==256;tmp___7==0;tmp___6==1;s__hit==0;s__debug==0;s__bbio==1;s__server==0;s__new_session==1;s__state==4400; state = s__state 117 117 s__s3__tmp__new_compression__id==0;tmp___8==0;s__s3__tmp__reuse_message==-1;skip==0;s__state==4400;tmp___6==1;tmp___9==0;s__in_handshake==1;s__version==66048;s__s3__tmp__new_cipher__algorithms==256;blastFlag==2;tmp___4==1;s__init_num==0;s__info_callback==0;s__wbio==0;buf==1;tmp___0==0;s__s3__tmp__new_compression==0;s__new_session==1;s__debug==0;s__bbio==1;tmp___5==1;tmp___3==1;initial_state==12292;s__server==0;tmp___7==0;s__ctx__stats__sess_connect==1;__cil_tmp55==768;s__ctx__stats__sess_connect_renegotiate==1;tmp___1==12288;s__s3__tmp__new_cipher==0;s__s3__tmp__cert_req==0;state==4400;tmp==0;s__shutdown==0;s__init_buf___0==1;s__ctx__stats__sess_hit==0;s__type==4096;tmp___2==0;s__ctx__stats__sess_connect_good==0;s__ctx__info_callback==-1;ret==1;cb==-1;s__hit==0; condition-false [!(s__state == 12292)] 119 119 buf==1;tmp___2==0;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_connect_good==0;s__ctx__info_callback==-1;initial_state==12292;s__s3__tmp__new_compression==0;tmp___4==1;s__server==0;__cil_tmp55==768;s__wbio==0;s__s3__tmp__cert_req==0;tmp___6==1;s__hit==0;tmp___0==0;s__init_buf___0==1;ret==1;tmp___7==0;s__debug==0;s__s3__tmp__new_cipher__algorithms==256;blastFlag==2;s__shutdown==0;s__state==4400;s__init_num==0;tmp___5==1;skip==0;s__ctx__stats__sess_connect_renegotiate==1;cb==-1;s__ctx__stats__sess_hit==0;s__s3__tmp__reuse_message==-1;s__in_handshake==1;s__bbio==1;state==4400;s__info_callback==0;s__ctx__stats__sess_connect==1;s__new_session==1;tmp___9==0;tmp==0;tmp___3==1;tmp___8==0;s__type==4096;tmp___1==12288;s__s3__tmp__new_compression__id==0;s__version==66048; condition-false [!(s__state == 16384)] 123 123 s__s3__tmp__new_compression__id==0;s__in_handshake==1;ret==1;tmp___7==0;tmp___0==0;s__wbio==0;s__new_session==1;tmp___1==12288;s__s3__tmp__new_compression==0;cb==-1;s__s3__tmp__reuse_message==-1;tmp___6==1;tmp___5==1;s__s3__tmp__new_cipher==0;buf==1;skip==0;s__version==66048;state==4400;s__type==4096;s__hit==0;s__s3__tmp__new_cipher__algorithms==256;s__server==0;s__ctx__stats__sess_connect_renegotiate==1;__cil_tmp55==768;s__info_callback==0;s__ctx__stats__sess_hit==0;tmp==0;s__init_buf___0==1;tmp___8==0;s__ctx__stats__sess_connect_good==0;tmp___4==1;s__debug==0;s__state==4400;s__ctx__stats__sess_connect==1;tmp___2==0;s__shutdown==0;s__init_num==0;tmp___3==1;initial_state==12292;s__bbio==1;s__s3__tmp__cert_req==0;tmp___9==0;blastFlag==2;s__ctx__info_callback==-1; condition-false [!(s__state == 4096)] 127 127 initial_state==12292;s__bbio==1;tmp___5==1;s__shutdown==0;tmp___2==0;s__ctx__stats__sess_connect_renegotiate==1;s__debug==0;s__s3__tmp__new_compression==0;s__s3__tmp__new_cipher__algorithms==256;tmp___0==0;s__in_handshake==1;s__new_session==1;s__hit==0;s__wbio==0;s__s3__tmp__reuse_message==-1;s__s3__tmp__new_cipher==0;ret==1;blastFlag==2;tmp___8==0;skip==0;state==4400;tmp___4==1;tmp___9==0;s__s3__tmp__new_compression__id==0;tmp___3==1;s__init_buf___0==1;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect==1;tmp___1==12288;s__state==4400;s__init_num==0;s__ctx__info_callback==-1;s__ctx__stats__sess_connect_good==0;__cil_tmp55==768;s__version==66048;s__type==4096;buf==1;s__ctx__stats__sess_hit==0;tmp___6==1;tmp==0;cb==-1;s__server==0;s__info_callback==0;tmp___7==0; condition-false [!(s__state == 20480)] 131 131 buf==1;s__init_buf___0==1;s__version==66048;tmp___1==12288;tmp___0==0;s__debug==0;s__s3__tmp__cert_req==0;s__s3__tmp__new_cipher==0;blastFlag==2;s__bbio==1;s__ctx__info_callback==-1;s__state==4400;s__s3__tmp__reuse_message==-1;tmp==0;s__ctx__stats__sess_connect_good==0;s__type==4096;tmp___4==1;s__new_session==1;s__ctx__stats__sess_hit==0;ret==1;tmp___7==0;tmp___5==1;s__in_handshake==1;tmp___3==1;s__wbio==0;tmp___6==1;s__server==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___8==0;s__ctx__stats__sess_connect==1;__cil_tmp55==768;s__s3__tmp__new_cipher__algorithms==256;s__init_num==0;s__s3__tmp__new_compression==0;s__info_callback==0;s__shutdown==0;s__s3__tmp__new_compression__id==0;tmp___9==0;tmp___2==0;cb==-1;state==4400;initial_state==12292;skip==0;s__hit==0; condition-false [!(s__state == 4099)] 135 135 buf==1;s__ctx__stats__sess_connect_good==0;s__version==66048;initial_state==12292;s__debug==0;s__s3__tmp__cert_req==0;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__info_callback==-1;tmp___7==0;tmp___8==0;s__type==4096;s__ctx__stats__sess_hit==0;tmp==0;s__bbio==1;tmp___1==12288;s__new_session==1;s__s3__tmp__new_compression==0;s__s3__tmp__new_cipher__algorithms==256;s__hit==0;s__s3__tmp__new_cipher==0;s__init_num==0;tmp___9==0;s__s3__tmp__new_compression__id==0;skip==0;tmp___3==1;__cil_tmp55==768;s__wbio==0;s__state==4400;state==4400;blastFlag==2;cb==-1;tmp___2==0;s__shutdown==0;tmp___5==1;ret==1;s__server==0;s__init_buf___0==1;s__info_callback==0;s__ctx__stats__sess_connect==1;tmp___0==0;tmp___6==1;tmp___4==1;s__in_handshake==1; condition-false [!(s__state == 4368)] 139 139 s__s3__tmp__new_compression__id==0;skip==0;tmp___7==0;s__wbio==0;s__state==4400;tmp___2==0;s__s3__tmp__new_cipher==0;tmp___6==1;__cil_tmp55==768;cb==-1;buf==1;blastFlag==2;s__s3__tmp__new_cipher__algorithms==256;tmp___4==1;s__ctx__stats__sess_connect==1;s__ctx__stats__sess_connect_good==0;s__shutdown==0;s__type==4096;s__debug==0;s__s3__tmp__cert_req==0;s__s3__tmp__new_compression==0;s__s3__tmp__reuse_message==-1;s__version==66048;tmp___0==0;tmp==0;s__ctx__stats__sess_connect_renegotiate==1;s__init_buf___0==1;ret==1;state==4400;s__new_session==1;s__init_num==0;tmp___1==12288;tmp___8==0;s__in_handshake==1;initial_state==12292;s__info_callback==0;tmp___9==0;tmp___3==1;s__ctx__info_callback==-1;s__ctx__stats__sess_hit==0;s__server==0;s__bbio==1;s__hit==0;tmp___5==1; condition-false [!(s__state == 4369)] 143 143 tmp___3==1;s__info_callback==0;tmp==0;buf==1;s__new_session==1;tmp___8==0;s__init_num==0;tmp___0==0;tmp___1==12288;skip==0;s__server==0;s__debug==0;s__s3__tmp__new_cipher__algorithms==256;s__shutdown==0;tmp___9==0;tmp___5==1;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_hit==0;tmp___4==1;s__wbio==0;state==4400;s__s3__tmp__new_compression__id==0;ret==1;s__ctx__stats__sess_connect_good==0;initial_state==12292;s__s3__tmp__cert_req==0;tmp___6==1;s__s3__tmp__reuse_message==-1;s__ctx__info_callback==-1;s__state==4400;s__ctx__stats__sess_connect==1;cb==-1;s__type==4096;s__hit==0;s__version==66048;s__bbio==1;s__ctx__stats__sess_connect_renegotiate==1;tmp___7==0;blastFlag==2;s__init_buf___0==1;tmp___2==0;s__s3__tmp__new_compression==0;s__in_handshake==1;__cil_tmp55==768; condition-false [!(s__state == 4384)] 147 147 ret==1;skip==0;tmp___4==1;s__init_num==0;s__shutdown==0;tmp___1==12288;tmp___7==0;s__s3__tmp__new_cipher==0;s__debug==0;s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect==1;s__in_handshake==1;s__type==4096;s__state==4400;tmp___6==1;s__server==0;blastFlag==2;s__bbio==1;__cil_tmp55==768;s__version==66048;s__s3__tmp__new_cipher__algorithms==256;tmp___0==0;s__ctx__stats__sess_connect_renegotiate==1;s__new_session==1;cb==-1;initial_state==12292;tmp___9==0;s__ctx__info_callback==-1;state==4400;s__s3__tmp__new_compression__id==0;s__wbio==0;tmp___5==1;tmp___3==1;s__s3__tmp__cert_req==0;s__s3__tmp__reuse_message==-1;buf==1;s__ctx__stats__sess_hit==0;tmp___2==0;tmp___8==0;s__ctx__stats__sess_connect_good==0;tmp==0;s__info_callback==0;s__init_buf___0==1;s__hit==0; condition-false [!(s__state == 4385)] 151 151 s__ctx__stats__sess_hit==0;s__s3__tmp__cert_req==0;s__s3__tmp__new_compression==0;s__init_buf___0==1;s__ctx__stats__sess_connect==1;s__new_session==1;s__ctx__stats__sess_connect_good==0;s__shutdown==0;s__server==0;s__info_callback==0;s__s3__tmp__new_cipher__algorithms==256;s__debug==0;tmp___9==0;s__version==66048;tmp==0;tmp___3==1;ret==1;tmp___7==0;s__bbio==1;s__s3__tmp__new_cipher==0;blastFlag==2;state==4400;cb==-1;buf==1;tmp___1==12288;s__hit==0;__cil_tmp55==768;s__type==4096;tmp___2==0;s__ctx__info_callback==-1;s__init_num==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___4==1;s__s3__tmp__new_compression__id==0;s__s3__tmp__reuse_message==-1;tmp___5==1;skip==0;initial_state==12292;s__state==4400;s__wbio==0;tmp___6==1;tmp___8==0;tmp___0==0;s__in_handshake==1; [s__state == 4400] 155 155 tmp___0==0;tmp___3==1;s__wbio==0;s__debug==0;s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect_good==0;s__hit==0;tmp___6==1;buf==1;s__s3__tmp__new_cipher==0;s__in_handshake==1;ret==1;s__init_buf___0==1;tmp___4==1;s__s3__tmp__reuse_message==-1;s__shutdown==0;tmp___9==0;tmp___7==0;s__ctx__stats__sess_connect==1;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect_renegotiate==1;tmp==0;s__version==66048;s__s3__tmp__new_cipher__algorithms==256;s__ctx__stats__sess_hit==0;s__bbio==1;s__s3__tmp__new_compression__id==0;__cil_tmp55==768;cb==-1;s__info_callback==0;state==4400;s__ctx__info_callback==-1;s__server==0;tmp___8==0;s__new_session==1;initial_state==12292;tmp___2==0;skip==0;s__init_num==0;s__type==4096;tmp___5==1;tmp___1==12288;s__state==4400;blastFlag==2; condition-false [!(s__s3__tmp__new_cipher__algorithms - 256)] 371 371 ret = __VERIFIER_nondet_int() 376 376 [blastFlag == 2] 378 378 blastFlag = 3 380 380 tmp___3==1;s__debug==0;s__s3__tmp__reuse_message==-1;tmp___0==0;tmp==0;buf==1;state==4400;tmp___5==1;blastFlag==3;tmp___2==0;s__version==66048;s__init_buf___0==1;tmp___4==1;__cil_tmp55==768;s__init_num==0;tmp___9==0;s__server==0;s__info_callback==0;s__hit==0;ret==1;s__ctx__info_callback==-1;tmp___1==12288;s__ctx__stats__sess_connect_good==0;tmp___6==1;s__ctx__stats__sess_hit==0;s__ctx__stats__sess_connect_renegotiate==1;s__in_handshake==1;s__type==4096;s__s3__tmp__new_cipher==0;initial_state==12292;s__s3__tmp__cert_req==0;s__s3__tmp__new_compression==0;s__bbio==1;s__s3__tmp__new_cipher__algorithms==256;s__new_session==1;tmp___7==0;s__shutdown==0;s__ctx__stats__sess_connect==1;cb==-1;skip==0;s__wbio==0;s__s3__tmp__new_compression__id==0;s__state==4400;tmp___8==0; condition-false [!(ret <= 0)] 383 383 cb==-1;s__init_buf___0==1;tmp___7==0;tmp___5==1;s__ctx__info_callback==-1;s__init_num==0;s__ctx__stats__sess_hit==0;s__in_handshake==1;state==4400;buf==1;skip==0;s__state==4400;tmp___4==1;tmp___1==12288;s__s3__tmp__new_compression==0;s__server==0;tmp___2==0;__cil_tmp55==768;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect_renegotiate==1;s__wbio==0;s__s3__tmp__new_compression__id==0;tmp___9==0;initial_state==12292;s__info_callback==0;s__ctx__stats__sess_connect==1;s__hit==0;s__bbio==1;s__ctx__stats__sess_connect_good==0;s__shutdown==0;ret==1;s__s3__tmp__new_cipher__algorithms==256;tmp___6==1;tmp___3==1;tmp___8==0;s__type==4096;s__new_session==1;tmp==0;s__debug==0;s__s3__tmp__new_cipher==0;s__version==66048;tmp___0==0;s__s3__tmp__reuse_message==-1;blastFlag==3; s__state = 4416 388 388 s__init_num = 0 390 390 s__state==4416;state==4400;tmp___7==0;s__init_buf___0==1;tmp==0;tmp___1==12288;blastFlag==3;s__ctx__stats__sess_connect_good==0;tmp___6==1;s__server==0;tmp___2==0;s__init_num==0;s__hit==0;ret==1;s__s3__tmp__cert_req==0;tmp___3==1;s__bbio==1;s__type==4096;s__debug==0;s__in_handshake==1;s__version==66048;s__ctx__stats__sess_connect_renegotiate==1;s__shutdown==0;tmp___4==1;tmp___9==0;tmp___0==0;s__ctx__stats__sess_hit==0;s__s3__tmp__new_compression__id==0;s__wbio==0;s__s3__tmp__new_cipher==0;__cil_tmp55==768;s__new_session==1;tmp___5==1;s__s3__tmp__new_compression==0;s__ctx__info_callback==-1;s__s3__tmp__new_cipher__algorithms==256;cb==-1;skip==0;tmp___8==0;s__info_callback==0;initial_state==12292;s__ctx__stats__sess_connect==1;buf==1;s__s3__tmp__reuse_message==-1; condition-false [!(! s__s3__tmp__reuse_message)] 710 710 s__server==0;s__ctx__info_callback==-1;s__shutdown==0;s__s3__tmp__new_compression__id==0;s__type==4096;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__new_compression==0;tmp___5==1;s__wbio==0;tmp___7==0;state==4400;initial_state==12292;tmp___9==0;s__init_num==0;buf==1;s__s3__tmp__cert_req==0;s__new_session==1;tmp___0==0;tmp___8==0;tmp___2==0;s__info_callback==0;tmp___1==12288;skip==0;tmp==0;s__hit==0;s__debug==0;tmp___3==1;s__ctx__stats__sess_connect_good==0;s__bbio==1;blastFlag==3;s__version==66048;s__s3__tmp__new_cipher==0;cb==-1;tmp___6==1;s__ctx__stats__sess_connect==1;s__state==4416;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__reuse_message==-1;__cil_tmp55==768;s__ctx__stats__sess_hit==0;s__init_buf___0==1;s__in_handshake==1;ret==1;tmp___4==1; skip = 0 737 737 s__shutdown==0;blastFlag==3;s__s3__tmp__reuse_message==-1;tmp___9==0;s__s3__tmp__new_compression__id==0;s__version==66048;s__type==4096;tmp___2==0;ret==1;tmp___4==1;tmp___5==1;s__ctx__stats__sess_connect==1;s__init_buf___0==1;s__ctx__stats__sess_connect_renegotiate==1;tmp___6==1;state==4400;s__info_callback==0;buf==1;__cil_tmp55==768;tmp___3==1;skip==0;s__in_handshake==1;cb==-1;s__hit==0;s__s3__tmp__new_cipher==0;tmp___8==0;s__ctx__info_callback==-1;s__ctx__stats__sess_hit==0;s__ctx__stats__sess_connect_good==0;s__s3__tmp__cert_req==0;s__wbio==0;tmp___0==0;s__init_num==0;tmp==0;s__new_session==1;s__s3__tmp__new_compression==0;tmp___1==12288;initial_state==12292;tmp___7==0;s__state==4416;s__debug==0;s__bbio==1;s__server==0;s__s3__tmp__new_cipher__algorithms==256; [1] 114 114 __cil_tmp55==768;s__s3__tmp__reuse_message==-1;s__debug==0;s__init_num==0;s__info_callback==0;tmp==0;s__ctx__info_callback==-1;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect==1;tmp___5==1;s__s3__tmp__new_compression__id==0;ret==1;s__init_buf___0==1;s__s3__tmp__new_cipher__algorithms==256;s__type==4096;state==4400;tmp___3==1;s__version==66048;s__state==4416;tmp___9==0;s__new_session==1;s__s3__tmp__new_compression==0;tmp___0==0;s__wbio==0;tmp___6==1;cb==-1;initial_state==12292;s__shutdown==0;tmp___2==0;blastFlag==3;s__hit==0;tmp___7==0;skip==0;s__bbio==1;tmp___4==1;tmp___8==0;s__server==0;buf==1;s__ctx__stats__sess_connect_good==0;tmp___1==12288;s__ctx__stats__sess_hit==0;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_connect_renegotiate==1;s__in_handshake==1; state = s__state 117 117 s__in_handshake==1;s__type==4096;s__init_num==0;initial_state==12292;s__shutdown==0;tmp___3==1;s__s3__tmp__new_compression==0;skip==0;s__server==0;tmp==0;s__new_session==1;tmp___1==12288;s__init_buf___0==1;s__state==4416;s__hit==0;s__s3__tmp__cert_req==0;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_connect_good==0;tmp___2==0;s__bbio==1;ret==1;s__s3__tmp__new_compression__id==0;s__debug==0;s__s3__tmp__new_cipher==0;buf==1;s__s3__tmp__new_cipher__algorithms==256;s__wbio==0;tmp___8==0;tmp___4==1;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_hit==0;tmp___5==1;__cil_tmp55==768;s__info_callback==0;tmp___7==0;cb==-1;blastFlag==3;tmp___9==0;tmp___6==1;s__ctx__stats__sess_connect==1;tmp___0==0;s__ctx__info_callback==-1;state==4416;s__version==66048; condition-false [!(s__state == 12292)] 119 119 s__s3__tmp__reuse_message==-1;cb==-1;s__ctx__stats__sess_hit==0;tmp___4==1;s__s3__tmp__new_cipher__algorithms==256;state==4416;s__s3__tmp__cert_req==0;s__server==0;blastFlag==3;tmp___6==1;tmp___7==0;tmp___3==1;s__type==4096;initial_state==12292;s__s3__tmp__new_compression==0;tmp___5==1;buf==1;s__version==66048;s__init_num==0;s__hit==0;s__s3__tmp__new_cipher==0;s__init_buf___0==1;s__wbio==0;tmp___0==0;s__bbio==1;s__info_callback==0;s__state==4416;tmp___9==0;s__shutdown==0;s__ctx__info_callback==-1;s__new_session==1;ret==1;s__ctx__stats__sess_connect==1;skip==0;s__ctx__stats__sess_connect_good==0;s__s3__tmp__new_compression__id==0;tmp___1==12288;tmp==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___2==0;__cil_tmp55==768;s__debug==0;tmp___8==0;s__in_handshake==1; condition-false [!(s__state == 16384)] 123 123 tmp___3==1;s__ctx__stats__sess_connect_renegotiate==1;buf==1;s__debug==0;tmp___0==0;s__new_session==1;skip==0;s__s3__tmp__new_compression__id==0;s__ctx__info_callback==-1;s__s3__tmp__cert_req==0;tmp___1==12288;s__ctx__stats__sess_hit==0;cb==-1;tmp___7==0;s__type==4096;s__s3__tmp__new_cipher__algorithms==256;state==4416;s__info_callback==0;s__s3__tmp__reuse_message==-1;tmp==0;s__bbio==1;s__version==66048;tmp___6==1;s__init_buf___0==1;s__wbio==0;tmp___5==1;ret==1;s__hit==0;s__in_handshake==1;s__s3__tmp__new_compression==0;tmp___2==0;tmp___9==0;tmp___8==0;initial_state==12292;s__state==4416;s__ctx__stats__sess_connect_good==0;tmp___4==1;blastFlag==3;s__init_num==0;s__ctx__stats__sess_connect==1;s__s3__tmp__new_cipher==0;s__server==0;__cil_tmp55==768;s__shutdown==0; condition-false [!(s__state == 4096)] 127 127 s__s3__tmp__new_cipher==0;tmp___2==0;buf==1;initial_state==12292;tmp___7==0;s__s3__tmp__new_compression==0;tmp___8==0;__cil_tmp55==768;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___5==1;s__s3__tmp__cert_req==0;tmp___3==1;s__hit==0;s__init_num==0;s__ctx__stats__sess_connect_good==0;s__new_session==1;s__ctx__info_callback==-1;tmp___6==1;cb==-1;s__ctx__stats__sess_connect==1;tmp___1==12288;tmp==0;s__shutdown==0;s__s3__tmp__new_cipher__algorithms==256;s__server==0;tmp___0==0;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_hit==0;s__init_buf___0==1;s__bbio==1;ret==1;s__info_callback==0;s__state==4416;tmp___4==1;tmp___9==0;s__version==66048;s__debug==0;s__in_handshake==1;blastFlag==3;s__wbio==0;skip==0;s__type==4096;state==4416; condition-false [!(s__state == 20480)] 131 131 s__s3__tmp__cert_req==0;s__s3__tmp__new_cipher__algorithms==256;s__shutdown==0;skip==0;buf==1;s__new_session==1;s__ctx__info_callback==-1;s__s3__tmp__reuse_message==-1;tmp==0;s__init_buf___0==1;tmp___4==1;s__wbio==0;tmp___7==0;ret==1;tmp___9==0;cb==-1;tmp___1==12288;tmp___8==0;s__in_handshake==1;s__bbio==1;s__server==0;s__type==4096;tmp___3==1;s__info_callback==0;tmp___5==1;s__ctx__stats__sess_hit==0;s__ctx__stats__sess_connect==1;blastFlag==3;s__s3__tmp__new_compression==0;state==4416;s__init_num==0;s__version==66048;s__ctx__stats__sess_connect_good==0;__cil_tmp55==768;tmp___6==1;tmp___2==0;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_cipher==0;initial_state==12292;s__state==4416;s__debug==0;tmp___0==0;s__hit==0;s__s3__tmp__new_compression__id==0; condition-false [!(s__state == 4099)] 135 135 s__type==4096;tmp___6==1;buf==1;s__shutdown==0;tmp___9==0;__cil_tmp55==768;tmp___8==0;s__s3__tmp__new_cipher==0;tmp___7==0;s__ctx__stats__sess_hit==0;s__s3__tmp__new_compression__id==0;initial_state==12292;s__debug==0;tmp___1==12288;ret==1;s__s3__tmp__cert_req==0;s__server==0;s__new_session==1;tmp___4==1;state==4416;s__hit==0;s__init_buf___0==1;blastFlag==3;tmp___2==0;cb==-1;s__state==4416;s__wbio==0;s__ctx__stats__sess_connect_good==0;s__ctx__stats__sess_connect==1;s__s3__tmp__new_compression==0;tmp___3==1;s__s3__tmp__reuse_message==-1;tmp___5==1;tmp___0==0;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__info_callback==-1;s__bbio==1;s__version==66048;s__init_num==0;skip==0;s__info_callback==0;s__in_handshake==1;tmp==0;s__s3__tmp__new_cipher__algorithms==256; condition-false [!(s__state == 4368)] 139 139 s__s3__tmp__cert_req==0;tmp___0==0;tmp___4==1;s__init_num==0;blastFlag==3;s__type==4096;s__shutdown==0;s__ctx__stats__sess_hit==0;s__state==4416;cb==-1;s__init_buf___0==1;s__server==0;state==4416;s__s3__tmp__new_compression__id==0;tmp___1==12288;s__ctx__stats__sess_connect_good==0;tmp___2==0;tmp___7==0;s__in_handshake==1;ret==1;s__s3__tmp__new_compression==0;s__s3__tmp__new_cipher__algorithms==256;tmp___3==1;initial_state==12292;s__ctx__stats__sess_connect==1;s__bbio==1;tmp___6==1;__cil_tmp55==768;tmp___5==1;s__wbio==0;s__s3__tmp__new_cipher==0;s__hit==0;skip==0;s__info_callback==0;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__reuse_message==-1;tmp==0;s__ctx__info_callback==-1;tmp___8==0;buf==1;s__debug==0;tmp___9==0;s__version==66048;s__new_session==1; condition-false [!(s__state == 4369)] 143 143 cb==-1;tmp___0==0;s__wbio==0;buf==1;blastFlag==3;tmp___1==12288;s__s3__tmp__cert_req==0;s__init_buf___0==1;s__s3__tmp__new_compression==0;s__version==66048;s__type==4096;tmp___8==0;s__s3__tmp__new_cipher==0;s__hit==0;s__state==4416;s__bbio==1;state==4416;skip==0;s__ctx__stats__sess_connect_good==0;s__s3__tmp__new_cipher__algorithms==256;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_connect==1;tmp___5==1;s__new_session==1;__cil_tmp55==768;tmp___7==0;s__in_handshake==1;ret==1;tmp___2==0;s__s3__tmp__new_compression__id==0;initial_state==12292;s__s3__tmp__reuse_message==-1;tmp___4==1;s__info_callback==0;s__server==0;s__init_num==0;s__debug==0;s__ctx__info_callback==-1;tmp___6==1;tmp___9==0;s__shutdown==0;tmp___3==1;s__ctx__stats__sess_hit==0;tmp==0; condition-false [!(s__state == 4384)] 147 147 s__ctx__stats__sess_hit==0;tmp___2==0;s__server==0;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect_good==0;tmp___4==1;s__in_handshake==1;cb==-1;buf==1;tmp___5==1;s__new_session==1;s__type==4096;s__debug==0;s__state==4416;s__info_callback==0;__cil_tmp55==768;tmp___3==1;tmp==0;tmp___9==0;s__init_buf___0==1;tmp___1==12288;s__s3__tmp__new_compression__id==0;s__s3__tmp__new_cipher__algorithms==256;s__ctx__stats__sess_connect==1;tmp___0==0;s__wbio==0;s__shutdown==0;state==4416;skip==0;initial_state==12292;tmp___6==1;s__s3__tmp__reuse_message==-1;s__version==66048;s__s3__tmp__new_compression==0;s__ctx__info_callback==-1;s__init_num==0;ret==1;s__s3__tmp__new_cipher==0;blastFlag==3;s__hit==0;s__bbio==1;tmp___8==0;tmp___7==0;s__ctx__stats__sess_connect_renegotiate==1; condition-false [!(s__state == 4385)] 151 151 initial_state==12292;state==4416;s__s3__tmp__reuse_message==-1;tmp___9==0;s__s3__tmp__new_compression==0;cb==-1;s__ctx__stats__sess_hit==0;s__init_num==0;s__server==0;s__s3__tmp__new_cipher__algorithms==256;ret==1;tmp___4==1;tmp___5==1;s__shutdown==0;buf==1;s__ctx__info_callback==-1;s__hit==0;__cil_tmp55==768;s__new_session==1;s__wbio==0;tmp___3==1;tmp___8==0;s__bbio==1;s__ctx__stats__sess_connect_good==0;s__s3__tmp__cert_req==0;tmp___7==0;blastFlag==3;s__type==4096;skip==0;tmp___1==12288;s__s3__tmp__new_cipher==0;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_connect==1;s__info_callback==0;s__state==4416;tmp==0;tmp___6==1;s__init_buf___0==1;tmp___2==0;tmp___0==0;s__version==66048;s__in_handshake==1;s__debug==0; condition-false [!(s__state == 4400)] 155 155 s__s3__tmp__new_cipher==0;__cil_tmp55==768;s__type==4096;s__ctx__stats__sess_hit==0;s__info_callback==0;tmp==0;tmp___3==1;tmp___9==0;ret==1;s__server==0;s__wbio==0;s__debug==0;initial_state==12292;s__s3__tmp__new_compression__id==0;tmp___5==1;s__in_handshake==1;s__ctx__stats__sess_connect==1;s__s3__tmp__new_compression==0;cb==-1;s__ctx__info_callback==-1;tmp___6==1;s__s3__tmp__new_cipher__algorithms==256;s__init_num==0;s__s3__tmp__reuse_message==-1;tmp___8==0;blastFlag==3;s__bbio==1;tmp___2==0;s__hit==0;s__shutdown==0;skip==0;state==4416;tmp___0==0;tmp___7==0;s__new_session==1;s__ctx__stats__sess_connect_renegotiate==1;tmp___4==1;s__init_buf___0==1;s__version==66048;s__state==4416;tmp___1==12288;s__ctx__stats__sess_connect_good==0;buf==1;s__s3__tmp__cert_req==0; condition-false [!(s__state == 4401)] 159 159 tmp___7==0;s__s3__tmp__new_compression==0;initial_state==12292;tmp___8==0;s__ctx__stats__sess_connect==1;s__info_callback==0;s__s3__tmp__cert_req==0;tmp___1==12288;s__type==4096;s__state==4416;s__server==0;cb==-1;s__ctx__stats__sess_connect_renegotiate==1;tmp___0==0;buf==1;skip==0;tmp___9==0;s__bbio==1;s__hit==0;s__version==66048;s__ctx__info_callback==-1;tmp___2==0;s__s3__tmp__reuse_message==-1;tmp___5==1;tmp___6==1;s__ctx__stats__sess_hit==0;s__debug==0;s__shutdown==0;s__s3__tmp__new_compression__id==0;s__in_handshake==1;state==4416;s__init_buf___0==1;s__init_num==0;s__ctx__stats__sess_connect_good==0;blastFlag==3;tmp==0;s__s3__tmp__new_cipher==0;__cil_tmp55==768;s__s3__tmp__new_cipher__algorithms==256;s__wbio==0;s__new_session==1;ret==1;tmp___4==1;tmp___3==1; [s__state == 4416] 163 163 s__ctx__stats__sess_hit==0;s__new_session==1;tmp___8==0;tmp___6==1;s__shutdown==0;tmp___5==1;s__ctx__info_callback==-1;s__type==4096;s__s3__tmp__new_cipher__algorithms==256;s__version==66048;s__server==0;tmp___9==0;tmp___2==0;s__s3__tmp__new_compression__id==0;s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect_good==0;s__ctx__stats__sess_connect==1;blastFlag==3;tmp___0==0;__cil_tmp55==768;s__wbio==0;s__bbio==1;s__info_callback==0;tmp___7==0;s__in_handshake==1;s__s3__tmp__new_cipher==0;state==4416;s__debug==0;tmp___4==1;s__init_buf___0==1;s__init_num==0;s__state==4416;ret==1;tmp___1==12288;initial_state==12292;skip==0;s__s3__tmp__reuse_message==-1;tmp==0;s__s3__tmp__cert_req==0;s__hit==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___3==1;buf==1;cb==-1; ret = __VERIFIER_nondet_int() 395 395 [blastFlag == 3] 397 397 blastFlag = 4 399 399 tmp___7==0;buf==1;s__hit==0;tmp___8==0;ret==1;tmp___1==12288;skip==0;tmp___9==0;s__debug==0;tmp___5==1;s__ctx__stats__sess_connect==1;s__init_num==0;s__new_session==1;s__info_callback==0;s__ctx__stats__sess_connect_good==0;tmp___0==0;s__init_buf___0==1;s__type==4096;tmp___6==1;s__bbio==1;s__version==66048;s__shutdown==0;state==4416;s__s3__tmp__new_compression==0;s__ctx__info_callback==-1;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_connect_renegotiate==1;s__wbio==0;initial_state==12292;cb==-1;s__server==0;tmp==0;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_hit==0;s__s3__tmp__new_cipher__algorithms==256;tmp___2==0;s__s3__tmp__cert_req==0;blastFlag==4;tmp___3==1;__cil_tmp55==768;s__in_handshake==1;s__state==4416;s__s3__tmp__reuse_message==-1;tmp___4==1; condition-false [!(ret <= 0)] 402 402 s__state = 4432 406 406 s__init_num = 0 408 408 s__hit==0;tmp___4==1;s__s3__tmp__cert_req==0;s__bbio==1;s__ctx__info_callback==-1;s__ctx__stats__sess_connect_renegotiate==1;blastFlag==4;s__state==4432;s__ctx__stats__sess_connect_good==0;s__shutdown==0;s__s3__tmp__new_cipher__algorithms==256;buf==1;tmp___9==0;s__wbio==0;ret==1;tmp___2==0;tmp___1==12288;__cil_tmp55==768;s__init_buf___0==1;tmp___3==1;s__new_session==1;s__server==0;initial_state==12292;tmp___7==0;s__type==4096;tmp___8==0;tmp___6==1;cb==-1;s__init_num==0;s__s3__tmp__reuse_message==-1;s__version==66048;skip==0;tmp==0;s__ctx__stats__sess_hit==0;s__debug==0;s__in_handshake==1;s__s3__tmp__new_cipher==0;tmp___5==1;s__s3__tmp__new_compression__id==0;s__s3__tmp__new_compression==0;tmp___0==0;state==4416;s__info_callback==0;s__ctx__stats__sess_connect==1; condition-false [!(! tmp___6)] 410 410 tmp___0==0;tmp___5==1;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect==1;s__init_buf___0==1;s__ctx__stats__sess_connect_good==0;s__server==0;s__ctx__info_callback==-1;s__s3__tmp__new_compression__id==0;s__s3__tmp__new_cipher==0;s__s3__tmp__new_cipher__algorithms==256;initial_state==12292;s__init_num==0;state==4416;__cil_tmp55==768;s__debug==0;skip==0;tmp___3==1;tmp==0;tmp___8==0;s__wbio==0;tmp___2==0;tmp___1==12288;tmp___9==0;s__ctx__stats__sess_hit==0;s__state==4432;s__new_session==1;s__s3__tmp__reuse_message==-1;s__info_callback==0;tmp___7==0;cb==-1;s__in_handshake==1;s__version==66048;buf==1;s__shutdown==0;s__hit==0;blastFlag==4;ret==1;tmp___4==1;s__ctx__stats__sess_connect_renegotiate==1;s__bbio==1;s__s3__tmp__new_compression==0;tmp___6==1;s__type==4096; condition-false [!(! s__s3__tmp__reuse_message)] 710 710 s__state==4432;s__debug==0;tmp___8==0;cb==-1;s__info_callback==0;tmp___0==0;s__init_num==0;s__init_buf___0==1;buf==1;tmp___3==1;s__wbio==0;tmp___7==0;s__s3__tmp__reuse_message==-1;tmp___6==1;s__shutdown==0;state==4416;s__s3__tmp__cert_req==0;tmp___5==1;skip==0;s__type==4096;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__new_compression==0;s__new_session==1;tmp___4==1;s__s3__tmp__new_cipher==0;tmp___9==0;s__ctx__stats__sess_connect_good==0;blastFlag==4;tmp___2==0;initial_state==12292;s__s3__tmp__new_compression__id==0;__cil_tmp55==768;ret==1;s__server==0;tmp==0;s__hit==0;tmp___1==12288;s__version==66048;s__ctx__info_callback==-1;s__in_handshake==1;s__bbio==1;s__ctx__stats__sess_hit==0;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_connect==1; skip = 0 737 737 s__shutdown==0;s__bbio==1;s__ctx__info_callback==-1;skip==0;s__type==4096;s__ctx__stats__sess_hit==0;tmp___9==0;tmp___6==1;tmp___3==1;tmp==0;s__ctx__stats__sess_connect==1;s__server==0;s__init_buf___0==1;blastFlag==4;__cil_tmp55==768;tmp___2==0;s__s3__tmp__cert_req==0;s__version==66048;tmp___8==0;tmp___4==1;ret==1;s__s3__tmp__new_cipher__algorithms==256;s__state==4432;cb==-1;s__wbio==0;s__s3__tmp__new_compression==0;s__new_session==1;s__hit==0;state==4416;s__ctx__stats__sess_connect_good==0;tmp___7==0;buf==1;tmp___1==12288;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___0==0;s__debug==0;s__info_callback==0;s__in_handshake==1;s__s3__tmp__reuse_message==-1;tmp___5==1;s__s3__tmp__new_cipher==0;s__init_num==0;initial_state==12292; [1] 114 114 tmp___2==0;tmp___9==0;s__init_buf___0==1;s__ctx__stats__sess_connect==1;tmp___3==1;skip==0;tmp___4==1;tmp___7==0;__cil_tmp55==768;tmp___5==1;s__wbio==0;s__s3__tmp__new_compression__id==0;initial_state==12292;s__ctx__info_callback==-1;tmp==0;blastFlag==4;cb==-1;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_hit==0;tmp___0==0;tmp___8==0;s__ctx__stats__sess_connect_renegotiate==1;state==4416;s__in_handshake==1;s__s3__tmp__new_compression==0;s__bbio==1;s__shutdown==0;s__init_num==0;s__version==66048;buf==1;s__s3__tmp__cert_req==0;tmp___6==1;s__debug==0;s__info_callback==0;s__s3__tmp__new_cipher__algorithms==256;s__state==4432;ret==1;s__hit==0;tmp___1==12288;s__new_session==1;s__s3__tmp__reuse_message==-1;s__type==4096;s__ctx__stats__sess_connect_good==0;s__server==0; state = s__state 117 117 s__state==4432;tmp___1==12288;__cil_tmp55==768;s__shutdown==0;s__in_handshake==1;tmp___8==0;s__s3__tmp__cert_req==0;s__s3__tmp__new_cipher==0;state==4432;s__s3__tmp__reuse_message==-1;s__hit==0;initial_state==12292;s__wbio==0;s__s3__tmp__new_cipher__algorithms==256;tmp___5==1;tmp___6==1;cb==-1;s__type==4096;s__new_session==1;buf==1;s__bbio==1;tmp___2==0;tmp==0;blastFlag==4;tmp___0==0;s__ctx__info_callback==-1;s__server==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___9==0;tmp___4==1;s__ctx__stats__sess_connect==1;s__debug==0;tmp___7==0;ret==1;s__init_buf___0==1;tmp___3==1;s__version==66048;s__ctx__stats__sess_hit==0;skip==0;s__s3__tmp__new_compression__id==0;s__info_callback==0;s__init_num==0;s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect_good==0; condition-false [!(s__state == 12292)] 119 119 s__bbio==1;s__s3__tmp__new_compression__id==0;s__s3__tmp__cert_req==0;s__init_buf___0==1;tmp___2==0;buf==1;cb==-1;s__s3__tmp__new_compression==0;s__state==4432;tmp___5==1;s__in_handshake==1;s__version==66048;s__init_num==0;skip==0;s__new_session==1;s__hit==0;state==4432;tmp___6==1;s__info_callback==0;tmp___3==1;blastFlag==4;tmp___0==0;ret==1;s__ctx__stats__sess_hit==0;initial_state==12292;s__s3__tmp__new_cipher==0;tmp___4==1;s__ctx__stats__sess_connect==1;s__ctx__info_callback==-1;s__wbio==0;__cil_tmp55==768;s__shutdown==0;tmp___7==0;tmp___9==0;s__ctx__stats__sess_connect_good==0;tmp___8==0;tmp==0;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_connect_renegotiate==1;s__debug==0;s__type==4096;tmp___1==12288;s__server==0; condition-false [!(s__state == 16384)] 123 123 s__new_session==1;s__ctx__stats__sess_connect_good==0;initial_state==12292;s__wbio==0;s__ctx__stats__sess_connect_renegotiate==1;s__hit==0;tmp___0==0;tmp___6==1;s__init_num==0;tmp___8==0;s__init_buf___0==1;s__state==4432;buf==1;s__s3__tmp__reuse_message==-1;s__s3__tmp__new_cipher==0;s__debug==0;tmp==0;tmp___5==1;s__server==0;s__version==66048;blastFlag==4;s__s3__tmp__new_compression__id==0;tmp___4==1;state==4432;s__shutdown==0;cb==-1;s__in_handshake==1;tmp___9==0;tmp___7==0;ret==1;s__info_callback==0;s__ctx__stats__sess_hit==0;__cil_tmp55==768;tmp___3==1;s__bbio==1;s__ctx__info_callback==-1;s__s3__tmp__cert_req==0;s__s3__tmp__new_cipher__algorithms==256;tmp___1==12288;s__s3__tmp__new_compression==0;skip==0;s__type==4096;tmp___2==0;s__ctx__stats__sess_connect==1; condition-false [!(s__state == 4096)] 127 127 blastFlag==4;initial_state==12292;s__s3__tmp__new_compression__id==0;skip==0;__cil_tmp55==768;tmp___3==1;s__shutdown==0;s__s3__tmp__reuse_message==-1;tmp___6==1;tmp___8==0;s__new_session==1;tmp___1==12288;s__ctx__stats__sess_connect==1;s__state==4432;state==4432;s__debug==0;ret==1;s__bbio==1;s__in_handshake==1;buf==1;s__ctx__stats__sess_connect_good==0;s__init_buf___0==1;s__ctx__stats__sess_hit==0;s__wbio==0;tmp___0==0;s__info_callback==0;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__new_cipher==0;s__s3__tmp__cert_req==0;s__init_num==0;s__server==0;tmp==0;s__ctx__info_callback==-1;s__type==4096;s__ctx__stats__sess_connect_renegotiate==1;tmp___9==0;s__s3__tmp__new_compression==0;cb==-1;s__version==66048;tmp___2==0;s__hit==0;tmp___4==1;tmp___5==1;tmp___7==0; condition-false [!(s__state == 20480)] 131 131 s__init_buf___0==1;s__ctx__stats__sess_connect_good==0;s__debug==0;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect_renegotiate==1;skip==0;s__version==66048;blastFlag==4;s__state==4432;initial_state==12292;ret==1;tmp___1==12288;tmp___3==1;s__s3__tmp__reuse_message==-1;s__s3__tmp__new_compression==0;s__server==0;s__wbio==0;s__init_num==0;s__in_handshake==1;tmp___9==0;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_hit==0;s__info_callback==0;tmp___5==1;cb==-1;tmp___2==0;tmp___0==0;buf==1;s__new_session==1;__cil_tmp55==768;tmp==0;s__bbio==1;s__s3__tmp__new_cipher==0;state==4432;s__type==4096;s__ctx__info_callback==-1;s__shutdown==0;tmp___4==1;s__hit==0;tmp___8==0;tmp___7==0;tmp___6==1;s__ctx__stats__sess_connect==1; condition-false [!(s__state == 4099)] 135 135 s__ctx__stats__sess_connect==1;tmp___5==1;s__server==0;s__wbio==0;s__bbio==1;tmp___2==0;s__in_handshake==1;skip==0;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_connect_renegotiate==1;s__state==4432;__cil_tmp55==768;buf==1;s__init_buf___0==1;s__type==4096;tmp___3==1;s__ctx__stats__sess_hit==0;s__ctx__stats__sess_connect_good==0;state==4432;s__ctx__info_callback==-1;s__version==66048;s__s3__tmp__new_compression__id==0;tmp___7==0;s__shutdown==0;tmp==0;s__s3__tmp__new_cipher__algorithms==256;tmp___1==12288;s__s3__tmp__new_compression==0;tmp___9==0;initial_state==12292;s__new_session==1;s__init_num==0;s__s3__tmp__cert_req==0;s__s3__tmp__new_cipher==0;s__debug==0;tmp___8==0;tmp___6==1;tmp___0==0;ret==1;tmp___4==1;s__hit==0;s__info_callback==0;blastFlag==4;cb==-1; condition-false [!(s__state == 4368)] 139 139 s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect_renegotiate==1;ret==1;tmp___9==0;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_connect==1;s__ctx__stats__sess_hit==0;state==4432;blastFlag==4;tmp___1==12288;tmp___5==1;tmp___8==0;tmp___7==0;s__bbio==1;tmp___6==1;s__wbio==0;s__ctx__info_callback==-1;s__new_session==1;s__info_callback==0;s__init_num==0;s__s3__tmp__cert_req==0;cb==-1;s__version==66048;s__ctx__stats__sess_connect_good==0;s__type==4096;s__debug==0;s__server==0;tmp==0;tmp___3==1;tmp___4==1;s__in_handshake==1;s__s3__tmp__new_compression__id==0;tmp___0==0;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__new_cipher==0;s__shutdown==0;initial_state==12292;buf==1;tmp___2==0;s__hit==0;s__init_buf___0==1;skip==0;__cil_tmp55==768;s__state==4432; condition-false [!(s__state == 4369)] 143 143 tmp___3==1;s__s3__tmp__new_compression__id==0;s__new_session==1;s__s3__tmp__reuse_message==-1;s__s3__tmp__cert_req==0;s__init_num==0;s__server==0;tmp___8==0;tmp___1==12288;s__ctx__stats__sess_hit==0;__cil_tmp55==768;skip==0;s__ctx__stats__sess_connect==1;tmp___7==0;ret==1;s__info_callback==0;tmp___2==0;s__init_buf___0==1;s__in_handshake==1;s__wbio==0;initial_state==12292;tmp==0;state==4432;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_cipher__algorithms==256;s__ctx__stats__sess_connect_good==0;cb==-1;s__ctx__info_callback==-1;tmp___0==0;tmp___4==1;buf==1;s__hit==0;blastFlag==4;s__s3__tmp__new_compression==0;tmp___9==0;s__version==66048;tmp___6==1;s__bbio==1;s__type==4096;s__s3__tmp__new_cipher==0;s__state==4432;s__shutdown==0;s__debug==0;tmp___5==1; condition-false [!(s__state == 4384)] 147 147 tmp___6==1;initial_state==12292;tmp___7==0;s__version==66048;buf==1;s__ctx__stats__sess_hit==0;tmp___4==1;s__s3__tmp__new_cipher__algorithms==256;tmp___2==0;s__init_num==0;tmp___9==0;s__debug==0;s__info_callback==0;s__in_handshake==1;__cil_tmp55==768;s__s3__tmp__new_compression__id==0;s__ctx__info_callback==-1;tmp___0==0;tmp___3==1;tmp==0;s__wbio==0;s__new_session==1;s__bbio==1;s__init_buf___0==1;tmp___1==12288;s__type==4096;s__state==4432;cb==-1;blastFlag==4;s__s3__tmp__cert_req==0;s__s3__tmp__new_compression==0;s__s3__tmp__reuse_message==-1;tmp___8==0;state==4432;s__ctx__stats__sess_connect==1;s__server==0;s__s3__tmp__new_cipher==0;tmp___5==1;skip==0;s__ctx__stats__sess_connect_renegotiate==1;s__ctx__stats__sess_connect_good==0;s__shutdown==0;ret==1;s__hit==0; condition-false [!(s__state == 4385)] 151 151 tmp___9==0;s__s3__tmp__new_cipher__algorithms==256;tmp___6==1;buf==1;initial_state==12292;cb==-1;s__version==66048;tmp___7==0;tmp___8==0;skip==0;tmp___2==0;state==4432;__cil_tmp55==768;s__state==4432;s__info_callback==0;tmp___1==12288;s__s3__tmp__new_compression__id==0;tmp___5==1;s__init_buf___0==1;s__shutdown==0;s__server==0;s__debug==0;tmp___4==1;s__ctx__stats__sess_connect==1;s__init_num==0;s__type==4096;s__ctx__stats__sess_connect_good==0;blastFlag==4;tmp==0;s__ctx__stats__sess_hit==0;s__hit==0;s__s3__tmp__new_compression==0;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_connect_renegotiate==1;s__bbio==1;tmp___0==0;tmp___3==1;s__in_handshake==1;s__new_session==1;s__s3__tmp__reuse_message==-1;s__wbio==0;s__s3__tmp__cert_req==0;ret==1;s__ctx__info_callback==-1; condition-false [!(s__state == 4400)] 155 155 tmp___2==0;s__s3__tmp__new_cipher==0;tmp___4==1;s__wbio==0;s__in_handshake==1;s__state==4432;blastFlag==4;s__ctx__stats__sess_hit==0;s__ctx__stats__sess_connect==1;s__init_num==0;s__s3__tmp__new_compression__id==0;s__debug==0;s__server==0;tmp___5==1;s__new_session==1;ret==1;s__init_buf___0==1;s__version==66048;s__bbio==1;s__type==4096;tmp___6==1;s__hit==0;s__s3__tmp__new_cipher__algorithms==256;__cil_tmp55==768;tmp___1==12288;s__ctx__stats__sess_connect_renegotiate==1;skip==0;s__s3__tmp__new_compression==0;s__s3__tmp__cert_req==0;initial_state==12292;s__ctx__info_callback==-1;tmp___7==0;tmp___0==0;cb==-1;tmp___3==1;tmp___8==0;tmp==0;s__shutdown==0;tmp___9==0;state==4432;s__ctx__stats__sess_connect_good==0;buf==1;s__info_callback==0;s__s3__tmp__reuse_message==-1; condition-false [!(s__state == 4401)] 159 159 s__s3__tmp__new_cipher==0;tmp___9==0;tmp___2==0;cb==-1;s__ctx__stats__sess_connect==1;tmp___0==0;s__server==0;blastFlag==4;skip==0;s__wbio==0;s__init_buf___0==1;s__bbio==1;s__debug==0;s__new_session==1;s__ctx__stats__sess_connect_good==0;ret==1;s__s3__tmp__new_compression__id==0;s__ctx__stats__sess_connect_renegotiate==1;__cil_tmp55==768;tmp___6==1;initial_state==12292;tmp___1==12288;s__info_callback==0;s__s3__tmp__new_cipher__algorithms==256;tmp___3==1;tmp___5==1;s__type==4096;tmp___8==0;s__hit==0;s__init_num==0;buf==1;s__shutdown==0;s__ctx__stats__sess_hit==0;s__s3__tmp__new_compression==0;s__s3__tmp__reuse_message==-1;tmp___7==0;tmp==0;s__state==4432;s__ctx__info_callback==-1;s__s3__tmp__cert_req==0;state==4432;s__version==66048;s__in_handshake==1;tmp___4==1; condition-false [!(s__state == 4416)] 163 163 tmp___4==1;tmp___5==1;s__type==4096;tmp___2==0;s__new_session==1;tmp___1==12288;s__ctx__stats__sess_hit==0;tmp___7==0;s__state==4432;tmp___9==0;s__info_callback==0;s__server==0;buf==1;s__s3__tmp__reuse_message==-1;initial_state==12292;s__ctx__stats__sess_connect==1;ret==1;tmp___0==0;s__init_num==0;s__s3__tmp__new_cipher==0;__cil_tmp55==768;s__in_handshake==1;s__ctx__stats__sess_connect_renegotiate==1;s__s3__tmp__new_compression__id==0;s__version==66048;s__wbio==0;blastFlag==4;cb==-1;s__init_buf___0==1;skip==0;state==4432;s__debug==0;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__cert_req==0;s__ctx__info_callback==-1;tmp___8==0;tmp___3==1;s__bbio==1;tmp==0;tmp___6==1;s__hit==0;s__s3__tmp__new_compression==0;s__ctx__stats__sess_connect_good==0;s__shutdown==0; condition-false [!(s__state == 4417)] 167 167 s__version==66048;tmp___4==1;tmp___5==1;tmp___2==0;s__s3__tmp__new_cipher==0;ret==1;__cil_tmp55==768;s__type==4096;s__state==4432;s__s3__tmp__new_compression==0;tmp___9==0;s__debug==0;s__ctx__stats__sess_connect_renegotiate==1;tmp___0==0;s__hit==0;s__init_num==0;buf==1;tmp==0;skip==0;s__wbio==0;cb==-1;blastFlag==4;s__server==0;s__in_handshake==1;tmp___3==1;s__ctx__stats__sess_connect_good==0;tmp___7==0;s__ctx__stats__sess_connect==1;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__cert_req==0;initial_state==12292;tmp___6==1;tmp___1==12288;tmp___8==0;s__bbio==1;s__init_buf___0==1;s__new_session==1;s__s3__tmp__reuse_message==-1;s__ctx__stats__sess_hit==0;s__s3__tmp__new_compression__id==0;s__info_callback==0;s__shutdown==0;s__ctx__info_callback==-1;state==4432; [s__state == 4432] 171 171 tmp___4==1;s__state==4432;__cil_tmp55==768;s__info_callback==0;s__in_handshake==1;initial_state==12292;s__ctx__stats__sess_connect_renegotiate==1;tmp___3==1;s__debug==0;s__init_buf___0==1;tmp___0==0;skip==0;s__s3__tmp__new_compression==0;tmp==0;s__shutdown==0;s__ctx__stats__sess_hit==0;tmp___5==1;s__ctx__stats__sess_connect==1;tmp___2==0;s__type==4096;tmp___9==0;s__init_num==0;blastFlag==4;tmp___7==0;s__s3__tmp__reuse_message==-1;s__server==0;s__new_session==1;s__s3__tmp__cert_req==0;tmp___1==12288;s__hit==0;state==4432;cb==-1;s__version==66048;s__ctx__stats__sess_connect_good==0;s__wbio==0;tmp___6==1;s__s3__tmp__new_cipher__algorithms==256;tmp___8==0;s__ctx__info_callback==-1;buf==1;ret==1;s__s3__tmp__new_compression__id==0;s__bbio==1;s__s3__tmp__new_cipher==0; ret = __VERIFIER_nondet_int() 419 419 [blastFlag == 4] 421 421 s__ctx__stats__sess_connect_good==0;tmp___2==0;state==4432;cb==-1;s__in_handshake==1;__cil_tmp55==768;s__hit==0;s__state==4432;s__ctx__stats__sess_connect_renegotiate==1;tmp___6==1;s__s3__tmp__new_cipher==0;s__ctx__stats__sess_hit==0;tmp___0==0;s__shutdown==0;tmp___4==1;s__s3__tmp__new_compression==0;s__init_num==0;blastFlag==4;tmp___1==12288;tmp___7==0;s__new_session==1;s__s3__tmp__reuse_message==-1;s__info_callback==0;s__bbio==1;tmp___3==1;ret==0;tmp___8==0;s__version==66048;tmp___9==0;s__ctx__stats__sess_connect==1;s__ctx__info_callback==-1;buf==1;skip==0;s__s3__tmp__new_cipher__algorithms==256;s__s3__tmp__cert_req==0;s__type==4096;tmp==0;s__debug==0;s__s3__tmp__new_compression__id==0;s__init_buf___0==1;s__wbio==0;tmp___5==1;s__server==0;initial_state==12292; __VERIFIER_error() 751 751 skip==0;s__s3__tmp__cert_req==0;s__ctx__stats__sess_connect==1;s__ctx__stats__sess_connect_renegotiate==1;s__debug==0;s__ctx__info_callback==-1;tmp___0==0;s__info_callback==0;tmp___1==12288;s__server==0;s__s3__tmp__new_compression__id==0;tmp___9==0;tmp___5==1;s__bbio==1;s__ctx__stats__sess_connect_good==0;blastFlag==4;buf==1;s__ctx__stats__sess_hit==0;tmp___3==1;s__s3__tmp__new_cipher__algorithms==256;initial_state==12292;tmp___4==1;tmp___7==0;s__s3__tmp__new_compression==0;tmp==0;s__hit==0;s__s3__tmp__new_cipher==0;cb==-1;s__new_session==1;s__state==4432;s__type==4096;__cil_tmp55==768;s__s3__tmp__reuse_message==-1;s__shutdown==0;tmp___6==1;s__wbio==0;tmp___2==0;s__version==66048;ret==0;s__init_buf___0==1;s__init_num==0;s__in_handshake==1;state==4432;tmp___8==0;