./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_spec8_product21.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_spec8_product21.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_spec8_product21.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_spec8_product21.cil.c:1116:3-1137:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1173:3-1198:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1258:5-1278: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:190:1-200:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:279:1-290:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:291:1-302:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:468:1-476:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:691:1-705:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1045:1-1090:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1091:1-1146:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1147:1-1206:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1209:1-1311:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1312:1-1357:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1358:1-1403:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1458:1-1472:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1476:1-1501:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1502:1-1521:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1526:1-1549:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1550:1-1569:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1617:1-1641:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1651:1-1719:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1720:1-1788:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1982:1-2005:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2006:1-2025:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2510:1-2519:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2557:1-2571:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2593:1-2608:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2685:1-2705:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2706:1-2721:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2724:1-2744:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2745:1-2760:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2837:1-2855:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2856:1-2871:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2874:1-2892:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2893:1-2908:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2911:1-2929:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2930:1-2945:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2948:1-2962:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:816-816)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2142-2142)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:489-489)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2348..2350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2348-2350)
  on lines 2352..2354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2352-2354)
  on lines 2356..2357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2356-2357)
  on line 2366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2366-2366)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1867..1869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1867-1869)
  on lines 1871..1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1871-1872)
  on lines 1877..1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1877-1880)
  on lines 1882..1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1882-1884)
  on lines 1886..1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1886-1888)
  on lines 1890..1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1890-1891)
  on lines 1896..1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1896-1899)
  on lines 1901..1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1901-1903)
  on lines 1905..1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1905-1907)
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1909-1910)
  on lines 1915..1916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1915-1916)
  on line 1920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1920-1920)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 1586..1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1586-1587)
  on line 1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1594-1594)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2422..2423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2422-2423)
  on line 2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2438-2438)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2477..2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2477-2478)
  on line 2485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2485-2485)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2270..2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2270-2272)
  on lines 2274..2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2274-2275)
  on lines 2279..2282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2279-2282)
  on lines 2284..2286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2284-2286)
  on lines 2288..2289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2288-2289)
  on lines 2293..2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2293-2296)
  on lines 2298..2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2298-2300)
  on lines 2302..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2302-2303)
  on lines 2307..2308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2307-2308)
  on line 2312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2312-2312)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2092..2093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2092-2093)
  on line 2097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2097-2097)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2163..2165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2163-2165)
  on lines 2167..2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2167-2168)
  on lines 2172..2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2172-2175)
  on lines 2177..2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2177-2179)
  on lines 2181..2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2181-2182)
  on lines 2186..2189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2186-2189)
  on lines 2191..2193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2191-2193)
  on lines 2195..2196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2195-2196)
  on lines 2200..2201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2200-2201)
  on line 2205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2205-2205)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2034..2035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2034-2035)
  on line 2050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2050-2050)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2809..2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2809-2810)
  on line 2816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2816-2816)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2620..2621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2620-2621)
  on line 2627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2627-2627)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2583..2584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2583-2584)
  on line 2590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2590-2590)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2657..2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2657-2658)
  on line 2664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2664-2664)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:744-744)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:753-753)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2772..2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2772-2773)
  on line 2779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2779-2779)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 770..771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:770-771)
  on line 778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:778-778)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:465-465)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:445-445)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:735-735)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1934..1935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1934-1935)
  on lines 1942..1944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1942-1944)
  on lines 1946..1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1946-1947)
  on lines 1949..1950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1949-1950)
  on lines 1957..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1957-1959)
  on lines 1961..1962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1961-1962)
  on lines 1964..1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1964-1965)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1797..1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1797-1798)
  on lines 1800..1801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1800-1801)
  on lines 1808..1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1808-1810)
  on lines 1812..1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1812-1813)
  on lines 1815..1816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1815-1816)
  on lines 1823..1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1823-1825)
  on lines 1827..1828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1827-1828)
  on lines 1830..1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1830-1831)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1604..1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1604-1605)
  on lines 1607..1608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1607-1608)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2446-2446)
  on lines 2451..2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2451-2452)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2377..2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2377-2378)
  on lines 2388..2389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2388-2389)
  on lines 2399..2400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2399-2400)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2216..2217 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2216-2217)
  on lines 2227..2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2227-2228)
  on lines 2238..2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2238-2239)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2827-2827)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2638-2638)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2790-2790)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2675-2675)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2540-2540)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 563
  dead: 608 (416 in uncalled functions)
  total lines: 1171
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2808:9-2808:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2110:11-2110:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2826:9-2826:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2582:9-2582:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2347:11-2347:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2158:7-2158:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2159:9-2159:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2619:9-2619:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1927:7-1927:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1931:11-1931:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2637:9-2637:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2374:9-2374:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2385:11-2385:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2656:9-2656:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2395:11-2395:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2396:13-2396:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2674:9-2674:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2421:7-2421:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2213:9-2213:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1585:11-1585:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:769:9-769:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2224:11-2224:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1793:7-1793:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2445:7-2445:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1794:9-1794:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1601:7-1601:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2234:11-2234:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2448:9-2448:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2235:13-2235:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2265:7-2265:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2266:9-2266:19)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2033:7-2033:18)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2476:11-2476:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:234:7-234:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2771:9-2771:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1858:7-1858:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:859:10-859:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2498:11-2498:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2063:11-2063:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:1863:11-1863:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2789:9-2789:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product21.cil.c:2088:11-2088: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
