CBMC crashes when shadow memory used with zero-sized types

[celinval]

CBMC shadow memory doesn't seem to handle well ZSTs, including structures with ZST fields and ZST structures. I created this small example:

// shadow.c
struct ZeroSized {};

struct WithZST {
  int i;
  struct ZeroSized zst;
};

struct TopStruct {
  int f1;
  struct WithZST f2;
};

void main() {
  __CPROVER_field_decl_local("shadow", (_Bool)0);
  struct TopStruct top;

  // This works
  __CPROVER_set_field(&top.f1, "shadow", 1);
  __CPROVER_assert(__CPROVER_get_field(&top.f1, "shadow") == 1,
                   "expected success: set field to value 1");

  // This crashes
  __CPROVER_assert(__CPROVER_get_field(&top.f2, "shadow") == 0,
                   "expected success: default value is 0");
}

CBMC version: 5.95.1
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: cbmc shadow.c
What behaviour did you expect: I expected the verification to succeed.
What happened instead: CBMC crashed with the following error:

Logs:

CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing struct.c
Converting
Type-checking struct
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00104798s
size of program expression: 36 steps
simple slicing removed 2 assignments
Generated 2 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 7.654e-06s
Passing problem to propositional reduction
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/flattening/boolbv.cpp:70 function: convert_bv
Condition: variable number must be different from the unused variable number
Reason: literal.var_no() != literalt::unused_var_no()
Backtrace:
...

Diagnostics: 
<< EXTRA DIAGNOSTICS >>
source location: 
bitor
  * type: c_bool
      * width: 8
<< END EXTRA DIAGNOSTICS >>