./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_product24.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_product24.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_product24.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_product24.cil.c:1511:3-1532:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1568:3-1593:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1653:5-1673: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_spec4_product24.cil.c:307:1-321:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:325:1-350:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:351:1-370:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:375:1-398:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:399:1-418:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:422:1-445:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:446:1-465:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:466:1-490:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:500:1-568:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:569:1-637:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:638:1-693:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:703:1-771:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:772:1-827:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1360:1-1374:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1391:1-1400:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1440:1-1485:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1486:1-1541:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1542:1-1601:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1604:1-1706:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1707:1-1752:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1753:1-1798:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1822:1-1836:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1858:1-1873:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1950:1-1970:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1971:1-1986:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1989:1-2009:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2010:1-2025:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2028:1-2046:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2047:1-2062:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2065:1-2083:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2084:1-2099:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2316:1-2326:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2405:1-2416:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2417:1-2428:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2605:1-2613:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2753:1-2767:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1430-1430)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:991-991)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2626-2626)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1215-1215)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:852-852)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1287-1287)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1326..1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1326-1327)
  on line 1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.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_spec4_product24.cil.c:1119-1121)
  on lines 1123..1124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1123-1124)
  on lines 1128..1131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1128-1131)
  on lines 1133..1135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1133-1135)
  on lines 1137..1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1137-1138)
  on lines 1142..1145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1142-1145)
  on lines 1147..1149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1147-1149)
  on lines 1151..1152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1151-1152)
  on lines 1156..1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1156-1157)
  on line 1161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.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_spec4_product24.cil.c:941-942)
  on line 946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.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_spec4_product24.cil.c:1012-1014)
  on lines 1016..1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1016-1017)
  on lines 1021..1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1021-1024)
  on lines 1026..1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1026-1028)
  on lines 1030..1031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1030-1031)
  on lines 1035..1038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1035-1038)
  on lines 1040..1042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1040-1042)
  on lines 1044..1045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1044-1045)
  on lines 1049..1050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1049-1050)
  on line 1054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1054-1054)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 891..892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:891-892)
  on line 899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:899-899)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1885..1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1885-1886)
  on line 1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1892-1892)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1848..1849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1848-1849)
  on line 1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1855-1855)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2148..2149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2148-2149)
  on line 2155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2155-2155)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1922..1923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1922-1923)
  on line 1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1929-1929)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2806-2806)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2815-2815)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2832..2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2832-2833)
  on line 2840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2840-2840)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2602-2602)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2111..2112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2111-2112)
  on line 2118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2118-2118)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2185..2186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2185-2186)
  on line 2192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2192-2192)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2797-2797)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:860-860)
  on lines 865..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:865-866)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1295-1295)
  on lines 1300..1301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1300-1301)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1226..1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1226-1227)
  on lines 1237..1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1237-1238)
  on lines 1248..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.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_spec4_product24.cil.c:1065-1066)
  on lines 1076..1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1076-1077)
  on lines 1087..1088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1087-1088)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1903-1903)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2203 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2203-2203)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2129-2129)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2166-2166)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1940-1940)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1421-1421)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2924-2924)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 557
  dead: 602 (485 in uncalled functions)
  total lines: 1159
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1114:7-1114:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2165:9-2165:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1115:9-1115:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1921:9-1921:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1325:11-1325:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:890:11-890:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2184:9-2184:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2831:9-2831:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1939:9-1939:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2202:9-2202:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.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_spec4_product24.cil.c:912:11-912:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:937:11-937:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2914:7-2914:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:959:11-959:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.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_spec4_product24.cil.c:1008:9-1008:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:98:10-98:11)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2360:7-2360:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1223:9-1223:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1234:11-1234:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1847:9-1847:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1244:11-1244:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1245:13-1245:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2110:9-2110:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1062:9-1062:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2128:9-2128:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1884:9-1884:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1073:11-1073:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:2147:9-2147:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1294:7-1294:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.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_spec4_product24.cil.c:1083:11-1083:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1297:9-1297:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.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_spec4_product24.cil.c:862:9-862:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product24.cil.c:1902:9-1902: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
