1extern void abort(void);
   2#include <assert.h>
   3void reach_error() { assert(0); }
   4
   5extern void abort(void);
   6void assume_abort_if_not(int cond) {
   7  if(!cond) {abort();}○NONE
   8}
   9void __VERIFIER_assert(int cond) {
  10  if (!(cond)) {◐PART
  11    ERROR: {reach_error();abort();}
  12  }
  13  return;
  14}
  15#define MAX 5
  16
  17char __VERIFIER_nondet_char();
  18
  19int main(void)
  20{
  21  char input_string[MAX], vogal_array[]={'a','A','e','E','i','I','o','O','u','U','\0'};;
  22  unsigned int  i,j,cont, tam_string, n_caracter;
  23
  24  for(i=0;i<MAX;i++)●FULL
  25    input_string[i] = __VERIFIER_nondet_char();
  26  if (!(input_string[MAX-1]=='\0')) return 0;●FULL
  27
  28  n_caracter = 0;
  29  while(input_string[n_caracter]!='\0')●FULL
  30    n_caracter++;
  31
  32  cont = 0;
  33  for(i=0;i<n_caracter;i++)●FULL
  34     for(j=0;j<MAX/2;j++)●FULL
  35        if(input_string[i] == vogal_array[j])●FULL
  36           cont++;
  37
  38  i=0;
  39  int cont_aux = 0;
  40  while(input_string[i]!='\0')●FULL
  41  {
  42    for(j=0;j<MAX/2;j++)●FULL
  43    {
  44        if(input_string[i] == vogal_array[j])●FULL
  45           cont_aux++;
  46    }
  47    i++;
  48  }
  49  __VERIFIER_assert(cont_aux==cont);
  50
  51  return 0;
  52}
  53