diff --git a/c/ldv-regression/rule57_ebda_blast.yml b/c/ldv-regression/rule57_ebda_blast.yml
index 68b114db2b8..d3b2a3b0254 100644
--- a/c/ldv-regression/rule57_ebda_blast.yml
+++ b/c/ldv-regression/rule57_ebda_blast.yml
@@ -12,7 +12,6 @@ properties:
   - property_file: ../properties/coverage-branches.prp
   - property_file: ../properties/coverage-conditions.prp
   - property_file: ../properties/coverage-statements.prp
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C
diff --git a/c/ldv-regression/test28-1.c b/c/ldv-regression/test28-1.c
index 8e63c90421d..6bfffc0672d 100644
--- a/c/ldv-regression/test28-1.c
+++ b/c/ldv-regression/test28-1.c
@@ -16,6 +16,7 @@ int main()
   struct dummy *pd = n ? &d1 : &d2;
   if (pd == &d2) {
     pd->a = 0;
+    pd->b = __VERIFIER_nondet_int();
   } else {
     pd->b = 0;
   }
diff --git a/c/loops/s3.i b/c/loops/s3.i
index 987fb3d2a4f..7e93ce60312 100644
--- a/c/loops/s3.i
+++ b/c/loops/s3.i
@@ -8,6 +8,7 @@ extern void *malloc(unsigned int sz);
 
 extern int __VERIFIER_nondet_int(void);
 extern unsigned long __VERIFIER_nondet_ulong(void);
+extern  long __VERIFIER_nondet_long(void);
 
 typedef unsigned int size_t;
 typedef long __time_t;
@@ -1067,9 +1068,19 @@ int main(void)
   {
   s = malloc (sizeof (SSL));
   s->s3 = malloc(sizeof(struct ssl3_state_st));
+  s->s3->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  s->s3->tmp.next_state = __VERIFIER_nondet_int();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
   s->ctx = malloc(sizeof(SSL_CTX));
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong();
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->info_callback = (void (*)()) __VERIFIER_nondet_ulong();
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_clnt.blast.01.i.cil-1.c b/c/openssl/s3_clnt.blast.01.i.cil-1.c
index ad427c69890..80be914b03f 100644
--- a/c/openssl/s3_clnt.blast.01.i.cil-1.c
+++ b/c/openssl/s3_clnt.blast.01.i.cil-1.c
@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+	
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+	
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_clnt.blast.01.i.cil-2.c b/c/openssl/s3_clnt.blast.01.i.cil-2.c
index ac779ace65e..0016215d3a3 100644
--- a/c/openssl/s3_clnt.blast.01.i.cil-2.c
+++ b/c/openssl/s3_clnt.blast.01.i.cil-2.c
@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+	
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+	
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_clnt.blast.02.i.cil-1.c b/c/openssl/s3_clnt.blast.02.i.cil-1.c
index 9eaed6afbbd..eed49e1c278 100644
--- a/c/openssl/s3_clnt.blast.02.i.cil-1.c
+++ b/c/openssl/s3_clnt.blast.02.i.cil-1.c
@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+	
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+	
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_clnt.blast.02.i.cil-2.c b/c/openssl/s3_clnt.blast.02.i.cil-2.c
index b732a5948c9..ca4e34639f2 100644
--- a/c/openssl/s3_clnt.blast.02.i.cil-2.c
+++ b/c/openssl/s3_clnt.blast.02.i.cil-2.c
@@ -1074,6 +1074,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+	
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+	
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_clnt.blast.03.i.cil-1.c b/c/openssl/s3_clnt.blast.03.i.cil-1.c
index 41180f9178b..f02cfbbe3e8 100644
--- a/c/openssl/s3_clnt.blast.03.i.cil-1.c
+++ b/c/openssl/s3_clnt.blast.03.i.cil-1.c
@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+	
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+	
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_clnt.blast.03.i.cil-2.c b/c/openssl/s3_clnt.blast.03.i.cil-2.c
index 2bebbd4536d..86a645ad266 100644
--- a/c/openssl/s3_clnt.blast.03.i.cil-2.c
+++ b/c/openssl/s3_clnt.blast.03.i.cil-2.c
@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+	
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+	
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_clnt.blast.04.i.cil-1.c b/c/openssl/s3_clnt.blast.04.i.cil-1.c
index ac0caa60780..7f3b44c3466 100644
--- a/c/openssl/s3_clnt.blast.04.i.cil-1.c
+++ b/c/openssl/s3_clnt.blast.04.i.cil-1.c
@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+	
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+	
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_clnt.blast.04.i.cil-2.c b/c/openssl/s3_clnt.blast.04.i.cil-2.c
index 474e5182b85..606857f58c3 100644
--- a/c/openssl/s3_clnt.blast.04.i.cil-2.c
+++ b/c/openssl/s3_clnt.blast.04.i.cil-2.c
@@ -1073,6 +1073,18 @@ int main(void)
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 12292;
   s->version = __VERIFIER_nondet_int();
+	
+	s->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  (s->ctx)->info_callback = (void (*)()) __VERIFIER_nondet_ulong(); 
+  s->init_buf = (BUF_MEM *)__VERIFIER_nondet_ulong();
+  s->bbio = (BIO *) __VERIFIER_nondet_ulong();
+  s->wbio = (BIO *) __VERIFIER_nondet_ulong();
+  (s->s3)->flags = __VERIFIER_nondet_long();
+  (s->s3)->tmp.cert_req = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.next_state = __VERIFIER_nondet_int();
+	
   ssl3_connect(s);
   }
   return (0);
