./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_spec9_product16.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_spec9_product16.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_spec9_product16.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_spec9_product16.cil.c:311:3-332:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:368:3-393:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:453:5-473: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:192:1-200:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:218:1-232:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:240:1-285:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:286:1-341:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:342:1-401:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:404:1-506:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:507:1-552:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:553:1-598:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:615:1-629:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:651:1-666:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:743:1-763:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:764:1-779:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:782:1-802:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:803:1-818:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:895:1-913:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:914:1-929:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:932:1-950:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:951:1-966:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:969:1-987:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:988:1-1003:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1166:1-1180:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1283:1-1292:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1655:1-1665:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1744:1-1755:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1756:1-1767:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1849:1-1863:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1867:1-1892:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1893:1-1912:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1917:1-1940:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1941:1-1960:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1964:1-1987:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1988:1-2007:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2008:1-2032:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2042:1-2110:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2111:1-2179:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2180:1-2235:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2245:1-2313:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2314:1-2369:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2373:1-2396:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2397:1-2416:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1547-1547)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2533-2533)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:213-213)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2716..2717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2716-2717)
  on lines 2739..2741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2739-2741)
  on lines 2743..2745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2743-2745)
  on lines 2747..2748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2747-2748)
  on line 2757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2757-2757)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2813..2814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2813-2814)
  on line 2829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2829-2829)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2868..2869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2868-2869)
  on line 2876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2876-2876)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2661..2663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2661-2663)
  on lines 2665..2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2665-2666)
  on lines 2670..2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2670-2673)
  on lines 2675..2677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2675-2677)
  on lines 2679..2680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2679-2680)
  on lines 2684..2687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2684-2687)
  on lines 2689..2691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2689-2691)
  on lines 2693..2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2693-2694)
  on lines 2698..2699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2698-2699)
  on line 2703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2703-2703)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2483..2484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2483-2484)
  on line 2488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2488-2488)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2554..2556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2554-2556)
  on lines 2558..2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2558-2559)
  on lines 2563..2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2563-2566)
  on lines 2568..2570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2568-2570)
  on lines 2572..2573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2572-2573)
  on lines 2577..2580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2577-2580)
  on lines 2582..2584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2582-2584)
  on lines 2586..2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2586-2587)
  on lines 2591..2592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2591-2592)
  on line 2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2596-2596)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2425..2426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2425-2426)
  on line 2441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2441-2441)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 867..868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:867-868)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:874-874)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 678..679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:678-679)
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:685-685)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 641..642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:641-642)
  on line 648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:648-648)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 715..716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:715-716)
  on line 722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:722-722)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1219-1219)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1228-1228)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 830..831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:830-831)
  on line 837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:837-837)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1245..1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1245-1246)
  on line 1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1253-1253)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:189-189)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:169-169)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1210-1210)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2837-2837)
  on lines 2842..2843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2842-2843)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2768..2769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2768-2769)
  on lines 2779..2780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2779-2780)
  on lines 2790..2791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2790-2791)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2607..2608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2607-2608)
  on lines 2618..2619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2618-2619)
  on lines 2629..2630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2629-2630)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:885-885)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:696-696)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:848-848)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:733-733)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1313-1313)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 500
  dead: 639 (518 in uncalled functions)
  total lines: 1139
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2604:9-2604:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2615:11-2615:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1699:7-1699:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:829:9-829:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2836:7-2836:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2625:11-2625:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2839:9-2839:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2626:13-2626:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:847:9-847:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2656:7-2656:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2657:9-2657:19)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2424:7-2424:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:866:9-866:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2867:11-2867:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:884:9-884:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:640:9-640:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2889:11-2889:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2454:11-2454:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2479:11-2479:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:677:9-677:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1244:9-1244:21)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2715:11-2715:48)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:695:9-695:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2501:11-2501:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:714:9-714:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2738:11-2738:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2549:7-2549:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:732:9-732:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2550:9-2550:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2765:9-2765:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:1365:10-1365:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2776:11-2776:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2786:11-2786:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2787:13-2787:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product16.cil.c:2812:7-2812:18)
[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)
