./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_spec9_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_spec9_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_spec9_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_spec9_product30.cil.c:2523:3-2544:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2580:3-2605:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2665:5-2685: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:186:1-196:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:275:1-286:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:287:1-298:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:556:1-570:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:745:1-772:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:773:1-791:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:792:1-810:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:811:1-824:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:854:1-862:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:895:1-909:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:913:1-938:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:939:1-958:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:963:1-986:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:987:1-1006:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1010:1-1033:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1034:1-1053:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1054:1-1078:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1088:1-1156:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1157:1-1225:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1226:1-1281:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1291:1-1359:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1360:1-1415:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1854:1-1877:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1878:1-1897:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1947:1-1956:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2033:1-2047:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2056:1-2070:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2073:1-2091:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2092:1-2107:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2184:1-2204:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2205:1-2220:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2223:1-2243:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2244:1-2259:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2410:1-2428:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2452:1-2497:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2498:1-2553:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2554:1-2613:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2616:1-2718:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2719:1-2764:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2765:1-2810:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1986-1986)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1579-1579)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:875-875)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1785..1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1785-1787)
  on lines 1789..1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1789-1791)
  on lines 1793..1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1793-1794)
  on line 1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1803-1803)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 1432..1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1432-1433)
  on line 1440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1440-1440)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1914..1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1914-1915)
  on line 1922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1922-1922)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1707..1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1707-1709)
  on lines 1711..1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1711-1712)
  on lines 1716..1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1716-1719)
  on lines 1721..1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1721-1723)
  on lines 1725..1726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1725-1726)
  on lines 1730..1733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1730-1733)
  on lines 1735..1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1735-1737)
  on lines 1739..1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1739-1740)
  on lines 1744..1745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1744-1745)
  on line 1749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1749-1749)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1529..1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1529-1530)
  on line 1534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1534-1534)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1600..1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1600-1602)
  on lines 1604..1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1604-1605)
  on lines 1609..1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1609-1612)
  on lines 1614..1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1614-1616)
  on lines 1618..1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1618-1619)
  on lines 1623..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1623-1626)
  on lines 1628..1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1628-1630)
  on lines 1632..1633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1632-1633)
  on lines 1637..1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1637-1638)
  on line 1642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1642-1642)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1479..1480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1479-1480)
  on line 1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1487-1487)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2308..2309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2308-2309)
  on line 2315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2315-2315)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2119..2120 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2119-2120)
  on line 2126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2126-2126)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2382..2383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2382-2383)
  on line 2389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2389-2389)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2156..2157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2156-2157)
  on line 2163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2163-2163)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:609-609)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:618-618)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2271..2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2271-2272)
  on line 2278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2278-2278)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 635..636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:635-636)
  on line 643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:643-643)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:851-851)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:831-831)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2345..2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2345-2346)
  on line 2352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2352-2352)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:600-600)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1448-1448)
  on lines 1453..1454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1453-1454)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1814..1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1814-1815)
  on lines 1825..1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1825-1826)
  on lines 1836..1837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1836-1837)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1653..1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1653-1654)
  on lines 1664..1665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1664-1665)
  on lines 1675..1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1675-1676)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2326-2326)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2137 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2137-2137)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2289-2289)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2437-2437)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2363 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2363-2363)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2400-2400)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2174 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2174-2174)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1977-1977)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 533
  dead: 653 (528 in uncalled functions)
  total lines: 1186
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2851:10-2851:11)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:634:9-634:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2288:9-2288:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1784:11-1784:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2307:9-2307:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1595:7-1595:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1596:9-1596:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2325:9-2325:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1811:9-1811:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2344:9-2344:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1822:11-1822:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1832:11-1832:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1833:13-1833:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2362:9-2362:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2118:9-2118:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2381:9-2381:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1650:9-1650:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2136:9-2136:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1431:11-1431:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1661:11-1661:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2399:9-2399:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2155:9-2155:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1447:7-1447:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1671:11-1671:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1672:13-1672:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1450:9-1450:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2173:9-2173:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1702:7-1702:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1703:9-1703:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2436:9-2436:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1913:11-1913:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1478:11-1478:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1935:11-1935:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1500:11-1500:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:230:7-230:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1525:11-1525:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:2270:9-2270:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product30.cil.c:1547:11-1547: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)
