[ 0:00] + divine verify -std=c++11 /home/xrockai/src/divine/nightly/test/demo/thread.cpp [ 0:00] + tee report.txt [ 0:00] compiling /home/xrockai/src/divine/nightly/test/demo/thread.cpp [ 0:00] loading bitcode … DiOS … LART … RR … constants … done [ 0:09] booting … done [ 0:09] states per second: 154.07 [ 0:12] state count: 371 [ 0:12] mips: 0.41 [ 0:12] [ 0:13] error found: yes [ 0:13] error trace: | [ 0:13] [0] starting thread [ 0:13] [1] thread started [ 0:13] [0] incrementing [ 0:13] [1] thread done [ 0:13] [0] waiting for the thread [ 0:13] [0] thread joined [ 0:13] FAULT: /home/xrockai/src/divine/nightly/test/demo/thread.cpp:18: int main(): assertion 'x == 2' failed [ 0:13] [0] FATAL: assertion failure in userspace [ 0:13] [ 0:13] active stack: [ 0:13] a report was written to thread.report [ 0:13] - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)()) [ 0:13] location: /dios/sys/fault.hpp:118 [ 0:13] - symbol: __dios_fault [ 0:13] location: /dios/arch/divm/fault.c:12 [ 0:13] - symbol: __assert_fail [ 0:13] location: /dios/libc/_PDCLIB/assert.c:24 [ 0:13] - symbol: main [ 0:13] location: /home/xrockai/src/divine/nightly/test/demo/thread.cpp:18 [ 0:13] - symbol: __dios_start [ 0:13] location: /dios/libc/sys/start.cpp:94 [ 0:13] + cat [ 0:14] + ordgrep expected [ 0:14] [0] starting thread | \[0\] starting thread [ 0:14] [0] incrementing | \[0\] incrementing [ 0:14] [1] thread done | \[1\] thread done [ 0:14] + check debris [ 0:14] + test -e warning