./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_spec4_product19.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_spec4_product19.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_spec4_product19.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_spec4_product19.cil.c:214:3-235:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:271:3-296:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:356:5-376: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 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:103:1-112:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:143:1-188:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:189:1-244:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:245:1-304:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:307:1-409:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:410:1-455:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:456:1-501:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:625:1-635:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:714:1-725:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:726:1-737:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1138:1-1152:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1321:1-1335:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1410:1-1418:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1451:1-1465:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1469:1-1494:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1495:1-1514:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1519:1-1542:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1543:1-1562:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1566:1-1589:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1590:1-1609:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1610:1-1634:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1644:1-1712:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1713:1-1781:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1782:1-1837:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1847:1-1915:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1916:1-1971:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1975:1-1998:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1999:1-2018:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2513:1-2527:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2549:1-2564:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2641:1-2661:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2662:1-2677:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2680:1-2700:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2701:1-2716:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2719:1-2737:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2738:1-2753:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2756:1-2774:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2775:1-2790:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:54-54)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2135-2135)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1431-1431)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2313..2315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2313-2315)
  on lines 2317..2319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2317-2319)
  on lines 2321..2322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2321-2322)
  on line 2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2359-2359)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2415..2416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2415-2416)
  on line 2431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2431-2431)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2470..2471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2470-2471)
  on line 2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2478-2478)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2263..2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2263-2265)
  on lines 2267..2268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2267-2268)
  on lines 2272..2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2272-2275)
  on lines 2277..2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2277-2279)
  on lines 2281..2282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2281-2282)
  on lines 2286..2289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2286-2289)
  on lines 2291..2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2291-2293)
  on lines 2295..2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2295-2296)
  on lines 2300..2301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2300-2301)
  on line 2305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2305-2305)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2085..2086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2085-2086)
  on line 2090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2090-2090)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2156..2158 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2156-2158)
  on lines 2160..2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2160-2161)
  on lines 2165..2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2165-2168)
  on lines 2170..2172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2170-2172)
  on lines 2174..2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2174-2175)
  on lines 2179..2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2179-2182)
  on lines 2184..2186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2184-2186)
  on lines 2188..2189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2188-2189)
  on lines 2193..2194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2193-2194)
  on line 2198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2198-2198)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2035..2036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2035-2036)
  on line 2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2043-2043)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2576..2577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2576-2577)
  on line 2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2583-2583)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2539..2540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2539-2540)
  on line 2546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2546-2546)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2839..2840 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2839-2840)
  on line 2846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2846-2846)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2613..2614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2613-2614)
  on line 2620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2620-2620)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1191-1191)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1200-1200)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1217..1218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1217-1218)
  on line 1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1225-1225)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1407-1407)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2802..2803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2802-2803)
  on line 2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2809-2809)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2876..2877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2876-2877)
  on line 2883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2883-2883)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1182-1182)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2439-2439)
  on lines 2444..2445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2444-2445)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2370..2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2370-2371)
  on lines 2381..2382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2381-2382)
  on lines 2392..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2392-2393)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2209..2210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2209-2210)
  on lines 2220..2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2220-2221)
  on lines 2231..2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2231-2232)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2594-2594)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2894-2894)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2820-2820)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2857-2857)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2631-2631)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:133-133)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1294-1294)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 513
  dead: 627 (504 in uncalled functions)
  total lines: 1140
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2819:9-2819:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2575:9-2575:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2838:9-2838:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2151:7-2151:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2152:9-2152:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2593:9-2593:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1216:9-1216:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2856:9-2856:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2612:9-2612:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2367:9-2367:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2875:9-2875:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2630:9-2630:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2378:11-2378:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:669:7-669:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2388:11-2388:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2893:9-2893:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2389:13-2389:23)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:1284:7-1284:10)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2414:7-2414:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2206:9-2206:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2217:11-2217:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2438:7-2438:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2227:11-2227:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2441:9-2441:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2228:13-2228:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2258:7-2258:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2259:9-2259:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2469:11-2469:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2034:11-2034:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2491:11-2491:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2056:11-2056:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:842:10-842:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2081:11-2081:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2538:9-2538:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2312:7-2312:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2801:9-2801:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product19.cil.c:2103:11-2103:22)
[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
