./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_spec6_product35.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_spec6_product35.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_product35.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_product35.cil.c:2407:3-2428:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2464:3-2489:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2549:5-2569: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 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:327:1-341:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:654:1-664:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:743:1-754:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:755:1-766:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1236:1-1244:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1279:1-1293:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1297:1-1322:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1323:1-1342:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1347:1-1370:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1371:1-1390:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1438:1-1462:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1472:1-1540:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1541:1-1609:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2336:1-2381:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2382:1-2437:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2438:1-2497:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2500:1-2602:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2603:1-2648:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2649:1-2694:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2703:1-2717:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2739:1-2754:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2831:1-2851:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2852:1-2867:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2870:1-2890:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2891:1-2906:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3094:1-3108:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3111:1-3120:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1266-1266)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1963 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1963-1963)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1257 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1257-1257)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2187-2187)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1688..1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1688-1690)
  on lines 1692..1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1692-1693)
  on lines 1698..1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1698-1701)
  on lines 1703..1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1703-1705)
  on lines 1707..1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1707-1709)
  on lines 1711..1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1711-1712)
  on lines 1717..1720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1717-1720)
  on lines 1722..1724 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1722-1724)
  on lines 1726..1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1726-1728)
  on lines 1730..1731 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1730-1731)
  on lines 1736..1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1736-1737)
  on line 1741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1741-1741)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1415-1415)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1824-1824)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2259-2259)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2306-2306)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2091..2093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2091-2093)
  on lines 2095..2096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2095-2096)
  on lines 2100..2103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2100-2103)
  on lines 2105..2107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2105-2107)
  on lines 2109..2110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2109-2110)
  on lines 2114..2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2114-2117)
  on lines 2119..2121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2119-2121)
  on lines 2123..2124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2123-2124)
  on lines 2128..2129 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2128-2129)
  on line 2133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2133-2133)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1913..1914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1913-1914)
  on line 1918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1918-1918)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1984..1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1984-1986)
  on lines 1988..1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1988-1989)
  on lines 1993..1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1993-1996)
  on lines 1998..2000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1998-2000)
  on lines 2002..2003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2002-2003)
  on lines 2007..2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2007-2010)
  on lines 2012..2014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2012-2014)
  on lines 2016..2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2016-2017)
  on lines 2021..2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2021-2022)
  on line 2026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2026-2026)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1871-1871)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2955..2956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2955-2956)
  on line 2962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2962-2962)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2766..2767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2766-2767)
  on line 2773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2773-2773)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2729..2730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2729-2730)
  on line 2736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2736-2736)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 3029..3030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3029-3030)
  on line 3036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3036-3036)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2803..2804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2803-2804)
  on line 2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2810-2810)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:380-380)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:389-389)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2918..2919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2918-2919)
  on line 2925 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2925-2925)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:414-414)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1233-1233)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1213-1213)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2992..2993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2992-2993)
  on line 2999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2999-2999)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 3066..3067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3066-3067)
  on line 3073 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3073-3073)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:371-371)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1755..1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1755-1756)
  on lines 1763..1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1763-1765)
  on lines 1767..1768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1767-1768)
  on lines 1770..1771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1770-1771)
  on lines 1778..1780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1778-1780)
  on lines 1782..1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1782-1783)
  on lines 1785..1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1785-1786)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1618..1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1618-1619)
  on lines 1621..1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1621-1622)
  on lines 1629..1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1629-1631)
  on lines 1633..1634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1633-1634)
  on lines 1636..1637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1636-1637)
  on lines 1644..1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1644-1646)
  on lines 1648..1649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1648-1649)
  on lines 1651..1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1651-1652)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1425..1426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1425-1426)
  on lines 1428..1429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1428-1429)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1832-1832)
  on lines 1837..1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1837-1838)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2267-2267)
  on lines 2272..2273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2272-2273)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2198..2199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2198-2199)
  on lines 2209..2210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2209-2210)
  on lines 2220..2221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2220-2221)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2037..2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2037-2038)
  on lines 2048..2049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2048-2049)
  on lines 2059..2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2059-2060)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2973-2973)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2784-2784)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2936-2936)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3084-3084)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3010-3010)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 3047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3047-3047)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2821-2821)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3141-3141)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 701
  dead: 545 (355 in uncalled functions)
  total lines: 1246
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3083:9-3083:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2086:7-2086:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2087:9-2087: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_product35.cil.c:941:10-941:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1679:7-1679:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2319:11-2319:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1884:11-1884:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1684:11-1684:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:698:7-698:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1909:11-1909:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2917:9-2917:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1931:11-1931:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2935:9-2935:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2954:9-2954:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1979:7-1979:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1980:9-1980:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2972:9-2972:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2728:9-2728:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1748:7-1748:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1752:11-1752:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2991:9-2991:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2195:9-2195:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3009:9-3009:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2206:11-2206:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2765:9-2765:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2216:11-2216:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2217:13-2217:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3028:9-3028:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2783:9-2783:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3046:9-3046:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2034:9-2034:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2802:9-2802:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2045:11-2045:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:3065:9-3065:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1614:7-1614:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2266:7-2266:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1615:9-1615:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1422:7-1422:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2820:9-2820:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1831:7-1831:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2055:11-2055:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2269:9-2269:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:2056:13-2056:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_product35.cil.c:1834:9-1834:20)
[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)
