[ 0:01]   | load /home/xrockai/src/divine/nightly/test/svcomp/recursion/Fibonacci04_false.c Fibonacci04_false.c
[ 0:01]   | expect --result error --location Fibonacci04_false.c:35
[ 0:01]   | expect --trace FAULT: --trace-count 1
[ 0:01]   | cc -o testcase.bc Fibonacci04_false.c
[ 0:01]   | verify --max-memory 4GiB --max-time 600 --threads 2 --report-filename verify.out --solver z3 --symbolic --sequential testcase.bc
[ 0:01] compiling Fibonacci04_false.c
[ 0:01] loading bitcode … DiOS … LART … RR … constants … done
[ 0:14] booting … done
[ 0:14] states per second: 9.64886
[ 0:24] state count: 97
[ 0:24] mips: 0.12
[ 0:24] symbolic: 1
[ 0:26] 
[ 0:26] error found: yes
[ 0:26] error trace: |
[ 0:26]   ASSUME (not (bvslt var_1 #x00000001))
[ 0:26]   ASSUME (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001)))
[ 0:26]   ASSUME (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000002) #x00000001))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000002) #x00000001)))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000002) #x00000001))) (= (bvsub (bvsub var_1 #x00000002) #x00000002) #x00000001))
[ 0:26]   ASSUME (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (bvslt var_1 #x00000001)) (not (= var_1 #x00000001))) (not (bvslt (bvsub var_1 #x00000001) #x00000001))) (not (= (bvsub var_1 #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000001) #x00000002) #x00000002) #x00000001)) (not (bvslt (bvsub var_1 #x00000002) #x00000001))) (not (= (bvsub var_1 #x00000002) #x00000001))) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (= (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001))) (not (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001))) (= (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000001) #x00000001)) (bvslt (bvsub (bvsub (bvsub var_1 #x00000002) #x00000001) #x00000002) #x00000001)) (not (bvslt (bvsub (bvsub var_1 #x00000002) #x00000002) #x00000001))) (= (bvsub (bvsub var_1 #x00000002) #x00000002) #x00000001)) (not (not (= var_1 #x00000005))))
[ 0:26]   FAULT: verifier error called
[ 0:26]   [0] FATAL: dios assertion violation in userspace
[ 0:26] 
[ 0:26] active stack:
[ 0:27]   - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)())
[ 0:27]     location: /dios/sys/fault.hpp:118
[ 0:27]   - symbol: __dios_fault
[ 0:27]     location: /dios/arch/divm/fault.c:12
[ 0:27]   - symbol: __VERIFIER_error
[ 0:27]     location: /dios/libc/svcomp/svcomp-error.cpp:5
[ 0:27]   - symbol: main
[ 0:27]     location: Fibonacci04_false.c:35
[ 0:27]   - symbol: __dios_start
[ 0:27]     location: /dios/libc/sys/start.cpp:94
[ 0:27] + divine sim --batch --skip-init --load-report verify.out
[ 0:27] 
[ 0:39]            ^       —————.   —.—  .     .  —.—  .     .  .—————    .    .
[ 0:39]           ———      |     |   |   |     |   |   |\    |  |         |    |
[ 0:39]          —(o)—     |     |   |   |     |   |   |  \  |  |————     '————|
[ 0:39]         ———————    |     |   |    \   /    |   |    \|  |              |
[ 0:39]        —————————   —————'   —'—     '     —'—  '     '  '—————         '
[ 0:39] 
[ 0:39] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started.
[ 0:39] traced states:
[ 0:41] ▶ state   #16 [new] -- active threads: [0:0] --
[ 0:41] T: FAULT: verifier error called
[ 0:41] # executing void __dios::FaultBase::handler<{Context}>(_VM_Fault, _VM_Frame*, void (*)()) at /dios/sys/fault.hpp:118
[ 0:41] # NOTE: $frame in __dios_fault
[ 0:41] > backtrace
[ 0:41]   void __dios::FaultBase::handler<{Context}>(_VM_Fault, _VM_Frame*, void (*)()) at /dios/sys/fault.hpp:118
[ 0:41]   __dios_fault at /dios/arch/divm/fault.c:12
[ 0:41]   __VERIFIER_error at /dios/libc/svcomp/svcomp-error.cpp:5
[ 0:41]   main at Fibonacci04_false.c:35
[ 0:41]   __dios_start at /dios/libc/sys/start.cpp:94
[ 0:41] # executing void __dios::FaultBase::handler<{Context}>(_VM_Fault, _VM_Frame*, void (*)()) at /dios/sys/fault.hpp:118
[ 0:41] # NOTE: $frame in __dios_fault