./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_spec7_product33.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_spec7_product33.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_spec7_product33.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_spec7_product33.cil.c:286:3-307:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:343:3-368:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:428:5-448: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:184:1-192:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:215:1-260:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:261:1-316:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:317:1-376:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:379:1-481:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:482:1-527:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:528:1-573:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:721:1-731:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:810:1-821:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:822:1-833:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:910:1-919:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:973:1-987:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:991:1-1016:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1017:1-1036:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1041:1-1064:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1065:1-1084:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1088:1-1111:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1112:1-1131:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1132:1-1156:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1166:1-1234:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1235:1-1303:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1304:1-1359:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1369:1-1437:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1438:1-1493:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2434:1-2448:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2641:1-2655:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2677:1-2692:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2769:1-2789:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2790:1-2805:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2808:1-2828:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2829:1-2844:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:3032:1-3046:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:949-949)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1657-1657)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:205-205)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1881-1881)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1518-1518)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1953-1953)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1992..1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1992-1993)
  on line 2000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2000-2000)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1785..1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1785-1787)
  on lines 1789..1790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1789-1790)
  on lines 1794..1797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1794-1797)
  on lines 1799..1801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1799-1801)
  on lines 1803..1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1803-1804)
  on lines 1808..1811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1808-1811)
  on lines 1813..1815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1813-1815)
  on lines 1817..1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1817-1818)
  on lines 1822..1823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1822-1823)
  on line 1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1827-1827)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1607..1608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1607-1608)
  on line 1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1612-1612)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1678..1680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1678-1680)
  on lines 1682..1683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1682-1683)
  on lines 1687..1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1687-1690)
  on lines 1692..1694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1692-1694)
  on lines 1696..1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1696-1697)
  on lines 1701..1704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1701-1704)
  on lines 1706..1708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1706-1708)
  on lines 1710..1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1710-1711)
  on lines 1715..1716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1715-1716)
  on line 1720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1720-1720)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1565-1565)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2893..2894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2893-2894)
  on line 2900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2900-2900)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2704..2705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2704-2705)
  on line 2711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2711-2711)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2667..2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2667-2668)
  on line 2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2674-2674)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2967..2968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2967-2968)
  on line 2974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2974-2974)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2741..2742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2741-2742)
  on line 2748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2748-2748)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2487-2487)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2496-2496)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2856..2857 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2856-2857)
  on line 2863 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2863-2863)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2513..2514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2513-2514)
  on line 2521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2521-2521)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:181-181)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:161-161)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2930..2931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2930-2931)
  on line 2937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2937-2937)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 3004..3005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:3004-3005)
  on line 3011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:3011-3011)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2478-2478)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1526-1526)
  on lines 1531..1532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1531-1532)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1961-1961)
  on lines 1966..1967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1966-1967)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1892..1893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1892-1893)
  on lines 1903..1904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1903-1904)
  on lines 1914..1915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1914-1915)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1731..1732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1731-1732)
  on lines 1742..1743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1742-1743)
  on lines 1753..1754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1753-1754)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2911-2911)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2722-2722)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2874-2874)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:3022-3022)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2948-2948)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2985-2985)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2759-2759)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:940-940)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 619
  dead: 580 (457 in uncalled functions)
  total lines: 1199
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2013:11-2013:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1578:11-1578:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2855:9-2855:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1603:11-1603:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2873:9-2873:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2063:10-2063:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2892:9-2892:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1625:11-1625:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2910:9-2910:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2666:9-2666:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2929:9-2929:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1673:7-1673:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1674:9-1674:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2947:9-2947:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2703:9-2703:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1889:9-1889:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2966:9-2966:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2721:9-2721:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1900:11-1900:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2984:9-2984:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2740:9-2740:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1910:11-1910:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:765:7-765:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1911:13-1911:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:3003:9-3003:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2758:9-2758:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1728:9-1728:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:3021:9-3021:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1739:11-1739:21)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:2512:9-2512:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1960:7-1960:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1525:7-1525:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1749:11-1749:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1963:9-1963:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1750:13-1750:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1528:9-1528:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1780:7-1780:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1781:9-1781:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product33.cil.c:1991:11-1991:22)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
