./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_spec7_productSimulator.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_spec7_productSimulator.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_spec7_productSimulator.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_spec7_productSimulator.cil.c:3167:3-3188:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3224:3-3249:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3309:5-3329: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

[Info] runtime: 00:00:10.281
[Info] vars: 31812, evals: 25469

[Info] |called|=0

Memory statistics: total=21241.56MB, max=281.26MB, minor=21235.55MB, major=330.31MB, promoted=324.31MB
    minor collections=10133  major collections=15 compactions=0

[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:435:1-449:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:652:1-666:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:688:1-703:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:780:1-800:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:801:1-816:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:819:1-839:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:840:1-855:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1216:1-1226:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1305:1-1316:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1317:1-1328:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1615:1-1623:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1649:1-1663:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1667:1-1692:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1693:1-1712:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1717:1-1740:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1741:1-1760:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1808:1-1832:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1842:1-1910:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1911:1-1979:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3074:1-3088:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3096:1-3141:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3142:1-3197:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3198:1-3257:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3260:1-3362:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3363:1-3408:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3409:1-3454:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 3461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3461-3461)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2333-2333)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1636-1636)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2557-2557)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2058..2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2058-2060)
  on lines 2062..2063 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2062-2063)
  on lines 2068..2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2068-2071)
  on lines 2073..2075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2073-2075)
  on lines 2077..2079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2077-2079)
  on lines 2081..2082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2081-2082)
  on lines 2087..2090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2087-2090)
  on lines 2092..2094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2092-2094)
  on lines 2096..2098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2096-2098)
  on lines 2100..2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2100-2101)
  on lines 2106..2107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2106-2107)
  on line 2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2111-2111)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1785-1785)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2194 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2194-2194)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2629-2629)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2676-2676)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2461..2463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2461-2463)
  on lines 2465..2466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2465-2466)
  on lines 2470..2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2470-2473)
  on lines 2475..2477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2475-2477)
  on lines 2479..2480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2479-2480)
  on lines 2484..2487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2484-2487)
  on lines 2489..2491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2489-2491)
  on lines 2493..2494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2493-2494)
  on lines 2498..2499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2498-2499)
  on line 2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2503-2503)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2283..2284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2283-2284)
  on line 2288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2288-2288)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2354..2356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2354-2356)
  on lines 2358..2359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2358-2359)
  on lines 2363..2366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2363-2366)
  on lines 2368..2370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2368-2370)
  on lines 2372..2373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2372-2373)
  on lines 2377..2380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2377-2380)
  on lines 2382..2384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2382-2384)
  on lines 2386..2387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2386-2387)
  on lines 2391..2392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2391-2392)
  on line 2396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2396-2396)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2241-2241)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 904..905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:904-905)
  on line 911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:911-911)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 715..716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:715-716)
  on line 722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:722-722)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 678..679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:678-679)
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:685-685)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 978..979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:978-979)
  on line 985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:985-985)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 752..753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:752-753)
  on line 759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:759-759)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:488-488)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:497-497)
[Warning][Deadcode] Function 'incoming__before__Decrypt' has dead code:
  on line 371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:371-371)
  on line 373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:373-373)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 867..868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:867-868)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:874-874)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 514..515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:514-515)
  on line 522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:522-522)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1612-1612)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 1574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1574-1574)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1594-1594)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 941..942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:941-942)
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:948-948)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1015..1016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1015-1016)
  on line 1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1022-1022)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:479-479)
[Warning][Deadcode] Function 'printMail' has dead code:
  on line 1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1562-1562)
  on line 1564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1564-1564)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 2974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2974-2974)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2125..2126 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2125-2126)
  on lines 2133..2135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2133-2135)
  on lines 2137..2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2137-2138)
  on lines 2140..2141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2140-2141)
  on lines 2148..2150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2148-2150)
  on lines 2152..2153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2152-2153)
  on lines 2155..2156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2155-2156)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1988..1989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1988-1989)
  on lines 1991..1992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1991-1992)
  on lines 1999..2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1999-2001)
  on lines 2003..2004 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2003-2004)
  on lines 2006..2007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2006-2007)
  on lines 2014..2016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2014-2016)
  on lines 2018..2019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2018-2019)
  on lines 2021..2022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2021-2022)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1795..1796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1795-1796)
  on lines 1798..1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1798-1799)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2202-2202)
  on lines 2207..2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2207-2208)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2637-2637)
  on lines 2642..2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2642-2643)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2568..2569 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2568-2569)
  on lines 2579..2580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2579-2580)
  on lines 2590..2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2590-2591)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2407..2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2407-2408)
  on lines 2418..2419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2418-2419)
  on lines 2429..2430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2429-2430)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:922-922)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:733-733)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:885-885)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1033-1033)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:959-959)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:996-996)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:770-770)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 3052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3052-3052)
  on line 3069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3069-3069)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 809
  dead: 550 (351 in uncalled functions)
  total lines: 1359
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2576:11-2576:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2586:11-2586:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2587:13-2587:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2636:7-2636:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1792:7-1792:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2201:7-2201:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2639:9-2639:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2204:9-2204:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:677:9-677:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:714:9-714:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2689:11-2689:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2254:11-2254:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:732:9-732:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2279:11-2279:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:751:9-751:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2739:10-2739:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2301:11-2301:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:769:9-769:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2349:7-2349:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2350:9-2350:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:866:9-866:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2404:9-2404:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:884:9-884:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2415:11-2415:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1984:7-1984:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:903:9-903:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1985:9-1985:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2425:11-2425:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2426:13-2426:23)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Verify' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:364:7-364:32)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2456:7-2456:18)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Verify' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1555:7-1555:32)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:921:9-921:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2457:9-2457:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:940:9-940:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:958:9-958:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2049:7-2049:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2054:11-2054:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:977:9-977:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:995:9-995:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1014:9-1014:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:1032:9-1032:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:513:9-513:21)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Verify' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3026:21-3026:46)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Verify' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3028:23-3028:50)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Sign' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:3033:27-3033:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2118:7-2118:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2122:11-2122:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_productSimulator.cil.c:2565:9-2565: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)
