./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_product13.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_product13.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_product13.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_product13.cil.c:1505:3-1526:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1562:3-1587:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1647:5-1667: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 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:495:1-505:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:584:1-595:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:596:1-607:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:682:1-696:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:699:1-717:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:718:1-733:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:810:1-830:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:831:1-846:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:849:1-869:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:870:1-885:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:888:1-906:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:907:1-922:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:925:1-943:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:944:1-959:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1036:1-1054:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1156:1-1170:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1184:1-1193:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1203:1-1211:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1212:1-1220:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1333:1-1360:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1361:1-1379:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1380:1-1393:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1403:1-1411:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1434:1-1479:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1480:1-1535:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1536:1-1595:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1598:1-1700:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1701:1-1746:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1747:1-1792:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1812:1-1826:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1830:1-1855:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1856:1-1875:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1880:1-1903:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1904:1-1923:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1927:1-1950:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1951:1-1970:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1971:1-1995:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2005:1-2073:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2074:1-2142:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2143:1-2198:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2208:1-2276:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2277:1-2332:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2336:1-2359:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2360:1-2379:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2771:1-2794:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2795:1-2814:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2873:1-2887:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2868-2868)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 487..489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:487-489)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2496-2496)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1424-1424)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2674..2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2674-2676)
  on lines 2678..2680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2678-2680)
  on lines 2682..2683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2682-2683)
  on lines 2693..2694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2693-2694)
  on lines 2701..2704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2701-2704)
  on lines 2706..2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2706-2708)
  on lines 2710..2711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2710-2711)
  on lines 2715..2716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2715-2716)
  on line 2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2720-2720)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2826..2828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2826-2828)
  on lines 2830..2832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2830-2832)
  on lines 2834..2835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2834-2835)
  on line 2839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2839-2839)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2624..2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2624-2626)
  on lines 2628..2629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2628-2629)
  on lines 2633..2636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2633-2636)
  on lines 2638..2640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2638-2640)
  on lines 2642..2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2642-2643)
  on lines 2647..2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2647-2650)
  on lines 2652..2654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2652-2654)
  on lines 2656..2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2656-2657)
  on lines 2661..2662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2661-2662)
  on line 2666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2666-2666)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2446..2447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2446-2447)
  on line 2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2451-2451)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2517..2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2517-2519)
  on lines 2521..2522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2521-2522)
  on lines 2526..2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2526-2529)
  on lines 2531..2533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2531-2533)
  on lines 2535..2536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2535-2536)
  on lines 2540..2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2540-2543)
  on lines 2545..2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2545-2547)
  on lines 2549..2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2549-2550)
  on lines 2554..2555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2554-2555)
  on line 2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2559-2559)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2391..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2391-2393)
  on lines 2395..2397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2395-2397)
  on lines 2399..2400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2399-2400)
  on line 2404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2404-2404)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 744..746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:744-746)
  on lines 748..749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:748-749)
  on line 752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:752-752)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1007..1009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1007-1009)
  on lines 1011..1012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1011-1012)
  on line 1015 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1015-1015)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 781..783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:781-783)
  on lines 785..786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:785-786)
  on line 789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:789-789)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1231..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1231-1232)
  on lines 1235..1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1235-1236)
  on line 1243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1243-1243)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1400-1400)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 970..972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:970-972)
  on lines 974..975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:974-975)
  on line 978 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:978-978)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1200-1200)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2731..2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2731-2732)
  on lines 2742..2743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2742-2743)
  on lines 2753..2754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2753-2754)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2570..2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2570-2571)
  on lines 2581..2582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2581-2582)
  on lines 2592..2593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2592-2593)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 762..763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:762-763)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 1062..1063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1062-1063)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 988..989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:988-989)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 1025..1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1025-1026)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 799..800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:799-800)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1266-1266)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:94-94)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1302-1302)
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1305-1305)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 393
  dead: 735 (577 in uncalled functions)
  total lines: 1128
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2588:11-2588:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2589:13-2589:23)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:539:7-539:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2822:7-2822:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2619:7-2619:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2620:9-2620:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2387:7-2387:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2852:11-2852:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2417:11-2417:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2442:11-2442:22)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2673:7-2673:18)
[Warning][Deadcode][CWE-570] condition '! publicKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1230:7-1230:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2464:11-2464:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1234:9-1234:21)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2687:9-2687:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2692:13-2692:50)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:966:7-966:18)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1265:7-1265:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2512:7-2512:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2513:9-2513:19)
[Warning][Deadcode][CWE-571] condition 'sent_signed == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:134:7-134:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:985:7-985:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:740:7-740:18)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1295:7-1295:10)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1299:9-1299:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1003:7-1003:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2728:9-2728:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:759:7-759:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2739:11-2739:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1022:7-1022:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:777:7-777:18)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:483:7-483:14)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2749:11-2749:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2750:13-2750:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:211:10-211:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:796:7-796:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2567:9-2567:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:1059:7-1059:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product13.cil.c:2578:11-2578:21)
[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)
