Invariant check failed: Reason: mp_integer should be convertible to target integral type

[ligurio]

<snipped>

1898: Runtime Symex: 1.58311s                                       
1898: size of program expression: 45151 steps
1898: simple slicing removed 1 assignments 
1898: Generated 26942 VCC(s), 22471 remaining after simplification
1898: Runtime Postprocess Equation: 0.00846642s                
1898: Passing problem to propositional reduction
1898: converting SSA                                                                                                                    
1898: --- begin invariant violation report ---                                                                                          
1898: Invariant check failed                                        
1898: File: ../src/util/arith_tools.h:138 function: numeric_cast_v
1898: Condition: maybe
1898: Reason: mp_integer should be convertible to target integral type
1898: Backtrace:
1898: /bin/cbmc(+0xa4a922) [0x55c43c6b6922]
1898: /bin/cbmc(+0xa4b69d) [0x55c43c6b769d]
1898: /bin/cbmc(+0x14d2e2) [0x55c43bdb92e2]
1898: /bin/cbmc(+0x1b70dd) [0x55c43be230dd]
1898: /bin/cbmc(+0xa59e38) [0x55c43c6c5e38]
1898: /bin/cbmc(+0xa5bd47) [0x55c43c6c7d47]
1898: /bin/cbmc(+0xa63f2f) [0x55c43c6cff2f]
1898: /bin/cbmc(+0xa70a7a) [0x55c43c6dca7a]
1898: /bin/cbmc(+0xa7099f) [0x55c43c6dc99f]
1898: /bin/cbmc(+0xa7099f) [0x55c43c6dc99f]
1898: /bin/cbmc(+0xa7099f) [0x55c43c6dc99f]
1898: /bin/cbmc(+0xa7099f) [0x55c43c6dc99f]
1898: /bin/cbmc(+0x7f967d) [0x55c43c46567d]
1898: /bin/cbmc(+0x75640f) [0x55c43c3c240f]
1898: /bin/cbmc(+0x754e52) [0x55c43c3c0e52]
1898: /bin/cbmc(+0x48c42a) [0x55c43c0f842a]
1898: /bin/cbmc(+0x4930d3) [0x55c43c0ff0d3]
1898: /bin/cbmc(+0x493175) [0x55c43c0ff175]
1898: /bin/cbmc(+0x280b46) [0x55c43beecb46]
1898: /bin/cbmc(+0x280de1) [0x55c43beecde1]
1898: /bin/cbmc(+0x28ee6b) [0x55c43befae6b]
1898: /bin/cbmc(+0x157928) [0x55c43bdc3928]
1898: /bin/cbmc(+0x153ed3) [0x55c43bdbfed3]
1898: /bin/cbmc(+0x14ae5f) [0x55c43bdb6e5f]
1898: /bin/cbmc(+0x138ae9) [0x55c43bda4ae9]
1898: /lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f8effa29d90]
1898: /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f8effa29e40]
1898: /bin/cbmc(+0x14c7f5) [0x55c43bdb87f5]
1898: 
1898: 

How-to reproduce

curl -O https://raw.githubusercontent.com/tarantool/tarantool/refs/heads/master/src/trivia/util.h
curl -O https://raw.githubusercontent.com/tarantool/tarantool/refs/heads/master/third_party/qsort_arg.c
curl -O https://raw.githubusercontent.com/tarantool/tarantool/refs/heads/master/third_party/qsort_arg.h

mkdir trivia
echo > trivia/config.h

cat << EOF > qsort.c
#include "qsort_arg.h"
#include "util.h"

int nondet_int(void);

int
qsort_cmp(const void *a, const void *b, void *)
{
	int i = *(int *)a;
	int j = *(int *)b;
	return i < j ? -1 : i > j;
}

int
main(void)
{
	int size = nondet_int();
	size_t n_bytes = size * sizeof(int);
	int *array = (int *)malloc(n_bytes);
	qsort_arg(array, size, sizeof(array[0]), qsort_cmp, NULL);
	free(array);

	return 0;
}
EOF

/bin/goto-cc -I. -o qsort.c.o -c qsort.c 
/bin/goto-cc -I. -fPIC -shared -o qsort_arg.so -c qsort_arg.c
/bin/goto-cc -fPIC qsort.c.o -o qsort_arg.proof ./qsort_arg.so
/bin/cbmc  "--verbosity" "9" "--depth" 1000 ./qsort_arg.proof

CBMC version: 6.3.1 (cbmc-6.3.1)