goto-instrument for k-induction fails invariant check on SV-COMP style single loop reachability problem

[AdamZsofi]

CBMC version: 5.70.0 (cbmc-5.70.0-121-g4f69955d00, https://gitlab.com/sosy-lab/sv-comp/archives-2023/-/raw/svcomp23/2023/cbmc.zip )
Operating system: Linux (Ubuntu 22.04)

Exact command line resulting in the issue:

(0):

./goto-cc --object-bits 11 -m64 --function main count2.c -o count2.c.goto

(1):

./goto-instrument count2.c.goto count2.c.goto-10-step --step-case --k-induction 10 --remove-function-body reach_error --generate-function-body reach_error --generate-function-body-options assert-false
Reading GOTO program from 'count2.c.goto'
Removing body of reach_error
Instrumenting k-induction for k=10, step case
--- begin invariant violation report ---
Invariant check failed
File: ../src/util/dense_integer_map.h:241 function: setup_for_keys
Condition: seen_keys.insert(integer_key).second
Reason: keys for use in dense_integer_mapt must be unique
Backtrace:
./goto-instrument(+0xbb10a0) [0x584ecb24f0a0]
./goto-instrument(+0xbb1649) [0x584ecb24f649]
./goto-instrument(+0x2f3618) [0x584eca991618]
./goto-instrument(+0x312034) [0x584eca9b0034]
./goto-instrument(+0x34baf9) [0x584eca9e9af9]
./goto-instrument(+0x4b3b09) [0x584ecab51b09]
./goto-instrument(+0x2f8580) [0x584eca996580]
./goto-instrument(+0x2faec3) [0x584eca998ec3]
./goto-instrument(+0xbfaaef) [0x584ecb298aef]
./goto-instrument(+0x2f418f) [0x584eca99218f]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7b9004e29d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7b9004e29e40]
./goto-instrument(+0x2f302e) [0x584eca99102e]


--- end invariant violation report ---
Aborted (core dumped)

(2):

./goto-instrument count2.c.goto count2.c.goto.instrumented --remove-function-body reach_error --generate-function-body reach_error --generate-function-body-options assert-false
Reading GOTO program from 'count2.c.goto'
Removing body of reach_error
Writing GOTO program to 'count2.c.goto.instrumented'

What behaviour did you expect:
I am trying to update a few years old k-induction wrapper script for CBMC. I based the first goto-instrument command (2) above on the current SV-COMP wrapper script of CBMC and then added the --k-invariant and --step/base-case flags respectively in (1). I would expect (1) to work, if (2) also does. I get the same error output both for the base case and the step case.

The input program count2.c is a single loop program (generated from a simple btor2 circuit), the property is the SV-COMP unreach call property, with reach_error as the fail function. Files are added below.

count2.c.txt
count2.c.goto.txt

What happened instead:
See output of command (1)