./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec9_product35.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec9_product35.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1764:3-1785:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1821:3-1846:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1906:5-1926: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:192:1-202:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:281:1-292:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:293:1-304:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:410:1-424:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:428:1-453:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:454:1-473:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:478:1-501:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:502:1-521:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:569:1-593:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:603:1-671:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:672:1-740:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1462:1-1471:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1619:1-1627:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1693:1-1738:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1739:1-1794:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1795:1-1854:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1857:1-1959:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1960:1-2005:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2006:1-2051:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2519:1-2533:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2724:1-2738:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2747:1-2761:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2783:1-2798:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2875:1-2895:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2896:1-2911:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2914:1-2934:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2935:1-2950:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2058-2058)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1094-1094)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1640-1640)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1318-1318)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 819..821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:819-821)
  on lines 823..824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:823-824)
  on lines 829..832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:829-832)
  on lines 834..836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:834-836)
  on lines 838..840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:838-840)
  on lines 842..843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:842-843)
  on lines 848..851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:848-851)
  on lines 853..855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:853-855)
  on lines 857..859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:857-859)
  on lines 861..862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:861-862)
  on lines 867..868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:867-868)
  on line 872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:872-872)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:546-546)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:955-955)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1390-1390)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1437-1437)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1222..1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1222-1224)
  on lines 1226..1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1226-1227)
  on lines 1231..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1231-1234)
  on lines 1236..1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1236-1238)
  on lines 1240..1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1240-1241)
  on lines 1245..1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1245-1248)
  on lines 1250..1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1250-1252)
  on lines 1254..1255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1254-1255)
  on lines 1259..1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1259-1260)
  on line 1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1264-1264)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1044..1045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1044-1045)
  on line 1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1049-1049)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1115..1117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1115-1117)
  on lines 1119..1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1119-1120)
  on lines 1124..1127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1124-1127)
  on lines 1129..1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1129-1131)
  on lines 1133..1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1133-1134)
  on lines 1138..1141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1138-1141)
  on lines 1143..1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1143-1145)
  on lines 1147..1148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1147-1148)
  on lines 1152..1153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1152-1153)
  on line 1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1157-1157)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1002-1002)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2999..3000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2999-3000)
  on line 3006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3006-3006)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2810..2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2810-2811)
  on line 2817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2817-2817)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2773..2774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2773-2774)
  on line 2780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2780-2780)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 3073..3074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3073-3074)
  on line 3080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3080-3080)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2847..2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2847-2848)
  on line 2854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2854-2854)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2572-2572)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2581-2581)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2962..2963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2962-2963)
  on line 2969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2969-2969)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2598..2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2598-2599)
  on line 2606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2606-2606)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1616-1616)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1596-1596)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 3036..3037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3036-3037)
  on line 3043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3043-3043)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 3110..3111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3110-3111)
  on line 3117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3117-3117)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2563-2563)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 886..887 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:886-887)
  on lines 894..896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:894-896)
  on lines 898..899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:898-899)
  on lines 901..902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:901-902)
  on lines 909..911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:909-911)
  on lines 913..914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:913-914)
  on lines 916..917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:916-917)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 749..750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:749-750)
  on lines 752..753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:752-753)
  on lines 760..762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:760-762)
  on lines 764..765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:764-765)
  on lines 767..768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:767-768)
  on lines 775..777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:775-777)
  on lines 779..780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:779-780)
  on lines 782..783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:782-783)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 556..557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:556-557)
  on lines 559..560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:559-560)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:963-963)
  on lines 968..969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:968-969)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1398-1398)
  on lines 1403..1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1403-1404)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1329..1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1329-1330)
  on lines 1340..1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1340-1341)
  on lines 1351..1352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1351-1352)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1168..1169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1168-1169)
  on lines 1179..1180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1179-1180)
  on lines 1190..1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1190-1191)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 3017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3017-3017)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2828-2828)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2980-2980)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3128-3128)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 3054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3054-3054)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 3091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3091-3091)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2865-2865)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1492-1492)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 696
  dead: 547 (355 in uncalled functions)
  total lines: 1243
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1217:7-1217:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1218:9-1218:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3109:9-3109:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2864:9-2864:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3127:9-3127:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2597:9-2597:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:810:7-810:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1450:11-1450:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1015:11-1015:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:815:11-815:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1040:11-1040:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2101:10-2101:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1062:11-1062:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2961:9-2961:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2979:9-2979:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1110:7-1110:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1111:9-1111:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:879:7-879:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2998:9-2998:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:883:11-883:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1326:9-1326:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3016:9-3016:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2772:9-2772:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1337:11-1337:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3035:9-3035:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1347:11-1347:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1348:13-1348:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3053:9-3053:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2809:9-2809:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:236:7-236:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1165:9-1165:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3072:9-3072:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1176:11-1176:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2827:9-2827:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:745:7-745:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1397:7-1397:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:746:9-746:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:553:7-553:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:962:7-962:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1186:11-1186:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1400:9-1400:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:1187:13-1187:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:3090:9-3090:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:965:9-965:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product35.cil.c:2846:9-2846: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
