I would have put the id2string(...) on a new line.

It is very confusing that an integer can be "FALSE" or "TRUE". Either there has to be a different result.name, or the value has to be 0/1.

Currently, we have non-1 solutions for "true" in the counterexample, which comes from the fact that we are looking for a non-0 solution when translating the conditional:
// 26 file cover_line_input_boolean.c line 4 function foo
IF !(par != FALSE && a == 1) THEN GOTO 1

However, C99, at least, demands that the values of _Bool are 0 and 1 only. We can output the actual integer value provided that we force "true" to be 1 elsewhere...

This is failing:

void main()
{
  int x;
  _Bool y;
  if(y) 
  {  
    x=(int)y;
    assert(x==1);
  }
}

Note that the above has undefined behaviour, i.e., it's good that this fails!
If you do y=nondet_bool(), with _Bool nondet_bool(), you get the expected result.

We have to explicitly initialise all parameters passed to the entry function otherwise the following would still fail:

void foo(_Bool y)
{
  int x;
  if(y) 
  {  
    x=(int)y;
    assert(x==1);
  }
}

The "binary" should be 0/1; the above yields true/false.

The binary is at least a byte...

Indeed; will merge once value inconsistency is fixed.

The assertion is not guaranteed to hold; e.g., you can wreck this with a union, an uninitialised _Bool, or with a pointer typecast.

Use side_effect_expr_nondett(bool_typet()) instead.