./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/email_spec1_product21.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/email_spec1_product21.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_spec1_product21.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_spec1_product21.cil.c:931:3-952:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:988:3-1013:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1073:5-1093:5 with factor 2
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:112:1-126:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:148:1-163:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:240:1-260:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:261:1-276:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:279:1-299:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:300:1-315:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:392:1-410:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:411:1-426:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:429:1-447:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:448:1-463:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:466:1-484:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:485:1-500:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:812:1-820:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:838:1-852:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:860:1-905:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:906:1-961:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:962:1-1021:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1024:1-1126:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1127:1-1172:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1173:1-1218:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1224:1-1233:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1458:1-1472:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1599:1-1613:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1617:1-1642:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1643:1-1662:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1667:1-1690:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1691:1-1710:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1758:1-1782:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1792:1-1860:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1861:1-1929:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2123:1-2146:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2147:1-2166:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2747:1-2757:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2836:1-2847:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2848:1-2859:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2943-2943)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2283-2283)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:833-833)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2489..2491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2489-2491)
  on lines 2493..2495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2493-2495)
  on lines 2497..2498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2497-2498)
  on line 2507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2507-2507)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2008..2010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2008-2010)
  on lines 2012..2013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2012-2013)
  on lines 2018..2021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2018-2021)
  on lines 2023..2025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2023-2025)
  on lines 2027..2029 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2027-2029)
  on lines 2031..2032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2031-2032)
  on lines 2037..2040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2037-2040)
  on lines 2042..2044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2042-2044)
  on lines 2046..2048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2046-2048)
  on lines 2050..2051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2050-2051)
  on lines 2056..2057 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2056-2057)
  on line 2061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2061-2061)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 1727..1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1727-1728)
  on line 1735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1735-1735)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2563..2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2563-2564)
  on line 2579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2579-2579)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2618..2619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2618-2619)
  on line 2626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2626-2626)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2411..2413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2411-2413)
  on lines 2415..2416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2415-2416)
  on lines 2420..2423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2420-2423)
  on lines 2425..2427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2425-2427)
  on lines 2429..2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2429-2430)
  on lines 2434..2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2434-2437)
  on lines 2439..2441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2439-2441)
  on lines 2443..2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2443-2444)
  on lines 2448..2449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2448-2449)
  on line 2453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2453-2453)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2233..2234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2233-2234)
  on line 2238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2238-2238)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2304..2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2304-2306)
  on lines 2308..2309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2308-2309)
  on lines 2313..2316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2313-2316)
  on lines 2318..2320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2318-2320)
  on lines 2322..2323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2322-2323)
  on lines 2327..2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2327-2330)
  on lines 2332..2334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2332-2334)
  on lines 2336..2337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2336-2337)
  on lines 2341..2342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2341-2342)
  on line 2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2346-2346)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2175..2176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2175-2176)
  on line 2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2191-2191)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 364..365 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:364-365)
  on line 371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:371-371)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 175..176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:175-176)
  on line 182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:182-182)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 138..139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:138-139)
  on line 145 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:145-145)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 212..213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:212-213)
  on line 219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:219-219)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1511-1511)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1520-1520)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 327..328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:327-328)
  on line 334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:334-334)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1537..1538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1537-1538)
  on line 1545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1545-1545)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:809-809)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:789-789)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1502-1502)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2075..2076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2075-2076)
  on lines 2083..2085 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2083-2085)
  on lines 2087..2088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2087-2088)
  on lines 2090..2091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2090-2091)
  on lines 2098..2100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2098-2100)
  on lines 2102..2103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2102-2103)
  on lines 2105..2106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2105-2106)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1938..1939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1938-1939)
  on lines 1941..1942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1941-1942)
  on lines 1949..1951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1949-1951)
  on lines 1953..1954 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1953-1954)
  on lines 1956..1957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1956-1957)
  on lines 1964..1966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1964-1966)
  on lines 1968..1969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1968-1969)
  on lines 1971..1972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1971-1972)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1745..1746 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1745-1746)
  on lines 1748..1749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1748-1749)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2587-2587)
  on lines 2592..2593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2592-2593)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2518..2519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2518-2519)
  on lines 2529..2530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2529-2530)
  on lines 2540..2541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2540-2541)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2357..2358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2357-2358)
  on lines 2368..2369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2368-2369)
  on lines 2379..2380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2379-2380)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:382-382)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:193-193)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:345-345)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:230-230)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1254-1254)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 555
  dead: 608 (416 in uncalled functions)
  total lines: 1163
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:229:9-229:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2068:7-2068:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2072:11-2072:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2791:7-2791:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2515:9-2515:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2526:11-2526:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2536:11-2536:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2537:13-2537:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:551:10-551:11)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2562:7-2562:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2354:9-2354:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1726:11-1726:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2365:11-2365:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1934:7-1934:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2586:7-2586:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1935:9-1935:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1742:7-1742:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:326:9-326:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2375:11-2375:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2589:9-2589:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2376:13-2376:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2406:7-2406:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2407:9-2407:19)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2174:7-2174:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:344:9-344:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2617:11-2617:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:363:9-363:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1999:7-1999:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:381:9-381:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2639:11-2639:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:137:9-137:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2204:11-2204:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:1536:9-1536:21)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2004:11-2004:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2229:11-2229:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:174:9-174:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2251:11-2251:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:192:9-192:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:211:9-211:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2488:11-2488:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2299:7-2299:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product21.cil.c:2300:9-2300:19)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