diff --git a/c/openssl/s3_srvr.blast.01.i.cil-1.c b/c/openssl/s3_srvr.blast.01.i.cil-1.c
index 6205fcd7a64..fccbcebd902 100644
--- a/c/openssl/s3_srvr.blast.01.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.01.i.cil-1.c
@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+	s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.01.i.cil-2.c b/c/openssl/s3_srvr.blast.01.i.cil-2.c
index 05a6ac77c4d..1b5c7ac8dd0 100644
--- a/c/openssl/s3_srvr.blast.01.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.01.i.cil-2.c
@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.02.i.cil-1.c b/c/openssl/s3_srvr.blast.02.i.cil-1.c
index 9f7db7cb749..ca8b2c1deea 100644
--- a/c/openssl/s3_srvr.blast.02.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.02.i.cil-1.c
@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.02.i.cil-2.c b/c/openssl/s3_srvr.blast.02.i.cil-2.c
index ee42bafb9e5..029680759c5 100644
--- a/c/openssl/s3_srvr.blast.02.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.02.i.cil-2.c
@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.03.i.cil.c b/c/openssl/s3_srvr.blast.03.i.cil.c
index 8a03c8b625a..93c02db1a98 100644
--- a/c/openssl/s3_srvr.blast.03.i.cil.c
+++ b/c/openssl/s3_srvr.blast.03.i.cil.c
@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.04.i.cil.c b/c/openssl/s3_srvr.blast.04.i.cil.c
index f41a2bfc1c7..73004bd33fe 100644
--- a/c/openssl/s3_srvr.blast.04.i.cil.c
+++ b/c/openssl/s3_srvr.blast.04.i.cil.c
@@ -1074,6 +1074,25 @@ int main(void)
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
   s->state = 8464;
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.06.i.cil-1.c b/c/openssl/s3_srvr.blast.06.i.cil-1.c
index 7b1551d6086..3ec8c46c472 100644
--- a/c/openssl/s3_srvr.blast.06.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.06.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+	
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.06.i.cil-2.c b/c/openssl/s3_srvr.blast.06.i.cil-2.c
index 61ffc9d18a7..5ca16f6a8bd 100644
--- a/c/openssl/s3_srvr.blast.06.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.06.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.07.i.cil-1.c b/c/openssl/s3_srvr.blast.07.i.cil-1.c
index ef4450232f0..31f29023648 100644
--- a/c/openssl/s3_srvr.blast.07.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.07.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.07.i.cil-2.c b/c/openssl/s3_srvr.blast.07.i.cil-2.c
index 1be347a7dac..b68ecf27875 100644
--- a/c/openssl/s3_srvr.blast.07.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.07.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.08.i.cil-1.c b/c/openssl/s3_srvr.blast.08.i.cil-1.c
index 250d15dbd3b..59f76134cdf 100644
--- a/c/openssl/s3_srvr.blast.08.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.08.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.08.i.cil-2.c b/c/openssl/s3_srvr.blast.08.i.cil-2.c
index 7b4a845a823..aa2d471cec7 100644
--- a/c/openssl/s3_srvr.blast.08.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.08.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.09.i.cil-1.c b/c/openssl/s3_srvr.blast.09.i.cil-1.c
index bdc7ab23a58..8ef50f80929 100644
--- a/c/openssl/s3_srvr.blast.09.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.09.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.09.i.cil-2.c b/c/openssl/s3_srvr.blast.09.i.cil-2.c
index 9865d474fe9..cb5c9e12231 100644
--- a/c/openssl/s3_srvr.blast.09.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.09.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.10.i.cil-1.c b/c/openssl/s3_srvr.blast.10.i.cil-1.c
index 55be06f35c4..ae16cbe19f0 100644
--- a/c/openssl/s3_srvr.blast.10.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.10.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.10.i.cil-2.c b/c/openssl/s3_srvr.blast.10.i.cil-2.c
index 77a4d9985cc..5455b45b8b9 100644
--- a/c/openssl/s3_srvr.blast.10.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.10.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.11.i.cil-1.c b/c/openssl/s3_srvr.blast.11.i.cil-1.c
index 1c8850cdc08..2bae32356dd 100644
--- a/c/openssl/s3_srvr.blast.11.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.11.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.11.i.cil-2.c b/c/openssl/s3_srvr.blast.11.i.cil-2.c
index a8925bcf6aa..cb1dac9fb7b 100644
--- a/c/openssl/s3_srvr.blast.11.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.11.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.12.i.cil-1.c b/c/openssl/s3_srvr.blast.12.i.cil-1.c
index 9216a83fe11..1f89cada5c5 100644
--- a/c/openssl/s3_srvr.blast.12.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.12.i.cil-1.c
@@ -1073,6 +1073,26 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.12.i.cil-2.c b/c/openssl/s3_srvr.blast.12.i.cil-2.c
index 5dca6f8c9d8..b8a2368ef0c 100644
--- a/c/openssl/s3_srvr.blast.12.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.12.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.13.i.cil-1.c b/c/openssl/s3_srvr.blast.13.i.cil-1.c
index 73d2f60e92d..00eabfd0a76 100644
--- a/c/openssl/s3_srvr.blast.13.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.13.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.13.i.cil-2.c b/c/openssl/s3_srvr.blast.13.i.cil-2.c
index b8b792cf541..72ef6a1c426 100644
--- a/c/openssl/s3_srvr.blast.13.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.13.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+	s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.14.i.cil-1.c b/c/openssl/s3_srvr.blast.14.i.cil-1.c
index 093305d66a1..31afc58a612 100644
--- a/c/openssl/s3_srvr.blast.14.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.14.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.14.i.cil-2.c b/c/openssl/s3_srvr.blast.14.i.cil-2.c
index 14fc53fa040..0a85ee5159d 100644
--- a/c/openssl/s3_srvr.blast.14.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.14.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.15.i.cil-1.c b/c/openssl/s3_srvr.blast.15.i.cil-1.c
index c3dd4f3cb33..a0ef4c9cf2e 100644
--- a/c/openssl/s3_srvr.blast.15.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.15.i.cil-1.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.15.i.cil-2.c b/c/openssl/s3_srvr.blast.15.i.cil-2.c
index 95612f3f2b3..283365651b1 100644
--- a/c/openssl/s3_srvr.blast.15.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.15.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.16.i.cil-1.c b/c/openssl/s3_srvr.blast.16.i.cil-1.c
index 943a4b4837c..7d226425803 100644
--- a/c/openssl/s3_srvr.blast.16.i.cil-1.c
+++ b/c/openssl/s3_srvr.blast.16.i.cil-1.c
@@ -1073,6 +1073,26 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
+
   tmp = ssl3_accept(s);
   }
   return (tmp);
