./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_spec8_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_spec8_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_spec8_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_spec8_product33.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:268:5-288: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:417:1-431:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:471:1-485:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:489:1-514:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:515:1-534:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:539:1-562:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:563:1-582:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:586:1-609:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:610:1-629:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:630:1-654:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:664:1-732:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:733:1-801:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:802:1-857:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:867:1-935:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:936:1-991:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1656:1-1664:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2059:1-2069:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2148:1-2159:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2160:1-2171:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2248:1-2257:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2479:1-2493:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2683:1-2697:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2719:1-2734:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2811:1-2831:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2832:1-2847:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2850:1-2870:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2871:1-2886:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:438-438)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1155-1155)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1677-1677)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1379-1379)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1016-1016)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1451-1451)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1490..1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1490-1491)
  on line 1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1498-1498)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1283..1285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1283-1285)
  on lines 1287..1288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1287-1288)
  on lines 1292..1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1292-1295)
  on lines 1297..1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1297-1299)
  on lines 1301..1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1301-1302)
  on lines 1306..1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1306-1309)
  on lines 1311..1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1311-1313)
  on lines 1315..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1315-1316)
  on lines 1320..1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1320-1321)
  on line 1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1325-1325)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1105..1106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1105-1106)
  on line 1110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1110-1110)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1176..1178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1176-1178)
  on lines 1180..1181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1180-1181)
  on lines 1185..1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1185-1188)
  on lines 1190..1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1190-1192)
  on lines 1194..1195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1194-1195)
  on lines 1199..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1199-1202)
  on lines 1204..1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1204-1206)
  on lines 1208..1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1208-1209)
  on lines 1213..1214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1213-1214)
  on line 1218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1218-1218)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1063-1063)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2935..2936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2935-2936)
  on line 2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2942-2942)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2746..2747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2746-2747)
  on line 2753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2753-2753)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2709..2710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2709-2710)
  on line 2716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2716-2716)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 3009..3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3009-3010)
  on line 3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3016-3016)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2783..2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2783-2784)
  on line 2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2790-2790)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2532-2532)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2541-2541)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2898..2899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2898-2899)
  on line 2905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2905-2905)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2558..2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2558-2559)
  on line 2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2566-2566)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1653-1653)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1633-1633)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2972..2973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2972-2973)
  on line 2979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2979-2979)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 3046..3047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3046-3047)
  on line 3053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3053-3053)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2523-2523)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1024-1024)
  on lines 1029..1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1029-1030)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1459-1459)
  on lines 1464..1465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1464-1465)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1390..1391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1390-1391)
  on lines 1401..1402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1401-1402)
  on lines 1412..1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1412-1413)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1229..1230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1229-1230)
  on lines 1240..1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1240-1241)
  on lines 1251..1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1251-1252)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2953-2953)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2764-2764)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2916-2916)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3064-3064)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2990-2990)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 3027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3027-3027)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2801-2801)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2278-2278)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 631
  dead: 580 (457 in uncalled functions)
  total lines: 1211
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1387:9-1387:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1398:11-1398:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1408:11-1408:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1409:13-1409:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2897:9-2897:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1226:9-1226:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2915:9-2915:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1237:11-1237:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1458:7-1458:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1023:7-1023:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2934:9-2934:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1247:11-1247:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1461:9-1461:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1248:13-1248:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1773:10-1773:11)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1026:9-1026:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1278:7-1278:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1279:9-1279:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2952:9-2952:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2708:9-2708:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1489:11-1489:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2971:9-2971:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2103:7-2103:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2989:9-2989:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1511:11-1511:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2745:9-2745:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1076:11-1076:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3008:9-3008:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2763:9-2763:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1101:11-1101:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3026:9-3026:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2782:9-2782:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3045:9-3045:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1123:11-1123:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2800:9-2800:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:3063:9-3063:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1171:7-1171:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:2557:9-2557:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product33.cil.c:1172:9-1172: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
