./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_spec1_product22.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_spec1_product22.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_product22.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_product22.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:268:5-288: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:514:1-522:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:769:1-783:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:800:1-814:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:836:1-851:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:928:1-948:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:949:1-964:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:967:1-987:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:988:1-1003:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1080:1-1098:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1099:1-1114:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1117:1-1135:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1136:1-1151:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1154:1-1172:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1173:1-1188:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1194:1-1203:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1370:1-1380:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1459:1-1470:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1471:1-1482:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1587:1-1601:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1605:1-1630:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1631:1-1650:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1655:1-1678:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1679:1-1698:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1702:1-1725:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1726:1-1745:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1746:1-1770:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1780:1-1848:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1849:1-1917:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1918:1-1973:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1983:1-2051:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2052:1-2107:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2805:1-2819:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1563-1563)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2271 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2271-2271)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:535-535)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2454..2455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2454-2455)
  on lines 2477..2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2477-2479)
  on lines 2481..2483 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2481-2483)
  on lines 2485..2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2485-2486)
  on line 2495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2495-2495)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2132-2132)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2567-2567)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2606..2607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2606-2607)
  on line 2614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2614-2614)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2399..2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2399-2401)
  on lines 2403..2404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2403-2404)
  on lines 2408..2411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2408-2411)
  on lines 2413..2415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2413-2415)
  on lines 2417..2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2417-2418)
  on lines 2422..2425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2422-2425)
  on lines 2427..2429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2427-2429)
  on lines 2431..2432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2431-2432)
  on lines 2436..2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2436-2437)
  on line 2441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2441-2441)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2221..2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2221-2222)
  on line 2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2226-2226)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2292..2294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2292-2294)
  on lines 2296..2297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2296-2297)
  on lines 2301..2304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2301-2304)
  on lines 2306..2308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2306-2308)
  on lines 2310..2311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2310-2311)
  on lines 2315..2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2315-2318)
  on lines 2320..2322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2320-2322)
  on lines 2324..2325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2324-2325)
  on lines 2329..2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2329-2330)
  on line 2334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2334-2334)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2179 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2179-2179)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1052..1053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1052-1053)
  on line 1059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1059-1059)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 863..864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:863-864)
  on line 870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:870-870)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 826..827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:826-827)
  on line 833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:833-833)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 900..901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:900-901)
  on line 907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:907-907)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2858-2858)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2867-2867)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1015..1016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1015-1016)
  on line 1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1022-1022)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2884..2885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2884-2885)
  on line 2892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2892-2892)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:511-511)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:491-491)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2849-2849)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2140-2140)
  on lines 2145..2146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2145-2146)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2575-2575)
  on lines 2580..2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2580-2581)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2506..2507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2506-2507)
  on lines 2517..2518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2517-2518)
  on lines 2528..2529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2528-2529)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2345..2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2345-2346)
  on lines 2356..2357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2356-2357)
  on lines 2367..2368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2367-2368)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1070-1070)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:881-881)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1033-1033)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:918-918)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1224-1224)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 530
  dead: 620 (499 in uncalled functions)
  total lines: 1150
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1051:9-1051:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2514:11-2514:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2524:11-2524:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2525:13-2525:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1069:9-1069:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:825:9-825:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2342:9-2342:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1414:7-1414:10)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:588:10-588:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2353:11-2353:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:862:9-862:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2574:7-2574:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2139:7-2139:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2363:11-2363:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2577:9-2577:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2364:13-2364:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2142:9-2142:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2883:9-2883:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2394:7-2394:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:880:9-880:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2395:9-2395:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2605:11-2605:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:899:9-899:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:917:9-917:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2627:11-2627:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2192:11-2192:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2217:11-2217:22)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2453:11-2453:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2239:11-2239:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2476:11-2476:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2287:7-2287:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2288:9-2288:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1014:9-1014:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:1032:9-1032:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product22.cil.c:2503:9-2503:19)
[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
