./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/dnspod-sr/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/dnspod-sr/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/dnspod-sr/main.c
/mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c:7430:74: warning: format specifies type 'unsigned int' but the argument has type 'mbuf_type *' (aka 'struct _mem_buf *') [-Wformat]
    printf((char const   * __restrict  )"del list val =0, mbuf:0x%0x\n", mbuf);
                                                                 ~~~     ^~~~
Converting
Generating GOTO Program
GOTO program creation time: 0.598s
Adding Data Race Checks
GOTO program processing time: 6.146s
Checking base case, k = 1
Starting Bounded Model Checking
Symex completed in: 0.009s (123 assignments)
Slicing time: 0.000s (removed 113 assignments)
Generated 2 VCC(s), 1 remaining after simplification (10 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.002s
BMC program time: 0.010s
No bug has been found in the base case
Checking forward condition, k = 1
Starting Bounded Model Checking
Symex completed in: 0.008s (123 assignments)
Slicing time: 0.000s (removed 113 assignments)
Generated 2 VCC(s), 1 remaining after simplification (10 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s
BMC program time: 0.008s
Building successful trace
Generating Correctness Witness for: /mnt/goblint-svcomp/goblint-bench/bench/concrat/dnspod-sr/main.c

VERIFICATION SUCCESSFUL

Solution found by the forward condition; all states are reachable (k = 1)

TRUE
