./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_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_spec4_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_spec4_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_spec4_product35.cil.c:2065:3-2086:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2122:3-2147:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2207:5-2227: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_product35.cil.c:60:1-74:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:98:1-112:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:134:1-149:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:226:1-246:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:247:1-262:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:265:1-285:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:286:1-301:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:503:1-512:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:566:1-580:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:584:1-609:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:610:1-629:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:634:1-657:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:658:1-677:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:725:1-749:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:759:1-827:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:828:1-896:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1730:1-1738:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1994:1-2039:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2040:1-2095:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2096:1-2155:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2158:1-2260:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2261:1-2306:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2307:1-2352:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2458:1-2468:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2547:1-2558:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2559:1-2570:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2889:1-2903:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:54-54)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1250-1250)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1751-1751)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1474-1474)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 975..977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:975-977)
  on lines 979..980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:979-980)
  on lines 985..988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:985-988)
  on lines 990..992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:990-992)
  on lines 994..996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:994-996)
  on lines 998..999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:998-999)
  on lines 1004..1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1004-1007)
  on lines 1009..1011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1009-1011)
  on lines 1013..1015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1013-1015)
  on lines 1017..1018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1017-1018)
  on lines 1023..1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1023-1024)
  on line 1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1028-1028)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:702-702)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1111-1111)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1546-1546)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1593-1593)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1378..1380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1378-1380)
  on lines 1382..1383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1382-1383)
  on lines 1387..1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1387-1390)
  on lines 1392..1394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1392-1394)
  on lines 1396..1397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1396-1397)
  on lines 1401..1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1401-1404)
  on lines 1406..1408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1406-1408)
  on lines 1410..1411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1410-1411)
  on lines 1415..1416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1415-1416)
  on line 1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1420-1420)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1200..1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1200-1201)
  on line 1205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1205-1205)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1271..1273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1271-1273)
  on lines 1275..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1275-1276)
  on lines 1280..1283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1280-1283)
  on lines 1285..1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1285-1287)
  on lines 1289..1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1289-1290)
  on lines 1294..1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1294-1297)
  on lines 1299..1301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1299-1301)
  on lines 1303..1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1303-1304)
  on lines 1308..1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1308-1309)
  on line 1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1313-1313)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1158-1158)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 350..351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:350-351)
  on line 357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:357-357)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 161..162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:161-162)
  on line 168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:168-168)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 124..125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:124-125)
  on line 131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:131-131)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 424..425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:424-425)
  on line 431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:431-431)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 198..199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:198-199)
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:205-205)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2942-2942)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2951-2951)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 313..314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:313-314)
  on line 320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:320-320)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2968..2969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2968-2969)
  on line 2976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2976-2976)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1727-1727)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1707-1707)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 387..388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:387-388)
  on line 394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:394-394)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 461..462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:461-462)
  on line 468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:468-468)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2933-2933)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1042..1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1042-1043)
  on lines 1050..1052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1050-1052)
  on lines 1054..1055 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1054-1055)
  on lines 1057..1058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1057-1058)
  on lines 1065..1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1065-1067)
  on lines 1069..1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1069-1070)
  on lines 1072..1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1072-1073)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 905..906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:905-906)
  on lines 908..909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:908-909)
  on lines 916..918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:916-918)
  on lines 920..921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:920-921)
  on lines 923..924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:923-924)
  on lines 931..933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:931-933)
  on lines 935..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:935-936)
  on lines 938..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:938-939)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 712..713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:712-713)
  on lines 715..716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:715-716)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1119-1119)
  on lines 1124..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1124-1125)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1554-1554)
  on lines 1559..1560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1559-1560)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1485..1486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1485-1486)
  on lines 1496..1497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1496-1497)
  on lines 1507..1508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1507-1508)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1324..1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1324-1325)
  on lines 1335..1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1335-1336)
  on lines 1346..1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1346-1347)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:368-368)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:179-179)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:331-331)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:479-479)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:405-405)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:442-442)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:216-216)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:533-533)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 688
  dead: 547 (355 in uncalled functions)
  total lines: 1235
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:215:9-215:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:966:7-966:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1606:11-1606:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1171:11-1171:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:478:9-478:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:971:11-971:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2502:7-2502:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1196:11-1196:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1218:11-1218:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:312:9-312:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1266:7-1266:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1267:9-1267:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1035:7-1035:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1039:11-1039:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:330:9-330:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1482:9-1482:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:349:9-349:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1493:11-1493:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1503:11-1503:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:2967:9-2967:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1504:13-1504:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:367:9-367:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:123:9-123:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:386:9-386:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1805:10-1805:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1321:9-1321:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1332:11-1332:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:404:9-404:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:160:9-160:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:901:7-901:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1553:7-1553:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:902:9-902:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:709:7-709:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1118:7-1118:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1342:11-1342:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1556:9-1556:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1343:13-1343:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1121:9-1121:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:423:9-423:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:178:9-178:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1373:7-1373:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:1374:9-1374:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:441:9-441:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:197:9-197:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product35.cil.c:460:9-460: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
