./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec0_product22.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec0_product22.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:314:3-335:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:371:3-396:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:456:5-476:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:165:1-173:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:203:1-212:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:243:1-288:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:289:1-344:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:345:1-404:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:407:1-509:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:510:1-555:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:556:1-601:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:618:1-632:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:654:1-669:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:746:1-766:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:767:1-782:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:785:1-805:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:806:1-821:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:898:1-916:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:917:1-932:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:935:1-953:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:954:1-969:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:972:1-990:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:991:1-1006:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1184:1-1198:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1431:1-1441:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1520:1-1531:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1532:1-1543:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1652:1-1666:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1670:1-1695:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1696:1-1715:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1720:1-1743:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1744:1-1763:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1767:1-1790:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1791:1-1810:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1811:1-1835:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1845:1-1913:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1914:1-1982:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1983:1-2038:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2048:1-2116:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2117:1-2172:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:195-195)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2336-2336)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:186-186)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2519..2520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2519-2520)
  on lines 2542..2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2542-2544)
  on lines 2546..2548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2546-2548)
  on lines 2550..2551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2550-2551)
  on line 2560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2560-2560)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2197-2197)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2632-2632)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2671..2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2671-2672)
  on line 2679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2679-2679)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2464..2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2464-2466)
  on lines 2468..2469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2468-2469)
  on lines 2473..2476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2473-2476)
  on lines 2478..2480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2478-2480)
  on lines 2482..2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2482-2483)
  on lines 2487..2490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2487-2490)
  on lines 2492..2494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2492-2494)
  on lines 2496..2497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2496-2497)
  on lines 2501..2502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2501-2502)
  on line 2506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2506-2506)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2286..2287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2286-2287)
  on line 2291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2291-2291)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2357..2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2357-2359)
  on lines 2361..2362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2361-2362)
  on lines 2366..2369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2366-2369)
  on lines 2371..2373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2371-2373)
  on lines 2375..2376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2375-2376)
  on lines 2380..2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2380-2383)
  on lines 2385..2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2385-2387)
  on lines 2389..2390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2389-2390)
  on lines 2394..2395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2394-2395)
  on line 2399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2399-2399)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2244-2244)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 870..871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:870-871)
  on line 877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:877-877)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 681..682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:681-682)
  on line 688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:688-688)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 644..645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:644-645)
  on line 651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:651-651)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 718..719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:718-719)
  on line 725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:725-725)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1237-1237)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1246-1246)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 833..834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:833-834)
  on line 840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:840-840)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1263..1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1263-1264)
  on line 1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1271-1271)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:162-162)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:142-142)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1228-1228)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2205-2205)
  on lines 2210..2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2210-2211)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2640-2640)
  on lines 2645..2646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2645-2646)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2571..2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2571-2572)
  on lines 2582..2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2582-2583)
  on lines 2593..2594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2593-2594)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2410..2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2410-2411)
  on lines 2421..2422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2421-2422)
  on lines 2432..2433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2432-2433)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:888-888)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:699-699)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:851-851)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:736-736)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:233-233)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 527
  dead: 620 (499 in uncalled functions)
  total lines: 1147
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2579:11-2579:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2589:11-2589:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:832:9-832:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2590:13-2590:23)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1475:7-1475:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:850:9-850:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2407:9-2407:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:869:9-869:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2418:11-2418:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2639:7-2639:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2204:7-2204:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2428:11-2428:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2642:9-2642:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2429:13-2429:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2207:9-2207:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:887:9-887:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:643:9-643:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2459:7-2459:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2460:9-2460:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2670:11-2670:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:680:9-680:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2692:11-2692:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2257:11-2257:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:1262:9-1262:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:698:9-698:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2282:11-2282:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:717:9-717:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2742:10-2742:11)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2518:11-2518:48)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:735:9-735:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2304:11-2304:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2541:11-2541:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2352:7-2352:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2353:9-2353:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product22.cil.c:2568:9-2568:19)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
