./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_product19.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_product19.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:268:5-288: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:466:1-475:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:622:1-632:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:711:1-722:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:723:1-734:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1105:1-1113:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1131:1-1145:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1167:1-1181:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1185:1-1210:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1211:1-1230:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1235:1-1258:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1259:1-1278:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1282:1-1305:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1306:1-1325:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1326:1-1350:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1360:1-1428:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1429:1-1497:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1498:1-1553:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1563:1-1631:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1632:1-1687:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1691:1-1714:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1715:1-1734:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2232:1-2246:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2268:1-2283:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2360:1-2380:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2381:1-2396:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2399:1-2419:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2420:1-2435:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2438:1-2456:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2457:1-2472:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2475:1-2493:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2494:1-2509:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2725:1-2739:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:805-805)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1851-1851)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1126-1126)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2029..2031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2029-2031)
  on lines 2033..2035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2033-2035)
  on lines 2037..2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2037-2038)
  on line 2075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2075-2075)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2131..2132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2131-2132)
  on line 2147 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2147-2147)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2186..2187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2186-2187)
  on line 2194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2194-2194)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1979..1981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1979-1981)
  on lines 1983..1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1983-1984)
  on lines 1988..1991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1988-1991)
  on lines 1993..1995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1993-1995)
  on lines 1997..1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1997-1998)
  on lines 2002..2005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2002-2005)
  on lines 2007..2009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2007-2009)
  on lines 2011..2012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2011-2012)
  on lines 2016..2017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2016-2017)
  on line 2021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2021-2021)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1801..1802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1801-1802)
  on line 1806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1806-1806)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1872..1874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1872-1874)
  on lines 1876..1877 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1876-1877)
  on lines 1881..1884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1881-1884)
  on lines 1886..1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1886-1888)
  on lines 1890..1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1890-1891)
  on lines 1895..1898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1895-1898)
  on lines 1900..1902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1900-1902)
  on lines 1904..1905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1904-1905)
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1909-1910)
  on line 1914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1914-1914)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1751..1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1751-1752)
  on line 1759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1759-1759)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2295..2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2295-2296)
  on line 2302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2302-2302)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2258..2259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2258-2259)
  on line 2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2265-2265)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2558..2559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2558-2559)
  on line 2565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2565-2565)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2332..2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2332-2333)
  on line 2339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2339-2339)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2778-2778)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2787-2787)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2804..2805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2804-2805)
  on line 2812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2812-2812)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1102-1102)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2521..2522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2521-2522)
  on line 2528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2528-2528)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2595..2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2595-2596)
  on line 2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2602-2602)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2769-2769)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2155-2155)
  on lines 2160..2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2160-2161)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2086..2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2086-2087)
  on lines 2097..2098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2097-2098)
  on lines 2108..2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2108-2109)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1925..1926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1925-1926)
  on lines 1936..1937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1936-1937)
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1947-1948)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2313-2313)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2613-2613)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2539 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2539-2539)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2576-2576)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2350-2350)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:496-496)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2881-2881)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 515
  dead: 627 (504 in uncalled functions)
  total lines: 1142
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2257:9-2257:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2028:7-2028:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2803:9-2803:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2520:9-2520:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1819:11-1819:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2538:9-2538:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2294:9-2294:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2557:9-2557:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1867:7-1867:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1868:9-1868:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2871:7-2871:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2312:9-2312:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:666:7-666:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2575:9-2575:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2331:9-2331:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2083:9-2083:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2594:9-2594:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2349:9-2349:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2094:11-2094:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2104:11-2104:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2612:9-2612:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2105:13-2105:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2130:7-2130:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1922:9-1922:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1933:11-1933:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2154:7-2154:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1943:11-1943:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2157:9-2157:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1944:13-1944:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1974:7-1974:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1975:9-1975:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2185:11-2185:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1750:11-1750:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:848:10-848:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:2207:11-2207:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1772:11-1772:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product19.cil.c:1797:11-1797: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