diff --git a/c/openssl/s3_srvr.blast.16.i.cil-2.c b/c/openssl/s3_srvr.blast.16.i.cil-2.c
index a81c7b8cb01..ecc02fbcd1c 100644
--- a/c/openssl/s3_srvr.blast.16.i.cil-2.c
+++ b/c/openssl/s3_srvr.blast.16.i.cil-2.c
@@ -1073,6 +1073,25 @@ int main(void)
   s->s3 = malloc(sizeof(struct ssl3_state_st));
   s->ctx = malloc(sizeof(SSL_CTX));
   s->session = malloc(sizeof(SSL_SESSION));
+
+  s->info_callback = (void (*) ()) __VERIFIER_nondet_ulong();
+  s->options = __VERIFIER_nondet_ulong();
+  s->verify_mode = __VERIFIER_nondet_int();
+  (s->session)->peer = (struct x509_st*) __VERIFIER_nondet_ulong();
+  (s->s3)->tmp.cert_request = __VERIFIER_nondet_int();
+  (s->s3)->tmp.new_cipher = malloc(sizeof(struct ssl_cipher_st));
+  ((s->s3)->tmp.new_cipher)->algorithms = __VERIFIER_nondet_ulong();
+  ((s->s3)->tmp.new_cipher)->algo_strength = __VERIFIER_nondet_ulong();
+  if(__VERIFIER_nondet_int())
+  {
+    s->cert = (struct cert_st *) 0;
+  }
+  else
+  {
+    s->cert = malloc(sizeof(struct cert_st));
+    (s->cert)->pkeys[0].privatekey = (struct evp_pkey_st*) __VERIFIER_nondet_ulong(); 
+  }
+
   tmp = ssl3_accept(s);
   }
   return (tmp);