something is wrong with memory handling in concolic mode

[zapashcanon]

$ dune exec owi -- c --concolic sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby.5.ufo.BOUNDED-10.pals.c -O1 --debug -w1
typechecking ...
linking      ...
interpreting ...
stack        : [  ]
running instr: i32.const 1091
stack        : [ { c = 1091 ; s = (i32 1091) } ]
running instr: i32.const 0
stack        : [ { c = 0 ; s = (i32 0) } ; { c = 1091 ; s = (i32 1091) } ]
running instr: i32.const 1
stack        : [ { c = 1 ; s = (i32 1) } ; { c = 0 ; s = (i32 0) } ; { c = 1091 ; s = (i32 1091) } ]
running instr: memory.init 1
stack        : [  ]
running instr: data.drop 1
stack        : [  ]
stack        : [  ]
running instr: i32.const 1024
stack        : [ { c = 1024 ; s = (i32 1024) } ]
running instr: i32.const 0
stack        : [ { c = 0 ; s = (i32 0) } ; { c = 1024 ; s = (i32 1024) } ]
running instr: i32.const 66
stack        : [ { c = 66 ; s = (i32 66) } ; { c = 0 ; s = (i32 0) } ; { c = 1024 ; s = (i32 1024) } ]
running instr: memory.init 0
stack        : [  ]
running instr: data.drop 0
stack        : [  ]
interpreting ...
stack        : [  ]
running instr: i32.const 1091
stack        : [ { c = 1091 ; s = (i32 1091) } ]
running instr: i32.const 0
stack        : [ { c = 0 ; s = (i32 0) } ; { c = 1091 ; s = (i32 1091) } ]
running instr: i32.const 1
stack        : [ { c = 1 ; s = (i32 1) } ; { c = 0 ; s = (i32 0) } ; { c = 1091 ; s = (i32 1091) } ]
running instr: memory.init 1
Trap: out of bounds memory access
PC:

Assignments:

Model:
  (model
    )
Reached problem!

This requires #281 to be able to get the execution trace.

[filipeom]

Same symptom with global variables. Initial state seems to be corrupted after exploring the first path. Example to reproduce:

;; Loads symbolic memory in various iterations
(module
  (import "symbolic" "i32_symbol" (func $i32 (result i32)))
  (import "symbolic" "assert" (func $assert (param i32)))

  (func $test_globals (param i32)
        (global.get 0)
        (i32.const 2)
        (i32.sub)
        (global.set 0)
        (global.get 0)
        (local.get 0)
        (i32.eq)
        (call $assert))

  (func $main
        (i32.const 40)
        (call $test_globals)
        (if (i32.eq (call $i32) (i32.const 0))
          (then
            (i32.const 38)
            (call $test_globals))))
  (memory $0 1)
  (global $0 (mut i32) (i32.const 42))
  (export "main" (func $main))
  (start $main))

[zapashcanon]

This was fixed in #294 as illustrated in the test in b06034e0beca885cf72b24f2b2e8fdf85e87e98f.