./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_spec27_product31.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_spec27_product31.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_spec27_product31.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_spec27_product31.cil.c:2208:3-2229:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2265:3-2290:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2350:5-2370: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:186:1-196:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:275:1-286:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:287:1-298:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:365:1-374:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:421:1-435:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:457:1-472:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:549:1-569:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:570:1-585:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:588:1-608:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:609:1-624:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:832:1-846:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:850:1-875:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:876:1-895:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:900:1-923:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:924:1-943:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:947:1-970:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:971:1-990:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:991:1-1015:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1025:1-1093:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1094:1-1162:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1163:1-1218:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1228:1-1296:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1297:1-1352:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1356:1-1379:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1380:1-1399:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2137:1-2182:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2183:1-2238:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2239:1-2298:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2301:1-2403:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2404:1-2449:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2450:1-2495:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2498:1-2512:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2688:1-2702:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2989:1-2997:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2875-2875)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1516-1516)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:3010-3010)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1699..1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1699-1700)
  on line 1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1740-1740)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1796..1797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1796-1797)
  on line 1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1812-1812)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1851..1852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1851-1852)
  on line 1859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1859-1859)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1644..1646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1644-1646)
  on lines 1648..1649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1648-1649)
  on lines 1653..1656 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1653-1656)
  on lines 1658..1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1658-1660)
  on lines 1662..1663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1662-1663)
  on lines 1667..1670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1667-1670)
  on lines 1672..1674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1672-1674)
  on lines 1676..1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1676-1677)
  on lines 1681..1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1681-1682)
  on line 1686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1686-1686)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1466..1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1466-1467)
  on line 1471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1471-1471)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1537..1539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1537-1539)
  on lines 1541..1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1541-1542)
  on lines 1546..1549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1546-1549)
  on lines 1551..1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1551-1553)
  on lines 1555..1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1555-1556)
  on lines 1560..1563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1560-1563)
  on lines 1565..1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1565-1567)
  on lines 1569..1570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1569-1570)
  on lines 1574..1575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1574-1575)
  on line 1579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1579-1579)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1424-1424)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 673..674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:673-674)
  on line 680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:680-680)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 484..485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:484-485)
  on line 491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:491-491)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 447..448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:447-448)
  on line 454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:454-454)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 747..748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:747-748)
  on line 754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:754-754)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 521..522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:521-522)
  on line 528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:528-528)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2741-2741)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2750-2750)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 636..637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:636-637)
  on line 643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:643-643)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2767..2768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2767-2768)
  on line 2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2775-2775)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2986-2986)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2966-2966)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 710..711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:710-711)
  on line 717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:717-717)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 784..785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:784-785)
  on line 791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:791-791)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2732-2732)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1820-1820)
  on lines 1825..1826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1825-1826)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1751..1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1751-1752)
  on lines 1762..1763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1762-1763)
  on lines 1773..1774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1773-1774)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1590..1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1590-1591)
  on lines 1601..1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1601-1602)
  on lines 1612..1613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1612-1613)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:691-691)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:502-502)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:654-654)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:802-802)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:728-728)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 765 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:765-765)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:539-539)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:395-395)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 587
  dead: 599 (476 in uncalled functions)
  total lines: 1186
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1484:11-1484:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1532:7-1532:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1533:9-1533:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:635:9-635:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1748:9-1748:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:653:9-653:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1759:11-1759:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1769:11-1769:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1770:13-1770:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:672:9-672:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1795:7-1795:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:690:9-690:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1587:9-1587:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:446:9-446:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1598:11-1598:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:709:9-709:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1819:7-1819:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1608:11-1608:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1822:9-1822:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1609:13-1609:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:727:9-727:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:483:9-483:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1639:7-1639:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1640:9-1640:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:746:9-746:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1850:11-1850:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:501:9-501:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:764:9-764:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:520:9-520:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1872:11-1872:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1437:11-1437:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:783:9-783:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:538:9-538:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:230:7-230:10)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:2766:9-2766:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1462:11-1462:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:801:9-801:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1922:10-1922:11)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product31.cil.c:1698:11-1698:48)
[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
