[HWToBTOR2] Support unary case of variadics

[TaoBi22]

This adds support for the case where a variadic op has only one operand by just forwarding future LID lookups of that op to the LID of the operand. There's also a tweak to some value names in the comb HWToBTOR2 test to avoid the faff of incrementing the names every time more NIDs are added.

I don't think there's any need to check for the nullary case since, based on a bit of testing, nullary comb variadics shouldn't be valid since there's no valid result type that can be derived, but if that's not the case then I'll add a check!

[tobiasgrosser]

Why is there no valid result that can be derived? Does the verifier reject nullary comp operations?

[TaoBi22]

Why is there no valid result that can be derived? Does the verifier reject nullary comp operations?

In my testing it couldn't derive a valid result type because they necessarily have a bitvector result type which can't be inferred from no inputs - I wasn't sure if there was some construction that could get around this but upon further inspection the verifier actually explicitly rejects them here

[tobiasgrosser]

Why is there no valid result that can be derived? Does the verifier reject nullary comp operations?

In my testing it couldn't derive a valid result type because they necessarily have a bitvector result type which can't be inferred from no inputs - I wasn't sure if there was some construction that could get around this but upon further inspection the verifier actually explicitly rejects them here

Then write this in the commit message. State that variadic operations with zero results are not supported.

[TaoBi22]

Then write this in the commit message. State that variadic operations with zero results are not supported.

I've added a comment to this effect