./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_spec4_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_spec4_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_spec4_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_spec4_product30.cil.c:2470:3-2491:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2527:3-2552:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2612:5-2632: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_spec4_product30.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:100:1-114:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:314:1-328:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:503:1-530:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:531:1-549:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:550:1-568:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:569:1-582:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:612:1-620:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:660:1-674:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:678:1-703:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:704:1-723:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:728:1-751:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:752:1-771:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:775:1-798:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:799:1-818:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:819:1-843:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:853:1-921:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:922:1-990:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:991:1-1046:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1056:1-1124:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1125:1-1180:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1619:1-1642:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1643:1-1662:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1718:1-1732:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1735:1-1753:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1754:1-1769:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1846:1-1866:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1867:1-1882:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1885:1-1905:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1906:1-1921:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2072:1-2090:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2215:1-2225:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2304:1-2315:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2316:1-2327:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2399:1-2444:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2445:1-2500:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2501:1-2560:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2563:1-2665:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2666:1-2711:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2712:1-2757:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:3008-3008)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1344-1344)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:633-633)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1550..1552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1550-1552)
  on lines 1554..1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1554-1556)
  on lines 1558..1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1558-1559)
  on line 1568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1568-1568)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 1197..1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1197-1198)
  on line 1205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1205-1205)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1679..1680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1679-1680)
  on line 1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1687-1687)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1472..1474 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1472-1474)
  on lines 1476..1477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1476-1477)
  on lines 1481..1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1481-1484)
  on lines 1486..1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1486-1488)
  on lines 1490..1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1490-1491)
  on lines 1495..1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1495-1498)
  on lines 1500..1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1500-1502)
  on lines 1504..1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1504-1505)
  on lines 1509..1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1509-1510)
  on line 1514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1514-1514)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1294..1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1294-1295)
  on line 1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1299-1299)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1365..1367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1365-1367)
  on lines 1369..1370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1369-1370)
  on lines 1374..1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1374-1377)
  on lines 1379..1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1379-1381)
  on lines 1383..1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1383-1384)
  on lines 1388..1391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1388-1391)
  on lines 1393..1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1393-1395)
  on lines 1397..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1397-1398)
  on lines 1402..1403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1402-1403)
  on line 1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1407-1407)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1244..1245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1244-1245)
  on line 1252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1252-1252)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1970..1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1970-1971)
  on line 1977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1977-1977)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1781..1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1781-1782)
  on line 1788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1788-1788)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2044..2045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2044-2045)
  on line 2051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2051-2051)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1818..1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1818-1819)
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1825-1825)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:367-367)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 376 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:376-376)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1933..1934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1933-1934)
  on line 1940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1940-1940)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 393..394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:393-394)
  on line 401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:401-401)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:609-609)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:589-589)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2007..2008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2007-2008)
  on line 2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2014-2014)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:358-358)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1213-1213)
  on lines 1218..1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1218-1219)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1579..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1579-1580)
  on lines 1590..1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1590-1591)
  on lines 1601..1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1601-1602)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1418..1419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1418-1419)
  on lines 1429..1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1429-1430)
  on lines 1440..1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1440-1441)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1988-1988)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1799-1799)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1951-1951)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2099-2099)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2025-2025)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2062-2062)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1836-1836)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:94-94)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 525
  dead: 653 (528 in uncalled functions)
  total lines: 1178
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1950:9-1950:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1700:11-1700:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1265:11-1265:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2259:7-2259:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1969:9-1969:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1290:11-1290:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1987:9-1987:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2006:9-2006:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1312:11-1312:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2024:9-2024:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:392:9-392:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1780:9-1780:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1549:11-1549:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2043:9-2043:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1360:7-1360:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1361:9-1361:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1798:9-1798:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2061:9-2061:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1817:9-1817:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1576:9-1576:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1835:9-1835:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1587:11-1587:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1597:11-1597:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2098:9-2098:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1598:13-1598:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1415:9-1415:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1196:11-1196:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1426:11-1426:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1212:7-1212:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1436:11-1436:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1437:13-1437:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1215:9-1215:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1467:7-1467:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1468:9-1468:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:2826:10-2826:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1932:9-1932:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1678:11-1678:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product30.cil.c:1243:11-1243: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)
