It is not really allowed to have multiple never claims in spin.
If one does so, spin -a will give the following warning:

the model contains 2 never claims: never_1, never_0
only one claim is used in a verification run
choose which one with ./pan -N name (defaults to -N never_0)

Epispin remains silent on the following program:

…

never{
true;
}

never{
false;
}

init{
skip;
}

…
Apologies for the missing underscores to Danny… :-)

Submitted by Kees Pronk on 29 August 2011 at 22:04

Epispin gives a similar error from version 1.0.3 on.