./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_product12.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_product12.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_product12.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_product12.cil.c:288:3-309:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:345:3-370:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:430:5-450: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_spec6_product12.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:110:1-137:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:138:1-156:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:157:1-165:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:166:1-185:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:186:1-194:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:217:1-262:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:263:1-318:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:319:1-378:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:381:1-483:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:484:1-529:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:530:1-575:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:697:1-707:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:786:1-797:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:798:1-809:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:887:1-901:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:905:1-930:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:931:1-950:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:955:1-978:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:979:1-998:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1002:1-1025:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1026:1-1045:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1046:1-1070:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1080:1-1148:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1149:1-1217:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1218:1-1273:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1283:1-1351:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1352:1-1407:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1411:1-1434:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1435:1-1454:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1846:1-1869:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1870:1-1889:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1953:1-1967:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1970:1-1988:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1989:1-2004:1)
[Warning][Deadcode] Function 'getEmailFrom' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2007:1-2025:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2081:1-2101:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2102:1-2117:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2120:1-2140:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2141:1-2156:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2233:1-2251:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2252:1-2267:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2270:1-2288:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2289:1-2304:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2307:1-2325:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2326:1-2341:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2483:1-2497:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2511:1-2520:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2530:1-2538:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2539:1-2547:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2631:1-2645:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2348-2348)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 689..691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:689-691)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1571-1571)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:207-207)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1754..1755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1754-1755)
  on lines 1762..1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1762-1765)
  on lines 1767..1769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1767-1769)
  on lines 1771..1772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1771-1772)
  on lines 1776..1779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1776-1779)
  on lines 1781..1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1781-1783)
  on lines 1785..1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1785-1786)
  on lines 1790..1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1790-1791)
  on line 1795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1795-1795)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1901..1903 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1901-1903)
  on lines 1905..1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1905-1907)
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1909-1910)
  on line 1914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1914-1914)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1699..1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1699-1701)
  on lines 1703..1704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1703-1704)
  on lines 1708..1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1708-1711)
  on lines 1713..1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1713-1715)
  on lines 1717..1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1717-1718)
  on lines 1722..1725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1722-1725)
  on lines 1727..1729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1727-1729)
  on lines 1731..1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1731-1732)
  on lines 1736..1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1736-1737)
  on line 1741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1741-1741)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1521..1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1521-1522)
  on line 1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1526-1526)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1592..1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1592-1594)
  on lines 1596..1597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1596-1597)
  on lines 1601..1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1601-1604)
  on lines 1606..1608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1606-1608)
  on lines 1610..1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1610-1611)
  on lines 1615..1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1615-1618)
  on lines 1620..1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1620-1622)
  on lines 1624..1625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1624-1625)
  on lines 1629..1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1629-1630)
  on line 1634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1634-1634)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1463..1464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1463-1464)
  on lines 1470..1472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1470-1472)
  on lines 1474..1475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1474-1475)
  on line 1479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1479-1479)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2204..2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2204-2206)
  on lines 2208..2209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2208-2209)
  on line 2212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2212-2212)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2052..2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2052-2054)
  on lines 2056..2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2056-2057)
  on line 2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2060-2060)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2167..2169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2167-2169)
  on lines 2171..2172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2171-2172)
  on line 2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2175-2175)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2570-2570)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2527-2527)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1806..1807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1806-1807)
  on lines 1817..1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1817-1818)
  on lines 1828..1829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1828-1829)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1645..1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1645-1646)
  on lines 1656..1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1656-1657)
  on lines 1667..1668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1667-1668)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 2222..2223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2222-2223)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2033..2034 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2033-2034)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 2185..2186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2185-2186)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2070..2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2070-2071)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:94-94)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 376
  dead: 738 (596 in uncalled functions)
  total lines: 1114
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1753:11-1753:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1539:11-1539:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2030:7-2030:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1587:7-1587:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1588:9-1588:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2048:7-2048:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1803:9-1803:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2067:7-2067:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1814:11-1814:21)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:685:7-685:14)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1824:11-1824:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1825:13-1825:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1642:9-1642:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2686:10-2686:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1653:11-1653:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:741:7-741:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1663:11-1663:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1664:13-1664:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1897:7-1897:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1694:7-1694:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1695:9-1695:19)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1462:7-1462:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2163:7-2163:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1466:9-1466:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2182:7-2182:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1927:11-1927:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2200:7-2200:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1492:11-1492:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:2219:7-2219:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1517:11-1517:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product12.cil.c:1748:7-1748:18)
[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
