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


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:830:3-851:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:887:3-912:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:82:1-91:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:138:1-152:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:174:1-189:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:266:1-286:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:287:1-302:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:305:1-325:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:326:1-341:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.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_product31.cil.c:1613:1-1668:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1672:1-1695:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1696:1-1715:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2384:1-2398:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2672:1-2682:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2761:1-2772:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2773:1-2784:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:3002:1-3010:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2571-2571)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1832-1832)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:3023-3023)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2015..2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2015-2016)
  on line 2056 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2056-2056)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2112..2113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2112-2113)
  on line 2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2128-2128)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2167..2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2167-2168)
  on line 2175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.cil.c:1960-1962)
  on lines 1964..1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1964-1965)
  on lines 1969..1972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1969-1972)
  on lines 1974..1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1974-1976)
  on lines 1978..1979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1978-1979)
  on lines 1983..1986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1983-1986)
  on lines 1988..1990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1988-1990)
  on lines 1992..1993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1992-1993)
  on lines 1997..1998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1997-1998)
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.cil.c:1782-1783)
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.cil.c:1853-1855)
  on lines 1857..1858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1857-1858)
  on lines 1862..1865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1862-1865)
  on lines 1867..1869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1867-1869)
  on lines 1871..1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1871-1872)
  on lines 1876..1879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1876-1879)
  on lines 1881..1883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1881-1883)
  on lines 1885..1886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1885-1886)
  on lines 1890..1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1890-1891)
  on line 1895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1895-1895)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1740-1740)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 390..391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:390-391)
  on line 397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:397-397)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 201..202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:201-202)
  on line 208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:208-208)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 164..165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:164-165)
  on line 171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:171-171)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 464..465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:464-465)
  on line 471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:471-471)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 238..239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:238-239)
  on line 245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:245-245)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2437-2437)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2446-2446)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 353..354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:353-354)
  on line 360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:360-360)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2463..2464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2463-2464)
  on line 2471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2471-2471)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2999-2999)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2979-2979)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 427..428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:427-428)
  on line 434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:434-434)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 501..502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:501-502)
  on line 508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:508-508)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2428-2428)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2136-2136)
  on lines 2141..2142 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2141-2142)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2067..2068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2067-2068)
  on lines 2078..2079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2078-2079)
  on lines 2089..2090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.cil.c:1906-1907)
  on lines 1917..1918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1917-1918)
  on lines 1928..1929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1928-1929)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:408-408)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:219-219)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:371-371)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:519-519)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:445-445)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:482-482)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:256-256)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:112-112)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 593
  dead: 599 (476 in uncalled functions)
  total lines: 1192
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:500:9-500:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2166:11-2166:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:255:9-255:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:518:9-518:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.cil.c:1753:11-1753:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1778:11-1778: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_product31.cil.c:576:10-576:11)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.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_product31.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_product31.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_product31.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_product31.cil.c:370:9-370:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.cil.c:2064:9-2064:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2075:11-2075:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:407:9-407:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:163:9-163:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.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_product31.cil.c:426:9-426:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2716:7-2716:10)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2111:7-2111:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1903:9-1903:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:444:9-444:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:200:9-200:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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_product31.cil.c:463:9-463:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2135:7-2135:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1924:11-1924:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:218:9-218:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2138:9-2138:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1925:13-1925:23)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:2462:9-2462:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:481:9-481:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:1955:7-1955:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.cil.c:237:9-237:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product31.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
