Checks for multiple init and next blocks and throws a parser error if encountered

[polgreen]

No description provided.

[polgreen]

@kkmc I've disabled the code that combines init blocks in this PR, because the order they were combined in if there were two blocks written in the same module in the input file seemed to be nondeterministic

e.g., this passes:

module main {
  var x : integer;

  init {
    x = 1;
  }

  init {
    x = 0;
  }

  invariant prop_eq: x == 0;

  control {
    v = bmc(5);
    check;
    print_results;
  }
}

and this passes:

module main {
  var x : integer;

  init {
    x = 0;
  }

  init {
    x = 1;
  }

  invariant prop_eq: x == 0;

  control {
    v = bmc(5);
    check;
    print_results;
  }
}

But this does not:

module main {
  var x : integer;

  init {
    x=0;
    x = 1;
  }

  invariant prop_eq: x == 0;

  control {
    v = bmc(5);
    check;
    print_results;
  }
}

Do you need this code for the TAP proofs? If so, we need to figure out how to combine the init blocks in the order they are parsed in