gib# out run test/svcomp/pthread/read_write_lock.pkg.c error -DBUG error error --location-comment ERROR
gib# cmd /usr/bin/env
gib#     srcdir=/home/xrockai/src/divine/nightly
gib#     PATH=/home/xrockai/src/divine/nightly/test/lib:/usr/bin:/bin:/opt/klee/bin
gib#     sh
gib#     /home/xrockai/src/divine/nightly/test/lib/check
gib#     test/svcomp/pthread/read_write_lock.pkg.c
gib#     error
gib#     
gib#     -DBUG
gib#     
gib#     error
gib#     
gib#     error --location-comment ERROR
expect --result error --location-comment ERROR
cc     -o test.bc  -DBUG /home/xrockai/src/divine/nightly/test/svcomp/pthread/read_write_lock.pkg.c
verify -o nofail:malloc  test.bc

compiling /home/xrockai/src/divine/nightly/test/svcomp/pthread/read_write_lock.pkg.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 257.991
state count: 3624
mips: 0.28

error found: yes
error trace: |
  FAULT: /home/xrockai/src/divine/nightly/test/svcomp/pthread/read_write_lock.pkg.c:46: void *reader(void *): assertion 'y == x' failed
  [4] FATAL: assertion failure in userspace

active stack:
  - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)())
    location: /dios/sys/fault.hpp:118
  - symbol: __dios_fault
    location: /dios/arch/divm/fault.c:12
  - symbol: __assert_fail
    location: /dios/libc/_PDCLIB/assert.c:19
  - symbol: reader
    location: /home/xrockai/src/divine/nightly/test/svcomp/pthread/read_write_lock.pkg.c:46
  - symbol: __pthread_start
    location: /dios/libc/pthread/pthread-init.cpp:82
  - symbol: __pthread_entry
    location: /dios/libc/pthread/pthread-core.cpp:51