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 @ 91.1 kips, queued: 0
searching:      114 states in  2:00, avg     0.9/s @ 123.1 kips, queued: 0
searching:      410 states in  3:00, avg     2.3/s @ 185.5 kips, queued: 26
searching:      780 states in  4:00, avg     3.2/s @ 230.8 kips, queued: 36
searching:     1224 states in  5:00, avg     4.1/s @ 243.4 kips, queued: 48
searching:     1604 states in  6:00, avg     4.5/s @ 257.1 kips, queued: 58
searching:     1900 states in  7:00, avg     4.5/s @ 270.4 kips, queued: 72
searching:     2576 states in  8:00, avg     5.4/s @ 281.7 kips, queued: 66
searching:     3219 states in  9:00, avg     6.0/s @ 289.9 kips, queued: 72
searching:     3722 states in 10:00, avg     6.2/s @ 291.9 kips, queued: 80
searching:     4344 states in 11:00, avg     6.6/s @ 295.6 kips, queued: 88
searching:     4886 states in 12:00, avg     6.8/s @ 297.3 kips, queued: 102
searching:     5781 states in 13:00, avg     7.4/s @ 303.3 kips, queued: 108
searching:     6588 states in 14:00, avg     7.8/s @ 308.8 kips, queued: 108
states per second: 8.19869
state count: 7240
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 (= var_9 #x00000000))
  ASSUME (not (not (= var_10 #x00000000)))
  ASSUME (not (not (= var_11 #x00000000)))
  ASSUME (not (not (= var_12 #x00000000)))
  ASSUME (not (= var_13 #x00000000))
  ASSUME (not (not (= var_14 #x00000000)))
  ASSUME (not (= var_15 #x00000000))
  ASSUME (not (not (= var_16 #x00000000)))
  ASSUME (not (not (= var_17 #x00000000)))
  ASSUME (not (not (= var_18 #x00000000)))
  ASSUME (not (not (= var_19 #x00000000)))
  ASSUME (not (not (= var_20 #x00000000)))
  ASSUME (not (not (= var_21 #x00000000)))
  ASSUME (not (not (= var_22 #x00000000)))
  ASSUME (not (not (= var_23 #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