./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_product32.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_product32.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_product32.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_product32.cil.c:1874:3-1895:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1931:3-1956:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2016:5-2036: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 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:307:1-321:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:325:1-350:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:351:1-370:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:375:1-398:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:399:1-418:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:466:1-490:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:500:1-568:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:569:1-637:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1266:1-1289:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1290:1-1309:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1380:1-1394:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1397:1-1415:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1416:1-1431:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1508:1-1528:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1529:1-1544:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1547:1-1567:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1568:1-1583:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1734:1-1752:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1781:1-1795:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1803:1-1848:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1849:1-1904:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1905:1-1964:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1967:1-2069:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2070:1-2115:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2116:1-2161:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2395:1-2409:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2591:1-2600:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2768:1-2778:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2857:1-2868:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2869:1-2880:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2961:1-2988:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2989:1-3007:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:3008:1-3026:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:3027:1-3040:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:3070:1-3078:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1775-1775)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:991-991)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:3091-3091)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1215-1215)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 716..718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:716-718)
  on lines 720..721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:720-721)
  on lines 726..729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:726-729)
  on lines 731..733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:731-733)
  on lines 735..737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:735-737)
  on lines 739..740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:739-740)
  on lines 745..748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:745-748)
  on lines 750..752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:750-752)
  on lines 754..756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:754-756)
  on lines 758..759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:758-759)
  on lines 764..765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:764-765)
  on line 769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:769-769)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:443-443)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:852-852)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1334-1334)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1119..1121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1119-1121)
  on lines 1123..1124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1123-1124)
  on lines 1128..1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1128-1131)
  on lines 1133..1135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1133-1135)
  on lines 1137..1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1137-1138)
  on lines 1142..1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1142-1145)
  on lines 1147..1149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1147-1149)
  on lines 1151..1152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1151-1152)
  on lines 1156..1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1156-1157)
  on line 1161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1161-1161)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 941..942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:941-942)
  on line 946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:946-946)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1012..1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1012-1014)
  on lines 1016..1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1016-1017)
  on lines 1021..1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1021-1024)
  on lines 1026..1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1026-1028)
  on lines 1030..1031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1030-1031)
  on lines 1035..1038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1035-1038)
  on lines 1040..1042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1040-1042)
  on lines 1044..1045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1044-1045)
  on lines 1049..1050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1049-1050)
  on line 1054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1054-1054)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:899-899)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1632..1633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1632-1633)
  on line 1639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1639-1639)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1443..1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1443-1444)
  on line 1450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1450-1450)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1706..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1706-1707)
  on line 1713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1713-1713)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1480..1481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1480-1481)
  on line 1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1487-1487)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2448-2448)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2457-2457)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1595..1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1595-1596)
  on line 1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1602-1602)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2482-2482)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 3067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:3067-3067)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 3047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:3047-3047)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1669..1670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1669-1670)
  on line 1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1676-1676)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2439-2439)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 783..784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:783-784)
  on lines 791..793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:791-793)
  on lines 795..796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:795-796)
  on lines 798..799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:798-799)
  on lines 806..808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:806-808)
  on lines 810..811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:810-811)
  on lines 813..814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:813-814)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 646..647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:646-647)
  on lines 649..650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:649-650)
  on lines 657..659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:657-659)
  on lines 661..662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:661-662)
  on lines 664..665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:664-665)
  on lines 672..674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:672-674)
  on lines 676..677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:676-677)
  on lines 679..680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:679-680)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 453..454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:453-454)
  on lines 456..457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:456-457)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:860-860)
  on lines 865..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:865-866)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1226..1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1226-1227)
  on lines 1237..1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1237-1238)
  on lines 1248..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1248-1249)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1065..1066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1065-1066)
  on lines 1076..1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1076-1077)
  on lines 1087..1088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1087-1088)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1650-1650)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1461-1461)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1613-1613)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1761-1761)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1687-1687)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1724-1724)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1498-1498)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2621-2621)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 615
  dead: 606 (426 in uncalled functions)
  total lines: 1221
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1114:7-1114:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1115:9-1115:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:2812:7-2812:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1594:9-1594:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1612:9-1612:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:707:7-707:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1347:11-1347:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:912:11-912:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:712:11-712:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1631:9-1631:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:937:11-937:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1649:9-1649:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1668:9-1668:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:959:11-959:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1686:9-1686:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1442:9-1442:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1705:9-1705:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1007:7-1007:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1008:9-1008:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1460:9-1460: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_product32.cil.c:98:10-98:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:776:7-776:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1723:9-1723:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:780:11-780:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1479:9-1479:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1223:9-1223:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1497:9-1497:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1234:11-1234:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1244:11-1244:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1760:9-1760:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1245:13-1245:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1062:9-1062:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1073:11-1073:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:642:7-642:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:643:9-643:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:450:7-450:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:859:7-859:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1083:11-1083:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:1084:13-1084:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product32.cil.c:862:9-862: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
