Code generation error

[Skypr]

When generating code which BEAST claims as valid, and then starting CBMC, an error occurs:

Expected behavior

The user should be able to compare two voting arrays.

Actual behavior

If the user wants to compare two voting arrays, cbmc fails with the error:

member operator requires structure type on left hand side but got `unsigned int [1]'
CONVERSION ERROR
Numeric exception : 0

Steps to reproduce the behavior

Open BEAST, create a new Project with In: Single Choice, Out: Single Candidate.
In the code window: write
return votes[0];
In the PreProperty window, add:
VOTES1 == VOTES2;
In the PostProperty window add:
ELECT1 != ELECT2;

An excerpt of the code which causes the error is:
` unsigned int votes1[V];
for(unsigned int counter_0 = 0; counter_0 < V1; counter_0++){
votes1[counter_0] = nondet_uint();
assume((0 <= votes1[counter_0]) && (votes1[counter_0] < C1));
}

    unsigned int votes2[V];
    for(unsigned int counter_0 = 0; counter_0 < V2; counter_0++){
            votes2[counter_0] = nondet_uint();
            assume((0 <= votes2[counter_0]) && (votes2[counter_0] < C2));
    }
    
    unsigned int comparison_0 = 1;
    for(unsigned int count_0 = 0; comparison_0 && count_0 < V; ++count_0) {
            comparison_0 = votes1.arr[count_0] == votes2.arr[count_0];
    }`

The error appears because votesN is not a struct with the content ".arr", as expected, but just a normal array.