[ 0:01] --symbolic --sequential -o ignore:control [ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/loops/eureka_01_false.c [ 0:01] states per second: 0.134613 [ 7:35] state count: 55 [ 7:35] mips: 0.0091 [ 7:35] symbolic: 1 [14:43] [14:43] error found: yes [14:43] error trace: | [14:43] ASSUME (bvsle #x00000000 var_0) [14:43] ASSUME (not (= (ite (bvsle var_0 #x00000004) #x00000001 #x00000000) #x00000000)) [14:43] ASSUME (bvsle #x00000000 var_1) [14:43] ASSUME (not (= (ite (bvsle var_1 #x00000013) #x00000001 #x00000000) #x00000000)) [14:43] ASSUME (bvslt #x00000000 var_0) [14:43] ASSUME (bvslt #x00000001 var_0) [14:43] ASSUME (not (bvslt #x00000002 var_0)) [14:43] ASSUME (bvslt #x00000000 var_0) [14:43] ASSUME (bvslt #x00000000 var_1) [14:43] ASSUME (not (bvslt #x00000001 var_1)) [14:43] ASSUME (bvslt #x00000001 var_0) [14:43] ASSUME (bvslt #x00000000 var_1) [14:43] ASSUME (not (bvslt #x00000001 var_1)) [14:43] ASSUME (not (bvslt #x00000002 var_0)) [14:43] ASSUME (bvslt #x00000000 var_1) [14:43] ASSUME (not (bvslt #x00000001 var_1)) [14:43] ASSUME (bvslt #x00000000 var_0) [14:43] ASSUME (bvslt #x00000001 var_0) [14:43] (0) Assertion failed: cond, file /home/xrockai/src/divine/nightly/dios/libc/svcomp/svcomp-assert.cpp, line 5. [14:43] [0] FATAL: assertion failure in userspace [14:43] [14:43] active stack: [14:43] - symbol: void __dios::Fault<__dios::Scheduler<__dios::MachineParams<__dios::MonitorManager<__dios::BaseContext> > > >::handler<__dios::fs::VFS<__dios::ProcessManager<__dios::Fault<__dios::Scheduler<__dios::MachineParams<__dios::MonitorManager<__dios::BaseContext> > > > > > >(_VM_Fault, _VM_Frame*, void (*)()) [14:43] location: /dios/include/dios/sys/fault.hpp:193 [14:43] - symbol: __dios_fault [14:43] location: /home/xrockai/src/divine/nightly/dios/libc/sys/fault.c:12 [14:43] - symbol: __assert_fail [14:43] location: /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/assert.c:19 [14:43] - symbol: __VERIFIER_assert [14:43] location: /home/xrockai/src/divine/nightly/dios/libc/svcomp/svcomp-assert.cpp:5 [14:43] - symbol: main [14:43] location: /home/xrockai/src/divine/nightly/test/svcomp/loops/eureka_01_false.c:55 [14:43] - symbol: _start [14:43] location: /dios/src/libc/sys/start.cpp:82 [14:43] a report was written to verify.out [14:43] [15:19] ^ —————. —.— . . —.— . . .————— . . [15:19] ——— | | | | | | |\ | | | | [15:19] —(o)— | | | | | | | \ | |———— '————| [15:19] ——————— | | | \ / | | \| | | [15:19] ————————— —————' —'— ' —'— ' ' '————— ' [15:19] [15:19] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [15:19] traced states: #1 #2 #3 [15:20] # active threads: [0:0] [15:20] T: (0) Assertion failed: cond, file /home/xrockai/src/divine/nightly/dios/libc/svcomp/svcomp-assert.cpp, line 5. [15:20] T: [0] FATAL: assertion failure in userspace [15:20] # executing void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)()) at /dios/include/dios/sys/fault.hpp:193 [15:20] # NOTE: $frame in __dios_fault [15:20] > backtrace [15:20] void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)()) at /dios/include/dios/sys/fault.hpp:193 [15:20] __dios_fault at /home/xrockai/src/divine/nightly/dios/libc/sys/fault.c:12 [15:20] __assert_fail at /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/assert.c:19 [15:20] __VERIFIER_assert at /home/xrockai/src/divine/nightly/dios/libc/svcomp/svcomp-assert.cpp:5 [15:20] main at /home/xrockai/src/divine/nightly/test/svcomp/loops/eureka_01_false.c:55 [15:20] _start at /dios/src/libc/sys/start.cpp:82 [15:20] # executing void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)()) at /dios/include/dios/sys/fault.hpp:193 [15:20] # NOTE: $frame in __dios_fault