gib# out run test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c
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/product-lines/email_spec27_product18_false.cil.chk.c
expect --result error --location-comment ERROR
cc     -o test.bc   /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c
verify --symbolic --solver stp -o nofail:malloc -o ignore:control  test.bc

compiling /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c
/home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:363:44: warning: incompatible redeclaration of library function 'malloc'
extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
                                           ^
/home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:363:44: note: 'malloc' is a builtin with type 'void *(unsigned long)'
1 warning generated.
loading bitcode … DiOS … LART … RR … constants … done
booting … done
searching:        1 states in  1:00, avg     0.0/s @ 87.8 kips, queued: 0
searching:      114 states in  2:00, avg     0.9/s @ 141.6 kips, queued: 0
searching:      410 states in  3:00, avg     2.3/s @ 194.5 kips, queued: 26
searching:      811 states in  4:00, avg     3.4/s @ 212.4 kips, queued: 22
searching:     1107 states in  5:00, avg     3.7/s @ 220.2 kips, queued: 30
searching:     1403 states in  6:00, avg     3.9/s @ 239.4 kips, queued: 38
searching:     1931 states in  7:00, avg     4.6/s @ 253.2 kips, queued: 56
searching:     2429 states in  8:00, avg     5.1/s @ 267.8 kips, queued: 60
searching:     2989 states in  9:00, avg     5.5/s @ 277.6 kips, queued: 66
searching:     3737 states in 10:00, avg     6.2/s @ 287.0 kips, queued: 78
searching:     4405 states in 11:00, avg     6.7/s @ 294.5 kips, queued: 84
searching:     4961 states in 12:00, avg     6.9/s @ 300.0 kips, queued: 94
searching:     6007 states in 13:00, avg     7.7/s @ 308.6 kips, queued: 106
states per second: 7.98321
state count: 6564
mips: 0.31
symbolic: 1

error found: yes
error trace: |
  [0] bob: 1
  [0] rjh: 2
  [0] chuck: 3
  ASSUME (not (not (= var_1 #x00000000)))
  ASSUME (not (not (= var_2 #x00000000)))
  ASSUME (not (not (= var_3 #x00000000)))
  ASSUME (not (not (= var_4 #x00000000)))
  ASSUME (not (not (= var_5 #x00000000)))
  ASSUME (not (not (= var_6 #x00000000)))
  ASSUME (not (not (= var_7 #x00000000)))
  ASSUME (not (not (= var_8 #x00000000)))
  ASSUME (not (not (= var_9 #x00000000)))
  ASSUME (not (not (= var_10 #x00000000)))
  ASSUME (not (= var_11 #x00000000))
  ASSUME (not (not (= var_12 #x00000000)))
  ASSUME (not (not (= var_13 #x00000000)))
  ASSUME (not (not (= var_14 #x00000000)))
  ASSUME (not (not (= var_15 #x00000000)))
  ASSUME (not (not (= var_16 #x00000000)))
  ASSUME (not (not (= var_17 #x00000000)))
  ASSUME (not (not (= var_18 #x00000000)))
  ASSUME (not (= var_19 #x00000000))
  ASSUME (not (not (= var_20 #x00000000)))
  ASSUME (not (not (= var_21 #x00000000)))
  ASSUME (not (not (= var_22 #x00000000)))
  ASSUME (not (= var_23 #x00000000))
  ASSUME (not (not (= var_24 #x00000000)))
  ASSUME (not (= var_25 #x00000000))
  [0] Please enter a subject and a message body.
  [0] 
  [0] mail sent
  [0] keypair valid 123 123before deliver
  [0] 
  [0] mail delivered
  [0] 
  [0] sending autoresponse
  [0] 
  [0] mail sent
  [0] before deliver
  [0] 
  FAULT: verifier error called
  [0] FATAL: dios assertion violation 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: __VERIFIER_error
    location: /dios/libc/svcomp/svcomp-error.cpp:5
  - symbol: __automaton_fail
    location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:2898
  - symbol: __utac_acc__VerifyForward_spec__1
    location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:2847
  - symbol: deliver
    location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:2597
  - symbol: incoming__wrappee__Keys
    location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:2608
  - symbol: incoming__wrappee__Sign
    location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:2618
  - symbol: incoming
    location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:2637
  - symbol: mail
    location: /home/xrockai/src/divine/nightly/test/svcomp/product-lines/email_spec27_product18_false.cil.chk.c:2560