./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/email_spec6_product30.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/email_spec6_product30.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_product30.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_product30.cil.c:2459:3-2480:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2516:3-2541:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2601:5-2621:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:289:1-298:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:352:1-366:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:370:1-395:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:396:1-415:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:420:1-443:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:444:1-463:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:467:1-490:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:491:1-510:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:511:1-535:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:545:1-613:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:614:1-682:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:683:1-738:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:748:1-816:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:817:1-872:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1311:1-1334:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1335:1-1354:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1425:1-1439:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1442:1-1460:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1461:1-1476:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1553:1-1573:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1574:1-1589:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1592:1-1612:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1613:1-1628:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1779:1-1797:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1866:1-1880:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2061:1-2075:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2248:1-2275:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2276:1-2294:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2295:1-2313:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2314:1-2327:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2357:1-2365:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2388:1-2433:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2434:1-2489:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2490:1-2549:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2552:1-2654:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2655:1-2700:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2701:1-2746:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2845:1-2855:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2934:1-2945:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2946:1-2957:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:3028-3028)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1036-1036)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2378-2378)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1242..1244 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1242-1244)
  on lines 1246..1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1246-1248)
  on lines 1250..1251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1250-1251)
  on line 1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1260-1260)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 889..890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:889-890)
  on line 897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:897-897)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1371..1372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1371-1372)
  on line 1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1379-1379)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1164..1166 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1164-1166)
  on lines 1168..1169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1168-1169)
  on lines 1173..1176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1173-1176)
  on lines 1178..1180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1178-1180)
  on lines 1182..1183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1182-1183)
  on lines 1187..1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1187-1190)
  on lines 1192..1194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1192-1194)
  on lines 1196..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1196-1197)
  on lines 1201..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1201-1202)
  on line 1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1206-1206)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 986..987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:986-987)
  on line 991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:991-991)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1057..1059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1057-1059)
  on lines 1061..1062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1061-1062)
  on lines 1066..1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1066-1069)
  on lines 1071..1073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1071-1073)
  on lines 1075..1076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1075-1076)
  on lines 1080..1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1080-1083)
  on lines 1085..1087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1085-1087)
  on lines 1089..1090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1089-1090)
  on lines 1094..1095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1094-1095)
  on line 1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1099-1099)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 936..937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:936-937)
  on line 944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:944-944)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1677..1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1677-1678)
  on line 1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1684-1684)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1488..1489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1488-1489)
  on line 1495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1495-1495)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1751..1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1751-1752)
  on line 1758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1758-1758)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1525..1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1525-1526)
  on line 1532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1532-1532)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2114-2114)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2123-2123)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1640..1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1640-1641)
  on line 1647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1647-1647)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2148-2148)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2354-2354)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2334-2334)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1714..1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1714-1715)
  on line 1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1721-1721)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2105-2105)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:905-905)
  on lines 910..911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:910-911)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1271..1272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1271-1272)
  on lines 1282..1283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1282-1283)
  on lines 1293..1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1293-1294)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1110..1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1110-1111)
  on lines 1121..1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1121-1122)
  on lines 1132..1133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1132-1133)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1695-1695)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1506-1506)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1658-1658)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1806-1806)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1732-1732)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1769-1769)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1543-1543)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:319-319)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 538
  dead: 651 (528 in uncalled functions)
  total lines: 1189
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1118:11-1118:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:904:7-904:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1128:11-1128:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1129:13-1129:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:907:9-907:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1159:7-1159:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1160:9-1160:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1639:9-1639:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1370:11-1370:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:935:11-935:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1657:9-1657:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1392:11-1392:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:957:11-957:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1676:9-1676:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:2889:7-2889:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:982:11-982:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1694:9-1694:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1713:9-1713:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1004:11-1004:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1731:9-1731: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_product30.cil.c:97:10-97:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1487:9-1487:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1241:11-1241:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1750:9-1750:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1052:7-1052:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1053:9-1053:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1505:9-1505:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1768:9-1768:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1524:9-1524:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1268:9-1268:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1542:9-1542:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1279:11-1279:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1289:11-1289:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1805:9-1805:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1290:13-1290:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:1107:9-1107:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product30.cil.c:888:11-888:22)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
