./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_product22.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_product22.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_product22.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_product22.cil.c:587:3-608:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:644:3-669:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:729:5-749: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 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:71:1-85:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:107:1-122:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:199:1-219:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:220:1-235:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:238:1-258:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:259:1-274:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:351:1-369:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:370:1-385:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:388:1-406:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:407:1-422:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:425:1-443:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:444:1-459:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:476:1-485:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:516:1-561:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:562:1-617:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:618:1-677:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:680:1-782:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:783:1-828:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:829:1-874:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:878:1-892:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:981:1-995:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:999:1-1024:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1025:1-1044:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1049:1-1072:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1073:1-1092:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1096:1-1119:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1120:1-1139:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1140:1-1164:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1174:1-1242:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1243:1-1311:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1312:1-1367:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1377:1-1445:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1446:1-1501:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2364:1-2374:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2453:1-2464:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2465:1-2476:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2723:1-2737:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2929:1-2937:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:949-949)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1665-1665)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2950-2950)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1848..1849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1848-1849)
  on lines 1871..1873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1871-1873)
  on lines 1875..1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1875-1877)
  on lines 1879..1880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1879-1880)
  on line 1889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1889-1889)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1526-1526)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1961-1961)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2000..2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2000-2001)
  on line 2008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2008-2008)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1793..1795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1793-1795)
  on lines 1797..1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1797-1798)
  on lines 1802..1805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1802-1805)
  on lines 1807..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1807-1809)
  on lines 1811..1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1811-1812)
  on lines 1816..1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1816-1819)
  on lines 1821..1823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1821-1823)
  on lines 1825..1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1825-1826)
  on lines 1830..1831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1830-1831)
  on line 1835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1835-1835)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1615..1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1615-1616)
  on line 1620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1620-1620)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1686..1688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1686-1688)
  on lines 1690..1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1690-1691)
  on lines 1695..1698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1695-1698)
  on lines 1700..1702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1700-1702)
  on lines 1704..1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1704-1705)
  on lines 1709..1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1709-1712)
  on lines 1714..1716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1714-1716)
  on lines 1718..1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1718-1719)
  on lines 1723..1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1723-1724)
  on line 1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1728-1728)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1573-1573)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 323..324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:323-324)
  on line 330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:330-330)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 134..135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:134-135)
  on line 141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:141-141)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 97..98 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:97-98)
  on line 104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:104-104)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 171..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:171-172)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:178-178)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2776-2776)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2785-2785)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 286..287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:286-287)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:293-293)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2810-2810)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2926-2926)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2906-2906)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2767-2767)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1534-1534)
  on lines 1539..1540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1539-1540)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1969-1969)
  on lines 1974..1975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1974-1975)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1900..1901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1900-1901)
  on lines 1911..1912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1911-1912)
  on lines 1922..1923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1922-1923)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1739..1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1739-1740)
  on lines 1750..1751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1750-1751)
  on lines 1761..1762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1761-1762)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:341-341)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:152-152)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:304-304)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:189-189)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:506-506)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 543
  dead: 618 (499 in uncalled functions)
  total lines: 1161
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1919:13-1919:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1736:9-1736:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1747:11-1747:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1968:7-1968:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1533:7-1533:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1757:11-1757:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1971:9-1971:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1758:13-1758:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1536:9-1536:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1788:7-1788:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1789:9-1789:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:285:9-285:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1999:11-1999:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:303:9-303:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2021:11-2021:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1586:11-1586:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:322:9-322:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:340:9-340:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1611:11-1611:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:96:9-96: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_product22.cil.c:2081:10-2081:11)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1847:11-1847:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1633:11-1633:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:133:9-133:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1870:11-1870:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:2408:7-2408:10)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1681:7-1681:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1682:9-1682:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:170:9-170:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1897:9-1897:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:188:9-188:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1908:11-1908:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product22.cil.c:1918:11-1918:22)
[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
