./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_spec4_product25.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_spec4_product25.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_spec4_product25.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_spec4_product25.cil.c:144:3-165:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:201:3-226:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:286:5-306: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_spec4_product25.cil.c:51:1-65:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:73:1-118:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:119:1-174:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:175:1-234:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:237:1-339:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:340:1-385:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:386:1-431:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:526:1-534:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:712:1-726:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:912:1-926:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:948:1-963:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1040:1-1060:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1061:1-1076:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1079:1-1099:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1100:1-1115:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1118:1-1136:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1137:1-1152:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1155:1-1173:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1174:1-1189:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1423:1-1433:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1512:1-1523:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1524:1-1535:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1862:1-1871:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1907:1-1921:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1925:1-1950:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1951:1-1970:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1975:1-1998:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1999:1-2018:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2066:1-2090:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2100:1-2168:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2169:1-2237:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2431:1-2454:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2455:1-2474:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2963-2963)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2591-2591)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:547-547)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2769..2771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2769-2771)
  on lines 2773..2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2773-2775)
  on lines 2777..2778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2777-2778)
  on line 2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2815-2815)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2316..2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2316-2318)
  on lines 2320..2321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2320-2321)
  on lines 2326..2329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2326-2329)
  on lines 2331..2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2331-2333)
  on lines 2335..2337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2335-2337)
  on lines 2339..2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2339-2340)
  on lines 2345..2348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2345-2348)
  on lines 2350..2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2350-2352)
  on lines 2354..2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2354-2356)
  on lines 2358..2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2358-2359)
  on lines 2364..2365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2364-2365)
  on line 2369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2369-2369)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 2035..2036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2035-2036)
  on line 2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2043-2043)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2871..2872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2871-2872)
  on line 2887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2887-2887)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2926..2927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2926-2927)
  on line 2934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2934-2934)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2719..2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2719-2721)
  on lines 2723..2724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2723-2724)
  on lines 2728..2731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2728-2731)
  on lines 2733..2735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2733-2735)
  on lines 2737..2738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2737-2738)
  on lines 2742..2745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2742-2745)
  on lines 2747..2749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2747-2749)
  on lines 2751..2752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2751-2752)
  on lines 2756..2757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2756-2757)
  on line 2761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2761-2761)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2541..2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2541-2542)
  on line 2546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2546-2546)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2612..2614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2612-2614)
  on lines 2616..2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2616-2617)
  on lines 2621..2624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2621-2624)
  on lines 2626..2628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2626-2628)
  on lines 2630..2631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2630-2631)
  on lines 2635..2638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2635-2638)
  on lines 2640..2642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2640-2642)
  on lines 2644..2645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2644-2645)
  on lines 2649..2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2649-2650)
  on line 2654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2654-2654)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2491..2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2491-2492)
  on line 2499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2499-2499)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 975..976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:975-976)
  on line 982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:982-982)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 938..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:938-939)
  on line 945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:945-945)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1238..1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1238-1239)
  on line 1245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1245-1245)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1012..1013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1012-1013)
  on line 1019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1019-1019)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:765-765)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:774-774)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 791..792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:791-792)
  on line 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:799-799)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:523-523)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1201..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1201-1202)
  on line 1208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1208-1208)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1275..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1275-1276)
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1282-1282)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:756-756)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2383..2384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2383-2384)
  on lines 2391..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2391-2393)
  on lines 2395..2396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2395-2396)
  on lines 2398..2399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2398-2399)
  on lines 2406..2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2406-2408)
  on lines 2410..2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2410-2411)
  on lines 2413..2414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2413-2414)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2246..2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2246-2247)
  on lines 2249..2250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2249-2250)
  on lines 2257..2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2257-2259)
  on lines 2261..2262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2261-2262)
  on lines 2264..2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2264-2265)
  on lines 2272..2274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2272-2274)
  on lines 2276..2277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2276-2277)
  on lines 2279..2280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2279-2280)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2053..2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2053-2054)
  on lines 2056..2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2056-2057)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2895-2895)
  on lines 2900..2901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2900-2901)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2826..2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2826-2827)
  on lines 2837..2838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2837-2838)
  on lines 2848..2849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2848-2849)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2665..2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2665-2666)
  on lines 2676..2677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2676-2677)
  on lines 2687..2688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2687-2688)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:993-993)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1293-1293)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1219-1219)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1256-1256)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1030-1030)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1892-1892)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:875-875)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 574
  dead: 598 (402 in uncalled functions)
  total lines: 1172
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:865:7-865:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2834:11-2834:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2844:11-2844:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2845:13-2845:23)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1467:7-1467:10)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2870:7-2870:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2662:9-2662:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2034:11-2034:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:937:9-937:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2673:11-2673:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2242:7-2242:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2894:7-2894:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2243:9-2243:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2050:7-2050:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2683:11-2683:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.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_spec4_product25.cil.c:2684:13-2684:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1200:9-1200:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2714:7-2714:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2715:9-2715:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1218:9-1218:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:974:9-974:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2925:11-2925:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2490:11-2490:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1237:9-1237:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:992:9-992:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2307:7-2307:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2947:11-2947:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2512:11-2512:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1255:9-1255:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1011:9-1011:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2312:11-2312:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1274:9-1274:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1029:9-1029:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2537:11-2537:22)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2768:7-2768:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1292:9-1292:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2559:11-2559:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:790:9-790:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:1681:10-1681:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2607:7-2607:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2608:9-2608:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2376:7-2376:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2380:11-2380:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product25.cil.c:2823:9-2823: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
