./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_spec3_product19.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_spec3_product19.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_spec3_product19.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_spec3_product19.cil.c:2649:3-2670:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2706:3-2731:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2791:5-2811: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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:82:1-91:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:244:1-258:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:797:1-805:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:845:1-859:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:863:1-888:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:889:1-908:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:913:1-936:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:937:1-956:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:960:1-983:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:984:1-1003:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1004:1-1028:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1038:1-1106:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1107:1-1175:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1176:1-1231:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1241:1-1309:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1310:1-1365:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1369:1-1392:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1393:1-1412:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1993:1-2003:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2082:1-2093:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2094:1-2105:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2182:1-2196:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2218:1-2233:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2310:1-2330:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2331:1-2346:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2349:1-2369:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2370:1-2385:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2388:1-2406:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2407:1-2422:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2425:1-2443:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2444:1-2459:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2578:1-2623:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2624:1-2679:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2680:1-2739:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2742:1-2844:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2845:1-2890:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2891:1-2936:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:437-437)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1529-1529)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:818-818)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1707..1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1707-1709)
  on lines 1711..1713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1711-1713)
  on lines 1715..1716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1715-1716)
  on line 1753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1753-1753)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1809..1810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1809-1810)
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1825-1825)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1864..1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1864-1865)
  on line 1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1872-1872)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1657..1659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1657-1659)
  on lines 1661..1662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1661-1662)
  on lines 1666..1669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1666-1669)
  on lines 1671..1673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1671-1673)
  on lines 1675..1676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1675-1676)
  on lines 1680..1683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1680-1683)
  on lines 1685..1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1685-1687)
  on lines 1689..1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1689-1690)
  on lines 1694..1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1694-1695)
  on line 1699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1699-1699)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1479..1480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1479-1480)
  on line 1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1484-1484)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1550..1552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1550-1552)
  on lines 1554..1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1554-1555)
  on lines 1559..1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1559-1562)
  on lines 1564..1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1564-1566)
  on lines 1568..1569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1568-1569)
  on lines 1573..1576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1573-1576)
  on lines 1578..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1578-1580)
  on lines 1582..1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1582-1583)
  on lines 1587..1588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1587-1588)
  on line 1592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1592-1592)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1429..1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1429-1430)
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1437-1437)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2245..2246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2245-2246)
  on line 2252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2252-2252)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2208..2209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2208-2209)
  on line 2215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2215-2215)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2508..2509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2508-2509)
  on line 2515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2515-2515)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2282..2283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2282-2283)
  on line 2289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2289-2289)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:297-297)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:306-306)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 323..324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:323-324)
  on line 331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:331-331)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:794-794)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2471..2472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2471-2472)
  on line 2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2478-2478)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2545..2546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2545-2546)
  on line 2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2552-2552)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:288-288)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1833-1833)
  on lines 1838..1839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1838-1839)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1764..1765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1764-1765)
  on lines 1775..1776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1775-1776)
  on lines 1786..1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1786-1787)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1603..1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1603-1604)
  on lines 1614..1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1614-1615)
  on lines 1625..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1625-1626)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2263-2263)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2563-2563)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2489-2489)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2526-2526)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2300-2300)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:112-112)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:406-406)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 528
  dead: 627 (504 in uncalled functions)
  total lines: 1155
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2262:9-2262:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1497:11-1497:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2525:9-2525:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2281:9-2281:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:322:9-322:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2544:9-2544:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1545:7-1545:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2299:9-2299:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1546:9-1546:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2562:9-2562:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2037:7-2037:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1761:9-1761:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1772:11-1772:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:396:7-396:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1782:11-1782:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1783:13-1783:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1808:7-1808:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1600:9-1600:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1611:11-1611:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1832:7-1832:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1621:11-1621:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1835:9-1835:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1622:13-1622:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1652:7-1652:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1653:9-1653:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1863:11-1863:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1428:11-1428:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2207:9-2207:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1885:11-1885:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1450:11-1450:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2470:9-2470:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:547:10-547:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1475:11-1475:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2488:9-2488:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2244:9-2244:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:1706:7-1706:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product19.cil.c:2507:9-2507: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)
