./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_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_spec8_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_spec8_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_spec8_product26.cil.c:881:3-902:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:938:3-963:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1023:5-1043: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_product26.cil.c:192:1-202:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:281:1-292:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:293:1-304:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:660:1-674:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:810:1-855:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:856:1-911:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:912:1-971:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:974:1-1076:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1077:1-1122:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1123:1-1168:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1393:1-1402:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1428:1-1442:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1458:1-1472:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1494:1-1509:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1586:1-1606:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1607:1-1622:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1625:1-1645:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1646:1-1661:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1738:1-1756:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1757:1-1772:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1775:1-1793:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1794:1-1809:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1812:1-1830:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1831:1-1846:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1926:1-1934:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1960:1-1974:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1978:1-2003:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2004:1-2023:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2028:1-2051:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2052:1-2071:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2119:1-2143:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2153:1-2221:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2222:1-2290:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:800-800)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2644 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2644-2644)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1947-1947)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2868-2868)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2369..2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2369-2371)
  on lines 2373..2374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2373-2374)
  on lines 2379..2382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2379-2382)
  on lines 2384..2386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2384-2386)
  on lines 2388..2390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2388-2390)
  on lines 2392..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2392-2393)
  on lines 2398..2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2398-2401)
  on lines 2403..2405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2403-2405)
  on lines 2407..2409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2407-2409)
  on lines 2411..2412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2411-2412)
  on lines 2417..2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2417-2418)
  on line 2422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2422-2422)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 2096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2096-2096)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2505-2505)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2940-2940)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2987-2987)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2772..2774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2772-2774)
  on lines 2776..2777 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2776-2777)
  on lines 2781..2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2781-2784)
  on lines 2786..2788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2786-2788)
  on lines 2790..2791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2790-2791)
  on lines 2795..2798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2795-2798)
  on lines 2800..2802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2800-2802)
  on lines 2804..2805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2804-2805)
  on lines 2809..2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2809-2810)
  on line 2814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2814-2814)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2594..2595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2594-2595)
  on line 2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2599-2599)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2665..2667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2665-2667)
  on lines 2669..2670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2669-2670)
  on lines 2674..2677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2674-2677)
  on lines 2679..2681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2679-2681)
  on lines 2683..2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2683-2684)
  on lines 2688..2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2688-2691)
  on lines 2693..2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2693-2695)
  on lines 2697..2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2697-2698)
  on lines 2702..2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2702-2703)
  on line 2707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2707-2707)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2552-2552)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1710..1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1710-1711)
  on line 1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1717-1717)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1521..1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1521-1522)
  on line 1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1528-1528)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1484..1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1484-1485)
  on line 1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1491-1491)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1558..1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1558-1559)
  on line 1565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1565-1565)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:713-713)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:722-722)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1673..1674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1673-1674)
  on line 1680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1680-1680)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 739..740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:739-740)
  on line 747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:747-747)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1923-1923)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1903-1903)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:704-704)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2436..2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2436-2437)
  on lines 2444..2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2444-2446)
  on lines 2448..2449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2448-2449)
  on lines 2451..2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2451-2452)
  on lines 2459..2461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2459-2461)
  on lines 2463..2464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2463-2464)
  on lines 2466..2467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2466-2467)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2299..2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2299-2300)
  on lines 2302..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2302-2303)
  on lines 2310..2312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2310-2312)
  on lines 2314..2315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2314-2315)
  on lines 2317..2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2317-2318)
  on lines 2325..2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2325-2327)
  on lines 2329..2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2329-2330)
  on lines 2332..2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2332-2333)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2106..2107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2106-2107)
  on lines 2109..2110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2109-2110)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2513-2513)
  on lines 2518..2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2518-2519)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2948-2948)
  on lines 2953..2954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2953-2954)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2879..2880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2879-2880)
  on lines 2890..2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2890-2891)
  on lines 2901..2902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2901-2902)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2718..2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2718-2719)
  on lines 2729..2730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2729-2730)
  on lines 2740..2741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2740-2741)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1728-1728)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1539-1539)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1691-1691)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1576-1576)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1423-1423)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 613
  dead: 577 (397 in uncalled functions)
  total lines: 1190
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1209:10-1209:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1727:9-1727:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1483:9-1483:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2660:7-2660:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2661:9-2661:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2429:7-2429:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2433:11-2433:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1520:9-1520:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2876:9-2876:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2887:11-2887:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1538:9-1538:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2897:11-2897:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2898:13-2898:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1557:9-1557:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2715:9-2715:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1575:9-1575:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:738:9-738:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2726:11-2726:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2295:7-2295:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2947:7-2947:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2296:9-2296:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2103:7-2103:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2512:7-2512:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2736:11-2736:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2950:9-2950:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2737:13-2737:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2515:9-2515:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2767:7-2767:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2768:9-2768:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2360:7-2360:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:3000:11-3000:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2565:11-2565:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2365:11-2365:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1672:9-1672:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2590:11-2590:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:236:7-236:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1690:9-1690:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:1709:9-1709:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product26.cil.c:2612:11-2612: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
