./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_spec9_product33.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_spec9_product33.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_spec9_product33.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_spec9_product33.cil.c:1265:3-1286:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1322:3-1347:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1407:5-1427: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:184:1-192:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:336:1-346:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:425:1-436:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:437:1-448:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:798:1-812:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:834:1-849:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:926:1-946:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:947:1-962:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:965:1-985:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:986:1-1001:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1194:1-1239:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1240:1-1295:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1296:1-1355:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1358:1-1460:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1461:1-1506:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1507:1-1552:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1564:1-1578:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1778:1-1792:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1989:1-2003:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2007:1-2032:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2033:1-2052:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2057:1-2080:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2081:1-2100:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2104:1-2127:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2128:1-2147:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2148:1-2172:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2182:1-2250:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2251:1-2319:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2320:1-2375:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2385:1-2453:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2454:1-2509:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:3041:1-3050:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1559-1559)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2673-2673)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:205-205)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2897-2897)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2534-2534)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2969-2969)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 3008..3009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:3008-3009)
  on line 3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:3016-3016)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2801..2803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2801-2803)
  on lines 2805..2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2805-2806)
  on lines 2810..2813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2810-2813)
  on lines 2815..2817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2815-2817)
  on lines 2819..2820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2819-2820)
  on lines 2824..2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2824-2827)
  on lines 2829..2831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2829-2831)
  on lines 2833..2834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2833-2834)
  on lines 2838..2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2838-2839)
  on line 2843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2843-2843)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2623..2624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2623-2624)
  on line 2628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2628-2628)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2694..2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2694-2696)
  on lines 2698..2699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2698-2699)
  on lines 2703..2706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2703-2706)
  on lines 2708..2710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2708-2710)
  on lines 2712..2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2712-2713)
  on lines 2717..2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2717-2720)
  on lines 2722..2724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2722-2724)
  on lines 2726..2727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2726-2727)
  on lines 2731..2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2731-2732)
  on line 2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2736-2736)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2581-2581)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1050..1051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1050-1051)
  on line 1057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1057-1057)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 861..862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:861-862)
  on line 868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:868-868)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 824..825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:824-825)
  on line 831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:831-831)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1124..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1124-1125)
  on line 1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1131-1131)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 898..899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:898-899)
  on line 905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:905-905)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1831-1831)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1840-1840)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1013..1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1013-1014)
  on line 1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1020-1020)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1857..1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1857-1858)
  on line 1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1865-1865)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:181-181)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:161-161)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1087..1088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1087-1088)
  on line 1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1094-1094)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1161..1162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1161-1162)
  on line 1168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1168-1168)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1822-1822)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2542-2542)
  on lines 2547..2548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2547-2548)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2977-2977)
  on lines 2982..2983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2982-2983)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2908..2909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2908-2909)
  on lines 2919..2920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2919-2920)
  on lines 2930..2931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2930-2931)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2747..2748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2747-2748)
  on lines 2758..2759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2758-2759)
  on lines 2769..2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2769-2770)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1068-1068)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:879-879)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1031-1031)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1179-1179)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1105-1105)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1142-1142)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:916-916)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:3071-3071)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 631
  dead: 580 (457 in uncalled functions)
  total lines: 1211
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2641:11-2641:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1104:9-1104:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:860:9-860:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1123:9-1123:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:878:9-878:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2689:7-2689:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2690:9-2690:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1141:9-1141:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:897:9-897:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1160:9-1160:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2905:9-2905:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:915:9-915:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2916:11-2916:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:380:7-380:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1178:9-1178:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2926:11-2926:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2927:13-2927:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2744:9-2744:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2755:11-2755:21)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1856:9-1856:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2976:7-2976:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2541:7-2541:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2765:11-2765:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2979:9-2979:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2766:13-2766:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2544:9-2544:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2796:7-2796:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2797:9-2797:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1012:9-1012:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:3007:11-3007:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1030:9-1030:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:3029:11-3029:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1049:9-1049:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2594:11-2594:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1067:9-1067:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:563:10-563:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:823:9-823:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:2619:11-2619:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product33.cil.c:1086:9-1086:20)
[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
