./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_product21.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_product21.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_product21.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_product21.cil.c:2679:3-2700:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2736:3-2761:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2821:5-2841: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_spec6_product21.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:215:1-223:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:443:1-457:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:584:1-598:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:602:1-627:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:628:1-647:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:652:1-675:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:676:1-695:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:743:1-767:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:777:1-845:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:846:1-914:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1108:1-1131:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1132:1-1151:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1639:1-1648:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1999:1-2009:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2088:1-2099:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2100:1-2111:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2203:1-2217:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2239:1-2254:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2331:1-2351:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2352:1-2367:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2370:1-2390:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2391:1-2406:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2483:1-2501:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2502:1-2517:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2520:1-2538:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2539:1-2554:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2557:1-2575:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2576:1-2591:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2608:1-2653:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2654:1-2709:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2710:1-2769:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2772:1-2874:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2875:1-2920:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2921:1-2966:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2598-2598)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1268-1268)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:236-236)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1474..1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1474-1476)
  on lines 1478..1480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1478-1480)
  on lines 1482..1483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1482-1483)
  on line 1492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1492-1492)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 993..995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:993-995)
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:997-998)
  on lines 1003..1006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1003-1006)
  on lines 1008..1010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1008-1010)
  on lines 1012..1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1012-1014)
  on lines 1016..1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1016-1017)
  on lines 1022..1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1022-1025)
  on lines 1027..1029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1027-1029)
  on lines 1031..1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1031-1033)
  on lines 1035..1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1035-1036)
  on lines 1041..1042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1041-1042)
  on line 1046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1046-1046)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 712..713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:712-713)
  on line 720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:720-720)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1548..1549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1548-1549)
  on line 1564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1564-1564)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1603..1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1603-1604)
  on line 1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1611-1611)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1396..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1396-1398)
  on lines 1400..1401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1400-1401)
  on lines 1405..1408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1405-1408)
  on lines 1410..1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1410-1412)
  on lines 1414..1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1414-1415)
  on lines 1419..1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1419-1422)
  on lines 1424..1426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1424-1426)
  on lines 1428..1429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1428-1429)
  on lines 1433..1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1433-1434)
  on line 1438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1438-1438)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1218..1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1218-1219)
  on line 1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1223-1223)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1289..1291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1289-1291)
  on lines 1293..1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1293-1294)
  on lines 1298..1301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1298-1301)
  on lines 1303..1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1303-1305)
  on lines 1307..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1307-1308)
  on lines 1312..1315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1312-1315)
  on lines 1317..1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1317-1319)
  on lines 1321..1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1321-1322)
  on lines 1326..1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1326-1327)
  on line 1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1331-1331)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1160..1161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1160-1161)
  on line 1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1176-1176)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2455..2456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2455-2456)
  on line 2462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2462-2462)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2266..2267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2266-2267)
  on line 2273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2273-2273)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2229..2230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2229-2230)
  on line 2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2236-2236)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2303..2304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2303-2304)
  on line 2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2310-2310)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:496-496)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:505-505)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2418..2419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2418-2419)
  on line 2425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2425-2425)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:530-530)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:212-212)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:192-192)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:487-487)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1060..1061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1060-1061)
  on lines 1068..1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1068-1070)
  on lines 1072..1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1072-1073)
  on lines 1075..1076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1075-1076)
  on lines 1083..1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1083-1085)
  on lines 1087..1088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1087-1088)
  on lines 1090..1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1090-1091)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 923..924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:923-924)
  on lines 926..927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:926-927)
  on lines 934..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:934-936)
  on lines 938..939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:938-939)
  on lines 941..942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:941-942)
  on lines 949..951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:949-951)
  on lines 953..954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:953-954)
  on lines 956..957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:956-957)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 730..731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:730-731)
  on lines 733..734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:733-734)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1572-1572)
  on lines 1577..1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1577-1578)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1503..1504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1503-1504)
  on lines 1514..1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1514-1515)
  on lines 1525..1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1525-1526)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1342..1343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1342-1343)
  on lines 1353..1354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1353-1354)
  on lines 1364..1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1364-1365)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2473-2473)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2284-2284)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2436-2436)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2321-2321)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1669-1669)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 568
  dead: 606 (416 in uncalled functions)
  total lines: 1174
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2265:9-2265:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1236:11-1236:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2283:9-2283:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1722:10-1722:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2302:9-2302:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1473:11-1473:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1284:7-1284:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1285:9-1285:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1053:7-1053:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2320:9-2320:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1057:11-1057:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2043:7-2043:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1500:9-1500:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1511:11-1511:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1521:11-1521:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1522:13-1522:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1547:7-1547:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1339:9-1339:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:711:11-711:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1350:11-1350:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:919:7-919:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:920:9-920:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:727:7-727:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1571:7-1571:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2417:9-2417:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1360:11-1360:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1574:9-1574:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1361:13-1361:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1391:7-1391:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1159:7-1159:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1392:9-1392:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2435:9-2435:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1602:11-1602:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2454:9-2454:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:984:7-984:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2472:9-2472:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1624:11-1624:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:2228:9-2228:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1189:11-1189:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:989:11-989:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product21.cil.c:1214:11-1214:22)
[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
