./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_spec6_product31.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_spec6_product31.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_spec6_product31.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_spec6_product31.cil.c:1392:3-1413:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1449:3-1474:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1534:5-1554: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_spec6_product31.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:201:1-209:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:255:1-269:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:273:1-298:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:299:1-318:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:323:1-346:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:347:1-366:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:370:1-393:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:394:1-413:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:414:1-438:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:448:1-516:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:517:1-585:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:586:1-641:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:651:1-719:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:720:1-775:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:779:1-802:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:803:1-822:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1321:1-1366:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1367:1-1422:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1423:1-1482:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1485:1-1587:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1588:1-1633:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1634:1-1679:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2013:1-2023:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2102:1-2113:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2114:1-2125:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2373:1-2387:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2608:1-2622:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2644:1-2659:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2736:1-2756:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2757:1-2772:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2775:1-2795:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2796:1-2811:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2999:1-3008:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1311-1311)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:939-939)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:222-222)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1122..1123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1122-1123)
  on line 1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1163-1163)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1219..1220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1219-1220)
  on line 1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1235-1235)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1274..1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1274-1275)
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1282-1282)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1067..1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1067-1069)
  on lines 1071..1072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1071-1072)
  on lines 1076..1079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1076-1079)
  on lines 1081..1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1081-1083)
  on lines 1085..1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1085-1086)
  on lines 1090..1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1090-1093)
  on lines 1095..1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1095-1097)
  on lines 1099..1100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1099-1100)
  on lines 1104..1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1104-1105)
  on line 1109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1109-1109)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 889..890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:889-890)
  on line 894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:894-894)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 960..962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:960-962)
  on lines 964..965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:964-965)
  on lines 969..972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:969-972)
  on lines 974..976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:974-976)
  on lines 978..979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:978-979)
  on lines 983..986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:983-986)
  on lines 988..990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:988-990)
  on lines 992..993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:992-993)
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:997-998)
  on line 1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1002-1002)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:847-847)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2860..2861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2860-2861)
  on line 2867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2867-2867)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2671..2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2671-2672)
  on line 2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2678-2678)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2634..2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2634-2635)
  on line 2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2641-2641)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2934..2935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2934-2935)
  on line 2941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2941-2941)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2708..2709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2708-2709)
  on line 2715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2715-2715)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2426-2426)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2435-2435)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2823..2824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2823-2824)
  on line 2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2830-2830)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2460-2460)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:198-198)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:178-178)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2897..2898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2897-2898)
  on line 2904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2904-2904)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2971..2972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2971-2972)
  on line 2978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2978-2978)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2417-2417)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1243-1243)
  on lines 1248..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1248-1249)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1174..1175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1174-1175)
  on lines 1185..1186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1185-1186)
  on lines 1196..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1196-1197)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1013..1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1013-1014)
  on lines 1024..1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1024-1025)
  on lines 1035..1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1035-1036)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2878-2878)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2689-2689)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2841-2841)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2989-2989)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2915-2915)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2952-2952)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2726-2726)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:3029-3029)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 598
  dead: 597 (476 in uncalled functions)
  total lines: 1195
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1121:11-1121:48)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2822:9-2822:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:907:11-907:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2840:9-2840:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2859:9-2859:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:955:7-955:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:956:9-956:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2877:9-2877:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2633:9-2633:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1729:10-1729:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1171:9-1171:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2896:9-2896:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1182:11-1182:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1192:11-1192:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2914:9-2914:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1193:13-1193:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2670:9-2670:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2057:7-2057:10)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1218:7-1218:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2933:9-2933:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1010:9-1010:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2688:9-2688:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1021:11-1021:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2951:9-2951:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2707:9-2707:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1242:7-1242:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1031:11-1031:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1032:13-1032:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1245:9-1245:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2970:9-2970:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2725:9-2725:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1062:7-1062:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1063:9-1063:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:2988:9-2988:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1273:11-1273:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:1295:11-1295:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:860:11-860:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product31.cil.c:885:11-885:22)
[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
