./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec6_product16.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec6_product16.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1934:3-1955:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1991:3-2016:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2076:5-2096: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:186:1-196:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:275:1-286:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:287:1-298:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:385:1-399:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:403:1-428:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:429:1-448:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:453:1-476:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:477:1-496:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:500:1-523:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:524:1-543:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:544:1-568:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:578:1-646:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:647:1-715:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:716:1-771:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:781:1-849:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:850:1-905:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:909:1-932:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:933:1-952:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1458:1-1472:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1494:1-1509:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1586:1-1606:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1607:1-1622:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1625:1-1645:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1646:1-1661:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1738:1-1756:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1757:1-1772:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1775:1-1793:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1794:1-1809:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1812:1-1830:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1831:1-1846:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1863:1-1908:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1909:1-1964:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1965:1-2024:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2027:1-2129:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2130:1-2175:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2176:1-2221:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2224:1-2233:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2554:1-2562:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2580:1-2594:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2793:1-2807:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1853-1853)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1069-1069)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2575-2575)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1252..1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1252-1253)
  on lines 1275..1277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1275-1277)
  on lines 1279..1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1279-1281)
  on lines 1283..1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1283-1284)
  on line 1293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1293-1293)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1349..1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1349-1350)
  on line 1365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1365-1365)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1404..1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1404-1405)
  on line 1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1412-1412)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1197..1199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1197-1199)
  on lines 1201..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1201-1202)
  on lines 1206..1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1206-1209)
  on lines 1211..1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1211-1213)
  on lines 1215..1216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1215-1216)
  on lines 1220..1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1220-1223)
  on lines 1225..1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1225-1227)
  on lines 1229..1230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1229-1230)
  on lines 1234..1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1234-1235)
  on line 1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1239-1239)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1019..1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1019-1020)
  on line 1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1024-1024)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1090..1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1090-1092)
  on lines 1094..1095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1094-1095)
  on lines 1099..1102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1099-1102)
  on lines 1104..1106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1104-1106)
  on lines 1108..1109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1108-1109)
  on lines 1113..1116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1113-1116)
  on lines 1118..1120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1118-1120)
  on lines 1122..1123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1122-1123)
  on lines 1127..1128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1127-1128)
  on line 1132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1132-1132)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 961..962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:961-962)
  on line 977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:977-977)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1710..1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1710-1711)
  on line 1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1717-1717)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1521..1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1521-1522)
  on line 1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1528-1528)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1484..1485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1484-1485)
  on line 1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1491-1491)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1558..1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1558-1559)
  on line 1565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1565-1565)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2846-2846)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2855-2855)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1673..1674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1673-1674)
  on line 1680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1680-1680)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2880-2880)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2551-2551)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2531-2531)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2837-2837)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1373-1373)
  on lines 1378..1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1378-1379)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1304..1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1304-1305)
  on lines 1315..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1315-1316)
  on lines 1326..1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1326-1327)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1143..1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1143-1144)
  on lines 1154..1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1154-1155)
  on lines 1165..1166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1165-1166)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1728-1728)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1539-1539)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1691-1691)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1576-1576)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2254-2254)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 505
  dead: 637 (518 in uncalled functions)
  total lines: 1142
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1672:9-1672:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1403:11-1403:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1690:9-1690:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1425:11-1425:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:990:11-990:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1709:9-1709:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:2297:10-2297:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1015:11-1015:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1727:9-1727:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1483:9-1483:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1251:11-1251:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1037:11-1037:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1520:9-1520:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1274:11-1274:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1085:7-1085:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1086:9-1086:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1538:9-1538:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1557:9-1557:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1301:9-1301:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1575:9-1575:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1312:11-1312:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1322:11-1322:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1323:13-1323:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1348:7-1348:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1140:9-1140:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:230:7-230:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1151:11-1151:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1372:7-1372:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1161:11-1161:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1375:9-1375:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1162:13-1162:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1192:7-1192:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:960:7-960:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product16.cil.c:1193:9-1193: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
