./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_spec1_product33.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_spec1_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_spec1_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_spec1_product33.cil.c:312:3-333:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:369:3-394:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:454:5-474: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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:60:1-74:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:210:1-218:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:241:1-286:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:287:1-342:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:343:1-402:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:405:1-507:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:508:1-553:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:554:1-599:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:834:1-843:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1079:1-1093:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1326:1-1340:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1344:1-1369:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1370:1-1389:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1394:1-1417:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1418:1-1437:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1441:1-1464:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1465:1-1484:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1485:1-1509:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1519:1-1587:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1588:1-1656:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1657:1-1712:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1722:1-1790:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1791:1-1846:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2474:1-2484:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2563:1-2574:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2575:1-2586:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2669:1-2683:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2705:1-2720:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2797:1-2817:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2818:1-2833:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2836:1-2856:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2857:1-2872:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:54-54)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2010-2010)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:231-231)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2234-2234)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1871-1871)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2306-2306)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2345..2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2345-2346)
  on line 2353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2353-2353)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2138..2140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2138-2140)
  on lines 2142..2143 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2142-2143)
  on lines 2147..2150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2147-2150)
  on lines 2152..2154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2152-2154)
  on lines 2156..2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2156-2157)
  on lines 2161..2164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2161-2164)
  on lines 2166..2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2166-2168)
  on lines 2170..2171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2170-2171)
  on lines 2175..2176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2175-2176)
  on line 2180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2180-2180)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1960..1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1960-1961)
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1965-1965)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2031..2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2031-2033)
  on lines 2035..2036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2035-2036)
  on lines 2040..2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2040-2043)
  on lines 2045..2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2045-2047)
  on lines 2049..2050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2049-2050)
  on lines 2054..2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2054-2057)
  on lines 2059..2061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2059-2061)
  on lines 2063..2064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2063-2064)
  on lines 2068..2069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2068-2069)
  on line 2073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2073-2073)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1918-1918)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2921..2922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2921-2922)
  on line 2928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2928-2928)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2732..2733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2732-2733)
  on line 2739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2739-2739)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2695..2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2695-2696)
  on line 2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2702-2702)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2995..2996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2995-2996)
  on line 3002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:3002-3002)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2769..2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2769-2770)
  on line 2776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2776-2776)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1132-1132)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1141-1141)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2884..2885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2884-2885)
  on line 2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2891-2891)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1158..1159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1158-1159)
  on line 1166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1166-1166)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:207-207)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:187-187)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2958..2959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2958-2959)
  on line 2965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2965-2965)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 3032..3033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:3032-3033)
  on line 3039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:3039-3039)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1123-1123)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1879-1879)
  on lines 1884..1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1884-1885)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2314-2314)
  on lines 2319..2320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2319-2320)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2245..2246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2245-2246)
  on lines 2256..2257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2256-2257)
  on lines 2267..2268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2267-2268)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2084..2085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2084-2085)
  on lines 2095..2096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2095-2096)
  on lines 2106..2107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2106-2107)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2939-2939)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2750-2750)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2902-2902)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:3050-3050)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2976-2976)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 3013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:3013-3013)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2787-2787)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:864-864)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 623
  dead: 580 (457 in uncalled functions)
  total lines: 1203
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2264:13-2264:23)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1157:9-1157:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2081:9-2081:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2092:11-2092:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2883:9-2883:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2313:7-2313:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1878:7-1878:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2102:11-2102:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2316:9-2316:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2103:13-2103:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1881:9-1881:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2133:7-2133:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2901:9-2901:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2134:9-2134:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2344:11-2344:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2920:9-2920:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:650:10-650:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2938:9-2938:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2694:9-2694:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2366:11-2366:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1931:11-1931:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2957:9-2957:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1956:11-1956:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2975:9-2975:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2731:9-2731:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2994:9-2994:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:1978:11-1978:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2749:9-2749:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:3012:9-3012:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2768:9-2768:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:3031:9-3031:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2026:7-2026:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2027:9-2027:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2786:9-2786:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:3049:9-3049:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2518:7-2518:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2242:9-2242:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2253:11-2253:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product33.cil.c:2263:11-2263:22)
[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)
