./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_spec1_product31.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_spec1_product31.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_spec1_product31.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_spec1_product31.cil.c:567:3-588:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:624:3-649:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:709:5-729: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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:308:1-322:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:496:1-541:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:542:1-597:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:598:1-657:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:660:1-762:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:763:1-808:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:809:1-854:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:968:1-976:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1222:1-1231:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1360:1-1370:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1449:1-1460:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1461:1-1472:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1545:1-1559:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1581:1-1596:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1673:1-1693:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1694:1-1709:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1712:1-1732:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1733:1-1748:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1951:1-1965:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1969:1-1994:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1995:1-2014:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2019:1-2042:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2043:1-2062:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2066:1-2089:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2090:1-2109:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2110:1-2134:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2144:1-2212:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2213:1-2281:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2282:1-2337:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2347:1-2415:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2416:1-2471:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2475:1-2498:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2499:1-2518:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:3007-3007)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2635-2635)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:989-989)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2818..2819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2818-2819)
  on line 2859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2859-2859)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2915..2916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2915-2916)
  on line 2931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2931-2931)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2970..2971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2970-2971)
  on line 2978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2978-2978)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2763..2765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2763-2765)
  on lines 2767..2768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2767-2768)
  on lines 2772..2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2772-2775)
  on lines 2777..2779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2777-2779)
  on lines 2781..2782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2781-2782)
  on lines 2786..2789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2786-2789)
  on lines 2791..2793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2791-2793)
  on lines 2795..2796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2795-2796)
  on lines 2800..2801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2800-2801)
  on line 2805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2805-2805)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2585..2586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2585-2586)
  on line 2590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2590-2590)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2656..2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2656-2658)
  on lines 2660..2661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2660-2661)
  on lines 2665..2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2665-2668)
  on lines 2670..2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2670-2672)
  on lines 2674..2675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2674-2675)
  on lines 2679..2682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2679-2682)
  on lines 2684..2686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2684-2686)
  on lines 2688..2689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2688-2689)
  on lines 2693..2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2693-2694)
  on line 2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2698-2698)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2543-2543)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1797..1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1797-1798)
  on line 1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1804-1804)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1608..1609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1608-1609)
  on line 1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1615-1615)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1571..1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1571-1572)
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1578-1578)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1871..1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1871-1872)
  on line 1878 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1878-1878)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1645..1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1645-1646)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1652-1652)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:361-361)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:370-370)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1760..1761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1760-1761)
  on line 1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1767-1767)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 387..388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:387-388)
  on line 395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:395-395)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:965-965)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:945-945)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1834..1835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1834-1835)
  on line 1841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1841-1841)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1908..1909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1908-1909)
  on line 1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1915-1915)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:352-352)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2939-2939)
  on lines 2944..2945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2944-2945)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2870..2871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2870-2871)
  on lines 2881..2882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2881-2882)
  on lines 2892..2893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2892-2893)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2709..2710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2709-2710)
  on lines 2720..2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2720-2721)
  on lines 2731..2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2731-2732)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1815-1815)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1626-1626)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1778-1778)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1926-1926)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1852-1852)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1889-1889)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1663-1663)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1252-1252)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 585
  dead: 599 (476 in uncalled functions)
  total lines: 1184
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2651:7-2651:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2652:9-2652:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1759:9-1759:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2867:9-2867:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2878:11-2878:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1777:9-1777:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2888:11-2888:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2889:13-2889:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1796:9-1796:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2914:7-2914:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:386:9-386:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2706:9-2706:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1814:9-1814:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1570:9-1570:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2717:11-2717:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1833:9-1833:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2938:7-2938:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2727:11-2727:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2941:9-2941:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2728:13-2728:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1851:9-1851:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1607:9-1607:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2758:7-2758:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2759:9-2759:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1041:10-1041:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1870:9-1870:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2969:11-2969:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1625:9-1625:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1888:9-1888:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1644:9-1644:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2991:11-2991:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2556:11-2556:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1907:9-1907:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1662:9-1662:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2581:11-2581:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1925:9-1925:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:1404:7-1404:10)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2817:11-2817:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product31.cil.c:2603:11-2603: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
