./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_spec0_product16.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_spec0_product16.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_spec0_product16.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_spec0_product16.cil.c:813:3-834:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:870:3-895:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:955:5-975: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 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:221:1-231:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:310:1-321:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:322:1-333:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:495:1-503:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:742:1-787:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:788:1-843:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:844:1-903:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:906:1-1008:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1009:1-1054:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1055:1-1100:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1123:1-1137:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1141:1-1166:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1167:1-1186:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1191:1-1214:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1215:1-1234:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1238:1-1261:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1262:1-1281:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1282:1-1306:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1316:1-1384:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1385:1-1453:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1454:1-1509:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1519:1-1587:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1588:1-1643:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1647:1-1670:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1671:1-1690:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2189:1-2203:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2225:1-2240:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2317:1-2337:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2338:1-2353:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2356:1-2376:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2377:1-2392:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2469:1-2487:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2488:1-2503:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2506:1-2524:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2525:1-2540:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2543:1-2561:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2562:1-2577:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2599:1-2613:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2758:1-2772:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:404-404)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1807-1807)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:516-516)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1990..1991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1990-1991)
  on lines 2013..2015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2013-2015)
  on lines 2017..2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2017-2019)
  on lines 2021..2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2021-2022)
  on line 2031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2031-2031)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2087..2088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2087-2088)
  on line 2103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2103-2103)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2142..2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2142-2143)
  on line 2150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2150-2150)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1935..1937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1935-1937)
  on lines 1939..1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1939-1940)
  on lines 1944..1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1944-1947)
  on lines 1949..1951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1949-1951)
  on lines 1953..1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1953-1954)
  on lines 1958..1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1958-1961)
  on lines 1963..1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1963-1965)
  on lines 1967..1968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1967-1968)
  on lines 1972..1973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1972-1973)
  on line 1977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1977-1977)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1757..1758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1757-1758)
  on line 1762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1762-1762)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1828..1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1828-1830)
  on lines 1832..1833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1832-1833)
  on lines 1837..1840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1837-1840)
  on lines 1842..1844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1842-1844)
  on lines 1846..1847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1846-1847)
  on lines 1851..1854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1851-1854)
  on lines 1856..1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1856-1858)
  on lines 1860..1861 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1860-1861)
  on lines 1865..1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1865-1866)
  on line 1870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1870-1870)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1699..1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1699-1700)
  on line 1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1715-1715)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2441..2442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2441-2442)
  on line 2448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2448-2448)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2252..2253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2252-2253)
  on line 2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2259-2259)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2215..2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2215-2216)
  on line 2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2222-2222)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2289..2290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2289-2290)
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2296-2296)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2811-2811)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2820-2820)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2404..2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2404-2405)
  on line 2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2411-2411)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2837..2838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2837-2838)
  on line 2845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2845-2845)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:492-492)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:472-472)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2802-2802)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2111-2111)
  on lines 2116..2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2116-2117)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2042..2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2042-2043)
  on lines 2053..2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2053-2054)
  on lines 2064..2065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2064-2065)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1881..1882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1881-1882)
  on lines 1892..1893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1892-1893)
  on lines 1903..1904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1903-1904)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2459-2459)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2270-2270)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2422-2422)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2307-2307)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:94-94)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 489
  dead: 639 (518 in uncalled functions)
  total lines: 1128
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2251:9-2251:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2012:11-2012:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1823:7-1823:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1824:9-1824:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2269:9-2269:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2836:9-2836:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2288:9-2288:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2039:9-2039:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2306:9-2306:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2050:11-2050:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2060:11-2060:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2061:13-2061:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2086:7-2086:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1878:9-1878:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1889:11-1889:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2110:7-2110:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1899:11-1899:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2113:9-2113:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1900:13-1900:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1930:7-1930:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1931:9-1931:19)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1698:7-1698:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2403:9-2403:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2141:11-2141:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2421:9-2421:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2163:11-2163:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1728:11-1728:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2440:9-2440:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1753:11-1753:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2458:9-2458:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:559:10-559:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:2214:9-2214:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:265:7-265:10)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1989:11-1989:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product16.cil.c:1775:11-1775: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
