./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_product15.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_product15.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_product15.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_product15.cil.c:2618:3-2639:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2675:3-2700:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2760:5-2780: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 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:467:1-481:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:584:1-598:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:614:1-628:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:631:1-649:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:650:1-665:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:742:1-762:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:763:1-778:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:781:1-801:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:802:1-817:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:894:1-912:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:913:1-928:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:931:1-949:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:950:1-965:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:968:1-986:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:987:1-1002:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1007:1-1034:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1035:1-1053:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1054:1-1062:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1063:1-1082:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1083:1-1091:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1131:1-1145:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1149:1-1174:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1175:1-1194:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1199:1-1222:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1223:1-1242:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1246:1-1269:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1270:1-1289:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1290:1-1314:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1324:1-1392:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1393:1-1461:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1462:1-1517:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1527:1-1595:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1596:1-1651:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2090:1-2113:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2114:1-2133:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2186:1-2195:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2363:1-2373:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2452:1-2463:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2464:1-2475:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2547:1-2592:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2593:1-2648:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2649:1-2708:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2711:1-2813:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2814:1-2859:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2860:1-2905:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:279-279)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1815-1815)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1104-1104)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1998..1999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1998-1999)
  on lines 2021..2023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2021-2023)
  on lines 2025..2027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2025-2027)
  on lines 2029..2030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2029-2030)
  on line 2039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2039-2039)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 1668..1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1668-1669)
  on line 1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1676-1676)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2150..2151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2150-2151)
  on line 2158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2158-2158)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1943..1945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1943-1945)
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1947-1948)
  on lines 1952..1955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1952-1955)
  on lines 1957..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1957-1959)
  on lines 1961..1962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1961-1962)
  on lines 1966..1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1966-1969)
  on lines 1971..1973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1971-1973)
  on lines 1975..1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1975-1976)
  on lines 1980..1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1980-1981)
  on line 1985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1985-1985)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1765..1766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1765-1766)
  on line 1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1770-1770)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1836..1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1836-1838)
  on lines 1840..1841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1840-1841)
  on lines 1845..1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1845-1848)
  on lines 1850..1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1850-1852)
  on lines 1854..1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1854-1855)
  on lines 1859..1862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1859-1862)
  on lines 1864..1866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1864-1866)
  on lines 1868..1869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1868-1869)
  on lines 1873..1874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1873-1874)
  on line 1878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1878-1878)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1715..1716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1715-1716)
  on line 1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1723-1723)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 866..867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:866-867)
  on line 873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:873-873)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 677..678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:677-678)
  on line 684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:684-684)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 714..715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:714-715)
  on line 721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:721-721)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:520-520)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:529-529)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 829..830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:829-830)
  on line 836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:836-836)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:554-554)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:511-511)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1684-1684)
  on lines 1689..1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1689-1690)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2050..2051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2050-2051)
  on lines 2061..2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2061-2062)
  on lines 2072..2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2072-2073)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1889..1890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1889-1890)
  on lines 1900..1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1900-1901)
  on lines 1911..1912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1911-1912)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:884-884)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:695-695)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:847-847)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:732-732)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2216-2216)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 465
  dead: 672 (558 in uncalled functions)
  total lines: 1137
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2171:11-2171:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1736:11-1736:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:828:9-828:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1761:11-1761:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:846:9-846:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1997:11-1997:48)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:865:9-865:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1783:11-1783:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:883:9-883:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2020:11-2020:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1831:7-1831:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1832:9-1832:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:676:9-676:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2047:9-2047:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:97:10-97:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2058:11-2058:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:694:9-694:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2068:11-2068:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2069:13-2069:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:713:9-713:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1886:9-1886:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:731:9-731:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2407:7-2407:10)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1667:11-1667:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1897:11-1897:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1683:7-1683:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1907:11-1907:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1908:13-1908:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1686:9-1686:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1938:7-1938:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1939:9-1939:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:2149:11-2149:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product15.cil.c:1714:11-1714: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
