./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/lmdb/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/lmdb/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/lmdb/main.c
Converting
Generating GOTO Program
GOTO program creation time: 0.760s
Adding Data Race Checks
ERROR: Unexpected side-effect: sideeffect
* operand : typecast
    * from : symbol
        * name : c:main.c@300761@F@mdb_midl_grow@idn
        * renamelev : Level 0
        * level1_num : 0
        * level2_num : 0
        * thread_num : 0
        * node_num : 0
        * type : pointer
          * subtype : unsignedbv
              * width : 64
    * rounding_mode : symbol
        * name : c:@__ESBMC_rounding_mode
        * renamelev : Level 0
        * level1_num : 0
        * level2_num : 0
        * thread_num : 0
        * node_num : 0
        * type : signedbv
          * width : 32
    * type : pointer
      * subtype : empty
* size : mul
    * side_1 : add
        * side_1 : add
            * side_1 : dereference
                * pointer : symbol
                    * name : c:main.c@300761@F@mdb_midl_grow@idn
                    * renamelev : Level 0
                    * level1_num : 0
                    * level2_num : 0
                    * thread_num : 0
                    * node_num : 0
                    * type : pointer
                      * subtype : unsignedbv
                          * width : 64
                * type : unsignedbv
                  * width : 64
            * side_2 : typecast
                * from : symbol
                    * name : c:main.c@300745@F@mdb_midl_grow@num
                    * renamelev : Level 0
                    * level1_num : 0
                    * level2_num : 0
                    * thread_num : 0
                    * node_num : 0
                    * type : signedbv
                      * width : 32
                * rounding_mode : symbol
                    * name : c:@__ESBMC_rounding_mode
                    * renamelev : Level 0
                    * level1_num : 0
                    * level2_num : 0
                    * thread_num : 0
                    * node_num : 0
                    * type : signedbv
                      * width : 32
                * type : unsignedbv
                  * width : 64
            * type : unsignedbv
              * width : 64
        * side_2 : constant_int
            * value : 2
            * type : unsignedbv
              * width : 64
        * type : unsignedbv
          * width : 64
    * side_2 : constant_int
        * value : 8
        * type : unsignedbv
          * width : 64
    * type : unsignedbv
      * width : 64
* arguments : 

* alloctype : realloc
* type : pointer
  * subtype : empty

Unknown
