./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_product15.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/email_spec9_product15.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:830:3-851:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:887:3-912:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:972:5-992: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 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:120:1-134:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:137:1-155:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:156:1-171:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:248:1-268:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:269:1-284:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:287:1-307:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:308:1-323:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:400:1-418:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:419:1-434:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:437:1-455:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:456:1-471:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:474:1-492:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:493:1-508:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:737:1-751:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:759:1-804:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:805:1-860:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:861:1-920:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:923:1-1025:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1026:1-1071:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1072:1-1117:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1148:1-1162:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1166:1-1191:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1192:1-1211:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1216:1-1239:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1240:1-1259:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1263:1-1286:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1287:1-1306:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1307:1-1331:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1341:1-1409:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1410:1-1478:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1479:1-1534:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1544:1-1612:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1613:1-1668:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2107:1-2130:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2131:1-2150:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2364:1-2378:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2619:1-2629:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2708:1-2719:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2720:1-2731:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2800:1-2827:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2828:1-2846:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2847:1-2855:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2856:1-2875:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2876:1-2884:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2204-2204)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1832-1832)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2897-2897)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2015..2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2015-2016)
  on lines 2038..2040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2038-2040)
  on lines 2042..2044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2042-2044)
  on lines 2046..2047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2046-2047)
  on line 2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2056-2056)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 1685..1686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1685-1686)
  on line 1693 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1693-1693)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2167..2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2167-2168)
  on line 2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2175-2175)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1960..1962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1960-1962)
  on lines 1964..1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1964-1965)
  on lines 1969..1972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1969-1972)
  on lines 1974..1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1974-1976)
  on lines 1978..1979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1978-1979)
  on lines 1983..1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1983-1986)
  on lines 1988..1990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1988-1990)
  on lines 1992..1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1992-1993)
  on lines 1997..1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1997-1998)
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2002-2002)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1782..1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1782-1783)
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1787-1787)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1853..1855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1853-1855)
  on lines 1857..1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1857-1858)
  on lines 1862..1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1862-1865)
  on lines 1867..1869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1867-1869)
  on lines 1871..1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1871-1872)
  on lines 1876..1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1876-1879)
  on lines 1881..1883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1881-1883)
  on lines 1885..1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1885-1886)
  on lines 1890..1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1890-1891)
  on line 1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1895-1895)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1732..1733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1732-1733)
  on line 1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1740-1740)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 372..373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:372-373)
  on line 379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:379-379)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 183..184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:183-184)
  on line 190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:190-190)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 220..221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:220-221)
  on line 227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:227-227)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2417-2417)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2426-2426)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 335..336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:335-336)
  on line 342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:342-342)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2443..2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2443-2444)
  on line 2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2451-2451)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2408-2408)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1701-1701)
  on lines 1706..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1706-1707)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2067..2068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2067-2068)
  on lines 2078..2079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2078-2079)
  on lines 2089..2090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2089-2090)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1906..1907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1906-1907)
  on lines 1917..1918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1917-1918)
  on lines 1928..1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1928-1929)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:390-390)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:201-201)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:353-353)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:238-238)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:94-94)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 460
  dead: 674 (558 in uncalled functions)
  total lines: 1134
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:237:9-237:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2166:11-2166:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1731:11-1731:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2188:11-2188:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1753:11-1753: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_product15.cil.c:558:10-558:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1778:11-1778:22)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2014:11-2014:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1800:11-1800:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:334:9-334:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2037:11-2037:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:352:9-352:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1848:7-1848:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1849:9-1849:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:371:9-371:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2663:7-2663:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2064:9-2064:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:389:9-389:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2075:11-2075:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2085:11-2085:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2086:13-2086:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:182:9-182:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1903:9-1903:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1684:11-1684:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1914:11-1914:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:200:9-200:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1700:7-1700:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1924:11-1924:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:2442:9-2442:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1925:13-1925:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1703:9-1703:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:219:9-219:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1955:7-1955:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product15.cil.c:1956:9-1956:19)
[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
