./esbmc-wrapper.py -p /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp -s kinduction --arch 64 /mnt/goblint-svcomp/goblint-bench/bench/concrat/Mirai-Source-Code/main.c


--------------------------------------------------------------------------------


Verifying with ESBMC
Command: ./esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check /mnt/goblint-svcomp/goblint-bench/bench/concrat/Mirai-Source-Code/main.c --64  --no-por --context-bound 2 --witness-output witness.graphml --no-pointer-check --no-bounds-check --data-races-check --no-assertions --incremental-bmc 
ESBMC version 7.4.0 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing /mnt/goblint-svcomp/goblint-bench/bench/concrat/Mirai-Source-Code/main.c
/mnt/goblint-svcomp/goblint-bench/bench/concrat/Mirai-Source-Code/main.c:835:24: warning: passing 'volatile int *' to parameter of type 'int *' discards qualifiers [-Wincompatible-pointer-types-discards-qualifiers]
  __sync_fetch_and_add(& running_threads, 1);
                       ^~~~~~~~~~~~~~~~~
esbmc_intrinsics.h:103:36: note: passing argument to parameter here
int __ESBMC_sync_fetch_and_add(int*, int);
                                   ^
/mnt/goblint-svcomp/goblint-bench/bench/concrat/Mirai-Source-Code/main.c:1701:23: warning: implicitly declaring library function 'ceil' with type 'double (double)' [-Wimplicit-function-declaration]
  binary.num_slices = ceil((double )((float )size / (float )128));
                      ^
/mnt/goblint-svcomp/goblint-bench/bench/concrat/Mirai-Source-Code/main.c:1701:23: note: include the header <math.h> or explicitly provide a declaration for 'ceil'
/mnt/goblint-svcomp/goblint-bench/bench/concrat/Mirai-Source-Code/main.c:1859:13: warning: format specifies type 'unsigned long' but the argument has type 'int' [-Wformat]
            tmp___4);
            ^~~~~~~
Converting
Generating GOTO Program
GOTO program creation time: 0.229s
Adding Data Race Checks
ERROR: Can't construct rvalue reference to array type during dereference
(It isn't allowed by C anyway)


Unknown
