./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_spec3_product18.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_spec3_product18.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1548:3-1569:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1605:3-1630:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1690:5-1710: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_spec3_product18.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:127:1-141:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:145:1-170:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:171:1-190:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:195:1-218:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:219:1-238:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:242:1-265:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:266:1-285:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:286:1-310:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:320:1-388:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:389:1-457:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:458:1-513:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:523:1-591:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:592:1-647:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1086:1-1109:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1110:1-1129:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1293:1-1303:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1382:1-1393:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1394:1-1405:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1477:1-1522:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1523:1-1578:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1579:1-1638:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1641:1-1743:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1744:1-1789:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1790:1-1835:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1957:1-1971:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2161:1-2175:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2178:1-2196:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2197:1-2212:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2289:1-2309:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2310:1-2325:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2328:1-2348:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2349:1-2364:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2367:1-2385:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2386:1-2401:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2404:1-2422:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2423:1-2438:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2515:1-2533:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2827:1-2854:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2855:1-2873:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2874:1-2887:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2897:1-2905:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2923:1-2937:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1842-1842)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:811-811)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2918-2918)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1017..1019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1017-1019)
  on lines 1021..1023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1021-1023)
  on lines 1025..1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1025-1026)
  on line 1035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1035-1035)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 664..665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:664-665)
  on line 672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:672-672)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1146..1147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1146-1147)
  on line 1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1154-1154)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 939..941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:939-941)
  on lines 943..944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:943-944)
  on lines 948..951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:948-951)
  on lines 953..955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:953-955)
  on lines 957..958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:957-958)
  on lines 962..965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:962-965)
  on lines 967..969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:967-969)
  on lines 971..972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:971-972)
  on lines 976..977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:976-977)
  on line 981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:981-981)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 761..762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:761-762)
  on line 766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:766-766)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 832..834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:832-834)
  on lines 836..837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:836-837)
  on lines 841..844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:841-844)
  on lines 846..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:846-848)
  on lines 850..851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:850-851)
  on lines 855..858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:855-858)
  on lines 860..862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:860-862)
  on lines 864..865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:864-865)
  on lines 869..870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:869-870)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:874-874)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 711..712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:711-712)
  on line 719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:719-719)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2224..2225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2224-2225)
  on line 2231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2231-2231)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2487..2488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2487-2488)
  on line 2494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2494-2494)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2261..2262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2261-2262)
  on line 2268 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2268-2268)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2010-2010)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2019-2019)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2036..2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2036-2037)
  on line 2044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2044-2044)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2894-2894)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2450..2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2450-2451)
  on line 2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2457-2457)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2001-2001)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:680-680)
  on lines 685..686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:685-686)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1046..1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1046-1047)
  on lines 1057..1058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1057-1058)
  on lines 1068..1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1068-1069)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 885..886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:885-886)
  on lines 896..897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:896-897)
  on lines 907..908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:907-908)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2242-2242)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2542-2542)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2468-2468)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2505-2505)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2279-2279)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:94-94)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2122-2122)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 485
  dead: 665 (548 in uncalled functions)
  total lines: 1150
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:882:9-882:19)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2035:9-2035:21)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:663:11-663:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:893:11-893:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:679:7-679:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:903:11-903:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:904:13-904:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:682:9-682:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:934:7-934:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:935:9-935:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1145:11-1145:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:710:11-710:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2112:7-2112:10)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2648:10-2648:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1167:11-1167:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:732:11-732:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:757:11-757:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:779:11-779:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2449:9-2449:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2467:9-2467:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2223:9-2223:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1016:11-1016:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:827:7-827:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:828:9-828:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2486:9-2486:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2241:9-2241:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1337:7-1337:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2504:9-2504:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2260:9-2260:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1043:9-1043:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1054:11-1054:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2278:9-2278:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1064:11-1064:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:1065:13-1065:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product18.cil.c:2541:9-2541:20)
[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
