./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_product26.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_product26.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_product26.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_product26.cil.c:2670:3-2691:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2727:3-2752:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2812:5-2832: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_spec0_product26.cil.c:287:1-301:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:439:1-453:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:475:1-490:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:567:1-587:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:588:1-603:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:606:1-626:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:627:1-642:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:719:1-737:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:738:1-753:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:756:1-774:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:775:1-790:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:793:1-811:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:812:1-827:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:952:1-962:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1041:1-1052:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1053:1-1064:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1453:1-1461:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1479:1-1488:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1522:1-1536:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1540:1-1565:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1566:1-1585:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1590:1-1613:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1614:1-1633:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1681:1-1705:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1715:1-1783:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1784:1-1852:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2599:1-2644:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2645:1-2700:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2701:1-2760:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2763:1-2865:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2866:1-2911:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2912:1-2957:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2960:1-2974:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2981-2981)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2206-2206)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1474-1474)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2430-2430)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1931..1933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1931-1933)
  on lines 1935..1936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1935-1936)
  on lines 1941..1944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1941-1944)
  on lines 1946..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1946-1948)
  on lines 1950..1952 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1950-1952)
  on lines 1954..1955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1954-1955)
  on lines 1960..1963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1960-1963)
  on lines 1965..1967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1965-1967)
  on lines 1969..1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1969-1971)
  on lines 1973..1974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1973-1974)
  on lines 1979..1980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1979-1980)
  on line 1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1984-1984)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1658-1658)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2067-2067)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2502-2502)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2549-2549)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2334..2336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2334-2336)
  on lines 2338..2339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2338-2339)
  on lines 2343..2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2343-2346)
  on lines 2348..2350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2348-2350)
  on lines 2352..2353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2352-2353)
  on lines 2357..2360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2357-2360)
  on lines 2362..2364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2362-2364)
  on lines 2366..2367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2366-2367)
  on lines 2371..2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2371-2372)
  on line 2376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2376-2376)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2156..2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2156-2157)
  on line 2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2161-2161)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2227..2229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2227-2229)
  on lines 2231..2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2231-2232)
  on lines 2236..2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2236-2239)
  on lines 2241..2243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2241-2243)
  on lines 2245..2246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2245-2246)
  on lines 2250..2253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2250-2253)
  on lines 2255..2257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2255-2257)
  on lines 2259..2260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2259-2260)
  on lines 2264..2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2264-2265)
  on line 2269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2269-2269)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2114-2114)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 691..692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:691-692)
  on line 698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:698-698)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 502..503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:502-503)
  on line 509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:509-509)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 465..466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:465-466)
  on line 472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:472-472)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 539..540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:539-540)
  on line 546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:546-546)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:340-340)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:349-349)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 654..655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:654-655)
  on line 661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:661-661)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 366..367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:366-367)
  on line 374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:374-374)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1450-1450)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1430-1430)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:331-331)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1998..1999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1998-1999)
  on lines 2006..2008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2006-2008)
  on lines 2010..2011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2010-2011)
  on lines 2013..2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2013-2014)
  on lines 2021..2023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2021-2023)
  on lines 2025..2026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2025-2026)
  on lines 2028..2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2028-2029)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1861..1862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1861-1862)
  on lines 1864..1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1864-1865)
  on lines 1872..1874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1872-1874)
  on lines 1876..1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1876-1877)
  on lines 1879..1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1879-1880)
  on lines 1887..1889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1887-1889)
  on lines 1891..1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1891-1892)
  on lines 1894..1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1894-1895)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1668..1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1668-1669)
  on lines 1671..1672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1671-1672)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2075-2075)
  on lines 2080..2081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2080-2081)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2510-2510)
  on lines 2515..2516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2515-2516)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2441..2442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2441-2442)
  on lines 2452..2453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2452-2453)
  on lines 2463..2464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2463-2464)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2280..2281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2280-2281)
  on lines 2291..2292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2291-2292)
  on lines 2302..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2302-2303)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:709-709)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:520-520)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:672-672)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:557-557)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1509-1509)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 602
  dead: 577 (397 in uncalled functions)
  total lines: 1179
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1857:7-1857:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2509:7-2509:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1858:9-1858:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1665:7-1665:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2074:7-2074:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2298:11-2298:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:556:9-556:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2512:9-2512:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2299:13-2299:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2077:9-2077:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2329:7-2329:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2330:9-2330:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1192:10-1192:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1922:7-1922:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2562:11-2562:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2127:11-2127:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1927:11-1927:21)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:365:9-365:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2152:11-2152:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:653:9-653:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2174:11-2174:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:671:9-671:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:996:7-996:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:690:9-690:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2222:7-2222:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2223:9-2223:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:708:9-708:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:464:9-464:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1991:7-1991:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:1995:11-1995:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2438:9-2438:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2449:11-2449:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:501:9-501:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2459:11-2459:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2460:13-2460:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:519:9-519:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2277:9-2277:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:538:9-538:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product26.cil.c:2288:11-2288:21)
[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
