./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_spec3_product27.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_spec3_product27.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_spec3_product27.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_spec3_product27.cil.c:262:3-283:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:319:3-344:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:404:5-424: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_spec3_product27.cil.c:143:1-151:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:169:1-183:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:191:1-236:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:237:1-292:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:293:1-352:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:355:1-457:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:458:1-503:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:504:1-549:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:617:1-626:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:665:1-679:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:701:1-716:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:793:1-813:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:814:1-829:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:832:1-852:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:853:1-868:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:871:1-889:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:890:1-905:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:908:1-926:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:927:1-942:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1227:1-1241:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1556:1-1566:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1645:1-1656:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1657:1-1668:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1997:1-2011:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2015:1-2040:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2041:1-2060:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2065:1-2088:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2089:1-2108:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2156:1-2180:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2190:1-2258:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2259:1-2327:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1984-1984)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2681-2681)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:164-164)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2905-2905)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2406..2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2406-2408)
  on lines 2410..2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2410-2411)
  on lines 2416..2419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2416-2419)
  on lines 2421..2423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2421-2423)
  on lines 2425..2427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2425-2427)
  on lines 2429..2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2429-2430)
  on lines 2435..2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2435-2438)
  on lines 2440..2442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2440-2442)
  on lines 2444..2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2444-2446)
  on lines 2448..2449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2448-2449)
  on lines 2454..2455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2454-2455)
  on line 2459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2459-2459)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 2133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2133-2133)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2542-2542)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2977-2977)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 3024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:3024-3024)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2809..2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2809-2811)
  on lines 2813..2814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2813-2814)
  on lines 2818..2821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2818-2821)
  on lines 2823..2825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2823-2825)
  on lines 2827..2828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2827-2828)
  on lines 2832..2835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2832-2835)
  on lines 2837..2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2837-2839)
  on lines 2841..2842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2841-2842)
  on lines 2846..2847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2846-2847)
  on line 2851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2851-2851)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2631..2632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2631-2632)
  on line 2636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2636-2636)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2702..2704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2702-2704)
  on lines 2706..2707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2706-2707)
  on lines 2711..2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2711-2714)
  on lines 2716..2718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2716-2718)
  on lines 2720..2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2720-2721)
  on lines 2725..2728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2725-2728)
  on lines 2730..2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2730-2732)
  on lines 2734..2735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2734-2735)
  on lines 2739..2740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2739-2740)
  on line 2744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2744-2744)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2589-2589)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 728..729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:728-729)
  on line 735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:735-735)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 691..692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:691-692)
  on line 698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:698-698)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 991..992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:991-992)
  on line 998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:998-998)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 765..766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:765-766)
  on line 772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:772-772)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1280-1280)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1289-1289)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1306..1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1306-1307)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1314-1314)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:140-140)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 954..955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:954-955)
  on line 961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:961-961)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1028..1029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1028-1029)
  on line 1035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1035-1035)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1271-1271)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2473..2474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2473-2474)
  on lines 2481..2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2481-2483)
  on lines 2485..2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2485-2486)
  on lines 2488..2489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2488-2489)
  on lines 2496..2498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2496-2498)
  on lines 2500..2501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2500-2501)
  on lines 2503..2504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2503-2504)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2336..2337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2336-2337)
  on lines 2339..2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2339-2340)
  on lines 2347..2349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2347-2349)
  on lines 2351..2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2351-2352)
  on lines 2354..2355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2354-2355)
  on lines 2362..2364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2362-2364)
  on lines 2366..2367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2366-2367)
  on lines 2369..2370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2369-2370)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2143..2144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2143-2144)
  on lines 2146..2147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2146-2147)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2550-2550)
  on lines 2555..2556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2555-2556)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2985-2985)
  on lines 2990..2991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2990-2991)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2916..2917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2916-2917)
  on lines 2927..2928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2927-2928)
  on lines 2938..2939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2938-2939)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2755..2756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2755-2756)
  on lines 2766..2767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2766-2767)
  on lines 2777..2778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2777-2778)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:746-746)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1046 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1046-1046)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:972-972)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1009-1009)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:783-783)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:647-647)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1410-1410)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 639
  dead: 567 (383 in uncalled functions)
  total lines: 1206
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2649:11-2649:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1796:10-1796:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2697:7-2697:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2698:9-2698:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2466:7-2466:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2470:11-2470:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2913:9-2913:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2924:11-2924:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2934:11-2934:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2935:13-2935:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:690:9-690:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2752:9-2752:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:953:9-953:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1600:7-1600:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2763:11-2763:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2332:7-2332:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2984:7-2984:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2333:9-2333:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2140:7-2140:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2549:7-2549:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2773:11-2773:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2987:9-2987:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2774:13-2774:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:971:9-971:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2552:9-2552:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:727:9-727:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2804:7-2804:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2805:9-2805:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:990:9-990:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1305:9-1305:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:745:9-745:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1008:9-1008:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:764:9-764:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2397:7-2397:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1027:9-1027:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:3037:11-3037:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2602:11-2602:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:782:9-782:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2402:11-2402:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1045:9-1045:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:2627:11-2627:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product27.cil.c:1400:7-1400:10)
[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)
