hw-cbmc timeframe array bounds

After building the hw-cbmc executable from source and trying a simple example to equivalence check C with Verilog, I ran into the issue that assertions never pass once a Verilog module is involved.

The example in question is: tester.c

#include <assert.h>

extern const unsigned int bound;

void next_timeframe(void);
void set_inputs(void);

typedef unsigned char _u8;

struct module_zero_giver{
  _Bool enable;
  _u8 out;
};
extern struct module_zero_giver zero_giver;
int main()
{
zero_giver.enable = 1;
set_inputs();
assert(zero_giver.out == 0);
}

tested_rtl.v

module zero_giver(
input enable,
output [7:0] out
);
assign out = (enable == 1)? 0:1;
endmodule

Using the command hw-cbmc tested_rtl.v tester.c --module zero_giver produces the following result:

HW-CBMC version 6.3.1 (cbmc-6.3.1-10-g83922b2f54)
Starting Bounded Model Checking
Type-checking Verilog::zero_giver
Type-checking tester
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)
Mapping variables
mapping `zero_giver.enable' to `zero_giver.enable'
mapping `zero_giver.out' to `zero_giver.out'
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
converting constraints
Runtime Symex: 0.00164032s
size of program expression: 31 steps
simple slicing removed 5 assignments
Generated 3 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 0.000936248s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0077181s
Running propositional reduction
Runtime Post-process: 5.876e-06s
638 variables, 1799 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00438444s
Runtime decision procedure: 0.0123259s
Running propositional reduction
639 variables, 2 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 5.4916e-05s
Runtime decision procedure: 8.2e-05s

** Results:
[array_bounds.1] file tester.c line 14 array 'zero_giver_array' lower bound in zero_giver_array[timeframe]: FAILURE
[array_bounds.2] file tester.c line 14 array 'zero_giver_array' upper bound in zero_giver_array[timeframe]: FAILURE
tester.c function main
[main.assertion.1] line 19 assertion zero_giver.out == 0: FAILURE

** 3 of 3 failed (3 iterations)
VERIFICATION FAILED

Is there any definition I am missing in my proof harness? Using an even simpler Verilog code such as assign out = 0; and removing set_inputs() still fails the assertion, but the bound errors are gone as well.

diffblue / hw-cbmc

hw-cbmc timeframe array bounds #788