./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_spec11_product15.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_spec11_product15.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_spec11_product15.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_spec11_product15.cil.c:2484:3-2505:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2541:3-2566:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2626:5-2646: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_spec11_product15.cil.c:71:1-85:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:88:1-106:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:107:1-122:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:199:1-219:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:220:1-235:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:238:1-258:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:259:1-274:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:351:1-369:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:370:1-385:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:388:1-406:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:407:1-422:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:425:1-443:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:444:1-459:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:648:1-662:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:792:1-806:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:810:1-835:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:836:1-855:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:860:1-883:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:884:1-903:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:907:1-930:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:931:1-950:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:951:1-975:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:985:1-1053:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1054:1-1122:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1123:1-1178:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1188:1-1256:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1257:1-1312:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1751:1-1774:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1775:1-1794:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1844:1-1858:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2098:1-2107:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2229:1-2239:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2318:1-2329:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2330:1-2341:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2413:1-2458:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2459:1-2514:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2515:1-2574:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2577:1-2679:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2680:1-2725:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2726:1-2771:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2775:1-2802:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2803:1-2821:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2851:1-2859:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2090-2090)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1476-1476)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2872-2872)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1659..1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1659-1660)
  on lines 1682..1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1682-1684)
  on lines 1686..1688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1686-1688)
  on lines 1690..1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1690-1691)
  on line 1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1700-1700)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 1329..1330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1329-1330)
  on line 1337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1337-1337)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1811..1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1811-1812)
  on line 1819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1819-1819)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1604..1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1604-1606)
  on lines 1608..1609 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1608-1609)
  on lines 1613..1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1613-1616)
  on lines 1618..1620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1618-1620)
  on lines 1622..1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1622-1623)
  on lines 1627..1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1627-1630)
  on lines 1632..1634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1632-1634)
  on lines 1636..1637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1636-1637)
  on lines 1641..1642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1641-1642)
  on line 1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1646-1646)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1426..1427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1426-1427)
  on line 1431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1431-1431)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1497..1499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1497-1499)
  on lines 1501..1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1501-1502)
  on lines 1506..1509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1506-1509)
  on lines 1511..1513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1511-1513)
  on lines 1515..1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1515-1516)
  on lines 1520..1523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1520-1523)
  on lines 1525..1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1525-1527)
  on lines 1529..1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1529-1530)
  on lines 1534..1535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1534-1535)
  on line 1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1539-1539)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1376..1377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1376-1377)
  on line 1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1384-1384)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 323..324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:323-324)
  on line 330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.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_spec11_product15.cil.c:134-135)
  on line 141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:141-141)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 171..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:171-172)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:178-178)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:701-701)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 710 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:710-710)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 286..287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:286-287)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:293-293)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 727..728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:727-728)
  on line 735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:735-735)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2848-2848)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2828-2828)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:692-692)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1345-1345)
  on lines 1350..1351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1350-1351)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1711..1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1711-1712)
  on lines 1722..1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1722-1723)
  on lines 1733..1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1733-1734)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1550..1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1550-1551)
  on lines 1561..1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1561-1562)
  on lines 1572..1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1572-1573)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:341-341)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:152-152)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:304-304)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:189-189)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2128-2128)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 460
  dead: 666 (548 in uncalled functions)
  total lines: 1126
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1681:11-1681:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1492:7-1492:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1493:9-1493:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1708:9-1708:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:2273:7-2273:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1719:11-1719:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:285:9-285:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1729:11-1729:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1730:13-1730:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:303:9-303:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1547:9-1547:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:322:9-322:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1328:11-1328:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1558:11-1558:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1344:7-1344:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.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_spec11_product15.cil.c:1568:11-1568:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1569:13-1569:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1347:9-1347:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1599:7-1599:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1600:9-1600:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1810:11-1810:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1375:11-1375:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:133:9-133:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:726:9-726:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1832:11-1832:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1397:11-1397:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:170:9-170:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1422:11-1422:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:188:9-188:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1658:11-1658:48)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1908:10-1908:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product15.cil.c:1444:11-1444: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
