Invariant check failed : Condition: it != bv_cache.end()

[ligurio]

CBMC version: 5.95.1 (cbmc-5.95.1)
Operating system: Ubuntu 22.10 amd64
Exact command line resulting in the issue (see minimized reproducing steps below):

$ goto-cc -I /home/sergeyb/sources/cache/lua -L /home/sergeyb/sources/cache/lua -llua -lm -o lua_load.goto lua_load.c                      
$ cbmc lua_load.goto --trace --verbosity 10 --bitwuzla --unwind 5 --fpa --refine --depth 500 --depth 500 --bounds-check --conversion-check --div-by-zero-check --malloc-fail-null --malloc-may-fail --nan-check --pointer-primitive-check --unwindset luaS_hash.0:20 --unwindset tablerehash.0:130 --unwindset stack_init.0:50 --unwindset internshrstr.0:10 --unwindset luaS_init.0:10 --unwindset luaS_init.1:50 --unwindset luai_makeseed.0:10 --unwindset lua_newstate.0:10 --unwindset luaO_ceillog2.0:10 --unwindset clearNewSlice.0:10 --unwindset reinsert.0:10 --unwindset l_str2dloc.0:100 --unwindset l_str2dloc.1:100 --unwindset l_str2dloc.2:100 --unwindset l_str2dloc.3:100 --unwindset memcmp.0:50 --unwindset strchr.0:100 --unwindset strcpy.0:100 --unwindset strlen.0:100 --unwindset markold.0:50 --unwinding-assertions --object-bits 16 --xml-ui > lua_load-result.xml

What behavior did you expect: success
What happened instead:

--- begin invariant violation report ---
Invariant check failed                                                   
File: ../src/solvers/flattening/boolbv_get.cpp:263 function: bv_get_cache 
Condition: it != bv_cache.end() 
Reason: Check return value
Backtrace:
cbmc(+0xaccd60) [0x57d408f0fd60]                                         
cbmc(+0xacda39) [0x57d408f10a39]
cbmc(+0x1c46d4) [0x57d4086076d4]                                         
cbmc(+0x7bab66) [0x57d408bfdb66]                                                                                                                   
cbmc(+0x7bd2f1) [0x57d408c002f1]                                                                                                                   
cbmc(+0x7bbcc1) [0x57d408bfecc1]                                                                                                                   
cbmc(+0x7e84c0) [0x57d408c2b4c0]                                                                                                                   
cbmc(+0x7be6aa) [0x57d408c016aa]                                                                                                                   
cbmc(+0x806d70) [0x57d408c49d70]                                                                                                                   
cbmc(+0x7be5c3) [0x57d408c015c3]                                                                                                                   
cbmc(+0x806d70) [0x57d408c49d70]                                                                                                                   
cbmc(+0x7be5c3) [0x57d408c015c3]                                                                                                                   
cbmc(+0x806d70) [0x57d408c49d70]                                                                                                                   
cbmc(+0x7be5c3) [0x57d408c015c3]                                                                                                                   
cbmc(+0x813abb) [0x57d408c56abb]                                                                                                                   
cbmc(+0x80cc8b) [0x57d408c4fc8b]
cbmc(+0x2f8342) [0x57d40873b342]
cbmc(+0x307437) [0x57d40874a437]
cbmc(+0x1cfe32) [0x57d408612e32]
cbmc(+0x1cb65b) [0x57d40860e65b]
cbmc(+0x1c206f) [0x57d40860506f]
cbmc(+0x1aebf9) [0x57d4085f1bf9]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7ec716e29d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7ec716e29e40]
cbmc(+0x1c3a05) [0x57d408606a05]

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

Steps to reproduce

$ git clone https://github.com/lua/lua
$ cd lua
$ make CC=goto-cc LD=goto-ld CFLAGS=-DLUA_USE_LINUX
$ cat << EOF > sample.c
#include <assert.h>
#include "lua.h"

lua_State *
__luaL_newstate()
{
	lua_State *L = luaL_newstate();
	return L;
}

static const char *
Reader(lua_State *L, void *data, size_t *size)
{
	static char *buf = NULL;
	free(buf);
	*size = 1;
	buf = (char *)malloc(*size);
	__CPROVER_assume(buf != NULL);
	__CPROVER_assume(buf[size-1] == '\0');
	return buf;
}

int
main()
{
	lua_State *L = __luaL_newstate();
	lua_load(L, Reader, NULL, "cbmc", "t");
	return 0;
}
> EOF
$ goto-cc -I . -L . -llua -lm -o sample.goto sample.c
$  cbmc lua_load.goto --trace --bitwuzla --fpa --refine --depth 500 --bounds-check --conversion-check --div-by-zero-check --malloc-fail-null --malloc-may-fail --nan-check --pointer-primitive-check --object-bits 16 

<snipped>

--- begin invariant violation report ---
Invariant check failed                                                   
File: ../src/solvers/flattening/boolbv_get.cpp:263 function: bv_get_cache 
Condition: it != bv_cache.end() 
Reason: Check return value
Backtrace:

<snipped>