./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/email_spec1_product20.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/email_spec1_product20.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_product20.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_product20.cil.c:2607:3-2628:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2664:3-2689:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2749:5-2769: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] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:71:1-85:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:88:1-106:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:107:1-122:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:199:1-219:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:220:1-235:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:238:1-258:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:259:1-274:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:351:1-369:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:370:1-385:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:388:1-406:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:407:1-422:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:425:1-443:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:444:1-459:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:673:1-687:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:799:1-826:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:827:1-845:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:846:1-854:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:855:1-874:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:875:1-883:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1030:1-1040:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1119:1-1130:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1131:1-1142:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1451:1-1465:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1469:1-1494:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1495:1-1514:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1519:1-1542:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1543:1-1562:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1610:1-1634:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1644:1-1712:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1713:1-1781:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2410:1-2433:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2434:1-2453:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2536:1-2581:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2582:1-2637:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2638:1-2697:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2700:1-2802:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2803:1-2848:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2849:1-2894:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2897:1-2906:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2932:1-2946:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:905-905)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2135-2135)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:896-896)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2359-2359)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1860..1862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1860-1862)
  on lines 1864..1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1864-1865)
  on lines 1870..1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1870-1873)
  on lines 1875..1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1875-1877)
  on lines 1879..1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1879-1881)
  on lines 1883..1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1883-1884)
  on lines 1889..1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1889-1892)
  on lines 1894..1896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1894-1896)
  on lines 1898..1900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1898-1900)
  on lines 1902..1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1902-1903)
  on lines 1908..1909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1908-1909)
  on line 1913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1913-1913)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1587-1587)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1996-1996)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2478-2478)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2263..2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2263-2265)
  on lines 2267..2268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2267-2268)
  on lines 2272..2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2272-2275)
  on lines 2277..2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2277-2279)
  on lines 2281..2282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2281-2282)
  on lines 2286..2289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2286-2289)
  on lines 2291..2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2291-2293)
  on lines 2295..2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2295-2296)
  on lines 2300..2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2300-2301)
  on line 2305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2305-2305)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2085..2086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2085-2086)
  on line 2090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2090-2090)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2156..2158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2156-2158)
  on lines 2160..2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2160-2161)
  on lines 2165..2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2165-2168)
  on lines 2170..2172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2170-2172)
  on lines 2174..2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2174-2175)
  on lines 2179..2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2179-2182)
  on lines 2184..2186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2184-2186)
  on lines 2188..2189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2188-2189)
  on lines 2193..2194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2193-2194)
  on line 2198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2198-2198)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2043-2043)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 323..324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:323-324)
  on line 330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:330-330)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 134..135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:134-135)
  on line 141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:141-141)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 171..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:171-172)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:178-178)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:726-726)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:735-735)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 286..287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:286-287)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:293-293)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 752..753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:752-753)
  on line 760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:760-760)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:717-717)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1927..1928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1927-1928)
  on lines 1935..1937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1935-1937)
  on lines 1939..1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1939-1940)
  on lines 1942..1943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1942-1943)
  on lines 1950..1952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1950-1952)
  on lines 1954..1955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1954-1955)
  on lines 1957..1958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1957-1958)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1790..1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1790-1791)
  on lines 1793..1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1793-1794)
  on lines 1801..1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1801-1803)
  on lines 1805..1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1805-1806)
  on lines 1808..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1808-1809)
  on lines 1816..1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1816-1818)
  on lines 1820..1821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1820-1821)
  on lines 1823..1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1823-1824)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1597..1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1597-1598)
  on lines 1600..1601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1600-1601)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2004-2004)
  on lines 2009..2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2009-2010)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2370..2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2370-2371)
  on lines 2381..2382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2381-2382)
  on lines 2392..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2392-2393)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2209..2210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2209-2210)
  on lines 2220..2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2220-2221)
  on lines 2231..2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2231-2232)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:341-341)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:152-152)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:304-304)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:189-189)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2927-2927)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 531
  dead: 627 (456 in uncalled functions)
  total lines: 1158
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1851:7-1851:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2491:11-2491:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2056:11-2056:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1856:11-1856:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2081:11-2081:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2103:11-2103:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:285:9-285:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:303:9-303:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2151:7-2151:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2152:9-2152: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_product20.cil.c:1260:10-1260:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:322:9-322:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1920:7-1920:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1924:11-1924:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2367:9-2367:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:340:9-340:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2378:11-2378:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2388:11-2388:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2389:13-2389:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:133:9-133:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2206:9-2206:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2217:11-2217:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1786:7-1786:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1787:9-1787:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1594:7-1594:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2003:7-2003:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2227:11-2227:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:1074:7-1074:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:170:9-170:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2228:13-2228:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2006:9-2006:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:751:9-751:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2258:7-2258:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:2259:9-2259:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product20.cil.c:188:9-188:20)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
