./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_spec6_product33.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_spec6_product33.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_spec6_product33.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_spec6_product33.cil.c:2258:3-2279:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2315:3-2340:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2400:5-2420: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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:105:1-119:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:123:1-148:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:149:1-168:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:173:1-196:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:197:1-216:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:220:1-243:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:244:1-263:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:264:1-288:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:298:1-366:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:367:1-435:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:436:1-491:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:501:1-569:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:570:1-625:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1386:1-1400:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1958:1-1968:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2047:1-2058:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2059:1-2070:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2147:1-2156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2187:1-2232:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2233:1-2288:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2289:1-2348:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2351:1-2453:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2454:1-2499:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2500:1-2545:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2556:1-2570:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2592:1-2607:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2684:1-2704:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2705:1-2720:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2723:1-2743:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2744:1-2759:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:3056:1-3064:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 72 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:72-72)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:789-789)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:3077-3077)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1013-1013)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:650-650)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1085-1085)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1124..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1124-1125)
  on line 1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1132-1132)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 917..919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:917-919)
  on lines 921..922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:921-922)
  on lines 926..929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:926-929)
  on lines 931..933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:931-933)
  on lines 935..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:935-936)
  on lines 940..943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:940-943)
  on lines 945..947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:945-947)
  on lines 949..950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:949-950)
  on lines 954..955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:954-955)
  on line 959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:959-959)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 739..740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:739-740)
  on line 744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:744-744)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 810..812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:810-812)
  on lines 814..815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:814-815)
  on lines 819..822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:819-822)
  on lines 824..826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:824-826)
  on lines 828..829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:828-829)
  on lines 833..836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:833-836)
  on lines 838..840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:838-840)
  on lines 842..843 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:842-843)
  on lines 847..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:847-848)
  on line 852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:852-852)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:697-697)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2808..2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2808-2809)
  on line 2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2815-2815)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2619..2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2619-2620)
  on line 2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2626-2626)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2582..2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2582-2583)
  on line 2589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2589-2589)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2882..2883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2882-2883)
  on line 2889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2889-2889)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2656..2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2656-2657)
  on line 2663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2663-2663)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1439-1439)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1448-1448)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2771..2772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2771-2772)
  on line 2778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2778-2778)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1473-1473)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 3053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:3053-3053)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 3033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:3033-3033)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2845..2846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2845-2846)
  on line 2852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2852-2852)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2919..2920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2919-2920)
  on line 2926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2926-2926)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1430-1430)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:658-658)
  on lines 663..664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:663-664)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1093-1093)
  on lines 1098..1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1098-1099)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1024..1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1024-1025)
  on lines 1035..1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1035-1036)
  on lines 1046..1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1046-1047)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 863..864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:863-864)
  on lines 874..875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:874-875)
  on lines 885..886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:885-886)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2826-2826)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2637-2637)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2789-2789)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2937-2937)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2863-2863)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2900-2900)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2674-2674)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2177 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2177-2177)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 636
  dead: 578 (457 in uncalled functions)
  total lines: 1214
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2825:9-2825:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2581:9-2581:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:860:9-860:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2844:9-2844:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:871:11-871:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2002:7-2002:10)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1092:7-1092:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:657:7-657:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:881:11-881:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:882:13-882:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2862:9-2862:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1095:9-1095:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:660:9-660:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2618:9-2618:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:912:7-912:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:913:9-913:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2881:9-2881:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2636:9-2636:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1123:11-1123:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2899:9-2899:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2655:9-2655:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2918:9-2918:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1145:11-1145:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:710:11-710:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2673:9-2673:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2936:9-2936:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:735:11-735:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:757:11-757:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:805:7-805:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:806:9-806:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2770:9-2770:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1021:9-1021:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2788:9-2788:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1032:11-1032:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:2807:9-2807:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1678:10-1678:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1042:11-1042:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product33.cil.c:1043:13-1043:23)
[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
