./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_product33.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_product33.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_product33.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_product33.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:268:5-288: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:563:1-573:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:652:1-663:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:664:1-675:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:971:1-980:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1219:1-1233:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1430:1-1444:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1448:1-1473:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1474:1-1493:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1498:1-1521:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1522:1-1541:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1545:1-1568:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1569:1-1588:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1589:1-1613:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1623:1-1691:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1692:1-1760:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1761:1-1816:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1826:1-1894:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1895:1-1950:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2593:1-2601:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2619:1-2633:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2669:1-2683:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2705:1-2720:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2797:1-2817:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2818:1-2833:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2836:1-2856:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2857:1-2872:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:420-420)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2114-2114)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2614-2614)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2338-2338)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1975-1975)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2410-2410)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2449..2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2449-2450)
  on line 2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2457-2457)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2242..2244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2242-2244)
  on lines 2246..2247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2246-2247)
  on lines 2251..2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2251-2254)
  on lines 2256..2258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2256-2258)
  on lines 2260..2261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2260-2261)
  on lines 2265..2268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2265-2268)
  on lines 2270..2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2270-2272)
  on lines 2274..2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2274-2275)
  on lines 2279..2280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2279-2280)
  on line 2284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2284-2284)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2064..2065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2064-2065)
  on line 2069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2069-2069)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2135..2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2135-2137)
  on lines 2139..2140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2139-2140)
  on lines 2144..2147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2144-2147)
  on lines 2149..2151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2149-2151)
  on lines 2153..2154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2153-2154)
  on lines 2158..2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2158-2161)
  on lines 2163..2165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2163-2165)
  on lines 2167..2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2167-2168)
  on lines 2172..2173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2172-2173)
  on line 2177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2177-2177)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2022-2022)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2921..2922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2921-2922)
  on line 2928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2928-2928)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2732..2733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2732-2733)
  on line 2739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2739-2739)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2695..2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2695-2696)
  on line 2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2702-2702)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2995..2996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2995-2996)
  on line 3002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:3002-3002)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2769..2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2769-2770)
  on line 2776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2776-2776)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1272-1272)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1281-1281)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2884..2885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2884-2885)
  on line 2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2891-2891)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1298..1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1298-1299)
  on line 1306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1306-1306)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2590-2590)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2570-2570)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2958..2959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2958-2959)
  on line 2965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2965-2965)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 3032..3033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:3032-3033)
  on line 3039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:3039-3039)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1263-1263)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1983-1983)
  on lines 1988..1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1988-1989)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2418-2418)
  on lines 2423..2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2423-2424)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2349..2350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2349-2350)
  on lines 2360..2361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2360-2361)
  on lines 2371..2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2371-2372)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2188..2189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2188-2189)
  on lines 2199..2200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2199-2200)
  on lines 2210..2211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2210-2211)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2939-2939)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2750-2750)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2902-2902)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:3050-3050)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2976-2976)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 3013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:3013-3013)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2787-2787)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1001-1001)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 623
  dead: 580 (457 in uncalled functions)
  total lines: 1203
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2130:7-2130:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2131:9-2131:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:607:7-607:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2346:9-2346:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2883:9-2883:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2357:11-2357:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2367:11-2367:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2368:13-2368:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2901:9-2901:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2920:9-2920:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2185:9-2185:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2196:11-2196:21)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1297:9-1297:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2938:9-2938:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2694:9-2694:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2417:7-2417:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1982:7-1982:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2206:11-2206:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2420:9-2420:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2207:13-2207:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:1985:9-1985:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2957:9-2957:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2237:7-2237:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2238:9-2238:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2975:9-2975:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2448:11-2448:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2731:9-2731:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2994:9-2994:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2749:9-2749:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2470:11-2470:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2035:11-2035:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:790:10-790:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:3012:9-3012:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2768:9-2768:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:3031:9-3031:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2060:11-2060:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2786:9-2786:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:3049:9-3049:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product33.cil.c:2082:11-2082: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
