Avoid mismatch when generating structs that represent scalar data but also include ZSTs

[adpaco-aws]

Description of changes:

This PR considers another case for the code generation of scalar data. In particular, when the expected type is an ADT, we previously considered two cases: either there is no field or there is one. But in cases where the ADT includes a ZST, the ADT will contain multiple fields: one associated to the scalar data, and other fields associated to the ZSTs. In those cases, we ended up crashing as in #2680:

error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
                                assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_161424092592971241517604180463813633314")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }].

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
assertion failed: `(left == right)`
  left: `2`,
 right: `1`: Error in struct_expr; mismatch in number of fields and values.
	StructTag("tag-_161424092592971241517604180463813633314")
	[Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]

With the changes in this PR, that's no longer the case.

Resolves #2364
Resolves #2680

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

I'm worried this fix is too specific to PhantomData. Instead, we want something that will work for any struct with multiple fields where only one is not ZST.

[celinval]

Awesome! Thanks @adpaco-aws