./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_product20.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_product20.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_product20.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_product20.cil.c:1484:3-1505:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1541:3-1566:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1626:5-1646: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 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:356:1-370:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:374:1-399:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:400:1-419:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:424:1-447:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:448:1-467:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:515:1-539:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:549:1-617:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:618:1-686:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1315:1-1338:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1339:1-1358:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1413:1-1458:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1459:1-1514:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1515:1-1574:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1577:1-1679:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1680:1-1725:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1726:1-1771:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1795:1-1809:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1812:1-1830:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1831:1-1846:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1923:1-1943:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1944:1-1959:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1962:1-1982:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1983:1-1998:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2075:1-2093:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2094:1-2109:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2112:1-2130:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2131:1-2146:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2149:1-2167:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2168:1-2183:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2338:1-2348:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2427:1-2438:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2439:1-2450:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2724:1-2738:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2848:1-2862:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2867:1-2894:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2895:1-2913:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2914:1-2922:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2923:1-2942:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2943:1-2951:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2534-2534)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1040-1040)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2964-2964)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1264-1264)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 765..767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:765-767)
  on lines 769..770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:769-770)
  on lines 775..778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:775-778)
  on lines 780..782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:780-782)
  on lines 784..786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:784-786)
  on lines 788..789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:788-789)
  on lines 794..797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:794-797)
  on lines 799..801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:799-801)
  on lines 803..805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:803-805)
  on lines 807..808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:807-808)
  on lines 813..814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:813-814)
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:818-818)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:492-492)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:901-901)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1383-1383)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1168..1170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1168-1170)
  on lines 1172..1173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1172-1173)
  on lines 1177..1180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1177-1180)
  on lines 1182..1184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1182-1184)
  on lines 1186..1187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1186-1187)
  on lines 1191..1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1191-1194)
  on lines 1196..1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1196-1198)
  on lines 1200..1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1200-1201)
  on lines 1205..1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1205-1206)
  on line 1210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1210-1210)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 990..991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:990-991)
  on line 995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:995-995)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1061..1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1061-1063)
  on lines 1065..1066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1065-1066)
  on lines 1070..1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1070-1073)
  on lines 1075..1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1075-1077)
  on lines 1079..1080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1079-1080)
  on lines 1084..1087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1084-1087)
  on lines 1089..1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1089-1091)
  on lines 1093..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1093-1094)
  on lines 1098..1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1098-1099)
  on line 1103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1103-1103)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:948-948)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2047..2048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2047-2048)
  on line 2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2054-2054)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1858..1859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1858-1859)
  on line 1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1865-1865)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1895..1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1895-1896)
  on line 1902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1902-1902)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2777-2777)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2786-2786)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2010..2011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2010-2011)
  on line 2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2017-2017)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2811-2811)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2768-2768)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 832..833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:832-833)
  on lines 840..842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:840-842)
  on lines 844..845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:844-845)
  on lines 847..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:847-848)
  on lines 855..857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:855-857)
  on lines 859..860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:859-860)
  on lines 862..863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:862-863)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 695..696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:695-696)
  on lines 698..699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:698-699)
  on lines 706..708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:706-708)
  on lines 710..711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:710-711)
  on lines 713..714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:713-714)
  on lines 721..723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:721-723)
  on lines 725..726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:725-726)
  on lines 728..729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:728-729)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 502..503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:502-503)
  on lines 505..506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:505-506)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:909-909)
  on lines 914..915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:914-915)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1275..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1275-1276)
  on lines 1286..1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1286-1287)
  on lines 1297..1298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1297-1298)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1114..1115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1114-1115)
  on lines 1125..1126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1125-1126)
  on lines 1136..1137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1136-1137)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2065-2065)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1876-1876)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2028-2028)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1913-1913)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:94-94)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 544
  dead: 625 (456 in uncalled functions)
  total lines: 1169
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1122:11-1122:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:691:7-691:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:692:9-692:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:499:7-499:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:908:7-908:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1912:9-1912:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1132:11-1132:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1133:13-1133:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:911:9-911:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1163:7-1163:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1164:9-1164:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:756:7-756:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1396:11-1396:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:961:11-961:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:761:11-761:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:986:11-986:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2009:9-2009:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1008:11-1008:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2027:9-2027:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2046:9-2046:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1056:7-1056:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1057:9-1057:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:147:10-147:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2064:9-2064:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:825:7-825:18)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:2382:7-2382:10)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:829:11-829:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1272:9-1272:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1283:11-1283:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1857:9-1857:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1293:11-1293:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1294:13-1294:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1875:9-1875:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1111:9-1111:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product20.cil.c:1894:9-1894: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
