./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_spec27_product27.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_spec27_product27.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_spec27_product27.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_spec27_product27.cil.c:245:3-266:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:302:3-327:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:387:5-407: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:143:1-151:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:174:1-219:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:220:1-275:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:276:1-335:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:338:1-440:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:441:1-486:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:487:1-532:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:548:1-562:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:584:1-599:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:676:1-696:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:697:1-712:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:715:1-735:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:736:1-751:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:754:1-772:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:773:1-788:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:791:1-809:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:810:1-825:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1200:1-1214:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1218:1-1243:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1244:1-1263:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1268:1-1291:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1292:1-1311:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1359:1-1383:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1393:1-1461:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1462:1-1530:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2358:1-2368:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2447:1-2458:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2459:1-2470:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2560:1-2569:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2635:1-2649:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2811:1-2825:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2599-2599)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1884-1884)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:164-164)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2108-2108)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1609..1611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1609-1611)
  on lines 1613..1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1613-1614)
  on lines 1619..1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1619-1622)
  on lines 1624..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1624-1626)
  on lines 1628..1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1628-1630)
  on lines 1632..1633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1632-1633)
  on lines 1638..1641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1638-1641)
  on lines 1643..1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1643-1645)
  on lines 1647..1649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1647-1649)
  on lines 1651..1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1651-1652)
  on lines 1657..1658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1657-1658)
  on line 1662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1662-1662)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1336-1336)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1745-1745)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2180-2180)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2227-2227)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2012..2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2012-2014)
  on lines 2016..2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2016-2017)
  on lines 2021..2024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2021-2024)
  on lines 2026..2028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2026-2028)
  on lines 2030..2031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2030-2031)
  on lines 2035..2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2035-2038)
  on lines 2040..2042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2040-2042)
  on lines 2044..2045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2044-2045)
  on lines 2049..2050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2049-2050)
  on line 2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2054-2054)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1834..1835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1834-1835)
  on line 1839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1839-1839)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1905..1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1905-1907)
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1909-1910)
  on lines 1914..1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1914-1917)
  on lines 1919..1921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1919-1921)
  on lines 1923..1924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1923-1924)
  on lines 1928..1931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1928-1931)
  on lines 1933..1935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1933-1935)
  on lines 1937..1938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1937-1938)
  on lines 1942..1943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1942-1943)
  on line 1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1947-1947)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1792-1792)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 611..612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:611-612)
  on line 618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:618-618)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 574..575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:574-575)
  on line 581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:581-581)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 874..875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:874-875)
  on line 881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:881-881)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 648..649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:648-649)
  on line 655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:655-655)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2864-2864)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2873-2873)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2890..2891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2890-2891)
  on line 2898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2898-2898)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:140-140)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 837..838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:837-838)
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:844-844)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 911..912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:911-912)
  on line 918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:918-918)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2855-2855)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1676..1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1676-1677)
  on lines 1684..1686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1684-1686)
  on lines 1688..1689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1688-1689)
  on lines 1691..1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1691-1692)
  on lines 1699..1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1699-1701)
  on lines 1703..1704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1703-1704)
  on lines 1706..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1706-1707)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1539..1540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1539-1540)
  on lines 1542..1543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1542-1543)
  on lines 1550..1552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1550-1552)
  on lines 1554..1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1554-1555)
  on lines 1557..1558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1557-1558)
  on lines 1565..1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1565-1567)
  on lines 1569..1570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1569-1570)
  on lines 1572..1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1572-1573)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1346..1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1346-1347)
  on lines 1349..1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1349-1350)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1753-1753)
  on lines 1758..1759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1758-1759)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2188-2188)
  on lines 2193..2194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2193-2194)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2119..2120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2119-2120)
  on lines 2130..2131 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2130-2131)
  on lines 2141..2142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2141-2142)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1958..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1958-1959)
  on lines 1969..1970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1969-1970)
  on lines 1980..1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1980-1981)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:629-629)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:929-929)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:855-855)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:892-892)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:666-666)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2590-2590)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2989-2989)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 626
  dead: 567 (383 in uncalled functions)
  total lines: 1193
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1955:9-1955:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1966:11-1966:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1535:7-1535:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2187:7-2187:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1536:9-1536:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1343:7-1343:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1752:7-1752:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1976:11-1976:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:573:9-573:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2190:9-2190:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1977:13-1977:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1755:9-1755:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:836:9-836:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2007:7-2007:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2008:9-2008:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:854:9-854:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:610:9-610:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2889:9-2889:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:873:9-873:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1600:7-1600:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2240:11-2240:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:628:9-628:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1805:11-1805:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1605:11-1605:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:891:9-891:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:647:9-647:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1830:11-1830:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:910:9-910:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:665:9-665:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:928:9-928:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1852:11-1852:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2979:7-2979:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1900:7-1900:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1901:9-1901:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:988:10-988:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1669:7-1669:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:1673:11-1673:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2402:7-2402:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2116:9-2116:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2127:11-2127:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2137:11-2137:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product27.cil.c:2138:13-2138:23)
[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
