./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_spec9_product22.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_spec9_product22.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_spec9_product22.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_spec9_product22.cil.c:2566:3-2587:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2623:3-2648:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2708:5-2728: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:148:1-156:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:202:1-216:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:220:1-245:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:246:1-265:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:270:1-293:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:294:1-313:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:317:1-340:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:341:1-360:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:361:1-385:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:395:1-463:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:464:1-532:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:533:1-588:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:598:1-666:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:667:1-722:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1497:1-1511:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1533:1-1548:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1625:1-1645:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1646:1-1661:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1664:1-1684:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1685:1-1700:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1777:1-1795:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1796:1-1811:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1814:1-1832:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1833:1-1848:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1851:1-1869:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1870:1-1885:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2064:1-2078:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2292:1-2302:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2381:1-2392:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2393:1-2404:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2495:1-2540:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2541:1-2596:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2597:1-2656:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2659:1-2761:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2762:1-2807:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2808:1-2853:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2898:1-2912:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2915:1-2924:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2485-2485)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:886-886)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:169-169)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1069..1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1069-1070)
  on lines 1092..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1092-1094)
  on lines 1096..1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1096-1098)
  on lines 1100..1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1100-1101)
  on line 1110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1110-1110)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:747-747)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1182-1182)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1221..1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1221-1222)
  on line 1229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1229-1229)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1014..1016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1014-1016)
  on lines 1018..1019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1018-1019)
  on lines 1023..1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1023-1026)
  on lines 1028..1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1028-1030)
  on lines 1032..1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1032-1033)
  on lines 1037..1040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1037-1040)
  on lines 1042..1044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1042-1044)
  on lines 1046..1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1046-1047)
  on lines 1051..1052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1051-1052)
  on line 1056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1056-1056)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 836..837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:836-837)
  on line 841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:841-841)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 907..909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:907-909)
  on lines 911..912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:911-912)
  on lines 916..919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:916-919)
  on lines 921..923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:921-923)
  on lines 925..926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:925-926)
  on lines 930..933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:930-933)
  on lines 935..937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:935-937)
  on lines 939..940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:939-940)
  on lines 944..945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:944-945)
  on line 949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:949-949)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:794-794)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1749..1750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1749-1750)
  on line 1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1756-1756)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1560..1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1560-1561)
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1567-1567)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1523..1524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1523-1524)
  on line 1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1530-1530)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1597..1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1597-1598)
  on line 1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1604-1604)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2117-2117)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2126-2126)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1712..1713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1712-1713)
  on line 1719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1719-1719)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2143..2144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2143-2144)
  on line 2151 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2151-2151)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:145-145)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:125-125)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2108-2108)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:755-755)
  on lines 760..761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:760-761)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1190-1190)
  on lines 1195..1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1195-1196)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1121..1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1121-1122)
  on lines 1132..1133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1132-1133)
  on lines 1143..1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1143-1144)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 960..961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:960-961)
  on lines 971..972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:971-972)
  on lines 982..983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:982-983)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1767-1767)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1578-1578)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1730-1730)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1615-1615)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2945-2945)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 538
  dead: 620 (499 in uncalled functions)
  total lines: 1158
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1596:9-1596:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1091:11-1091:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:902:7-902:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:903:9-903:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1614:9-1614:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1118:9-1118:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1129:11-1129:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1139:11-1139:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1140:13-1140:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:957:9-957:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:968:11-968:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1189:7-1189:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:754:7-754:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:978:11-978:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:979:13-979:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1192:9-1192:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:757:9-757:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1711:9-1711:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1009:7-1009:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1010:9-1010:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2336:7-2336:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1729:9-1729:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1220:11-1220:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1748:9-1748:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1242:11-1242:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:807:11-807:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1766:9-1766:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1522:9-1522:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:832:11-832:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1302:10-1302:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1559:9-1559:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1068:11-1068:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:854:11-854:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:1577:9-1577:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product22.cil.c:2142:9-2142:21)
[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
