./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_spec8_product30.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_spec8_product30.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_spec8_product30.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_spec8_product30.cil.c:676:3-697:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:733:3-758:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:818:5-838: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:186:1-196:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:275:1-286:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:287:1-298:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:430:1-457:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:458:1-476:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:477:1-495:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:496:1-509:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:539:1-547:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:565:1-574:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:605:1-650:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:651:1-706:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:707:1-766:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:769:1-871:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:872:1-917:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:918:1-963:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1361:1-1375:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1547:1-1561:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1579:1-1593:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1597:1-1622:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1623:1-1642:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1647:1-1670:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1671:1-1690:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1694:1-1717:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1718:1-1737:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1738:1-1762:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1772:1-1840:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1841:1-1909:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1910:1-1965:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1975:1-2043:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2044:1-2099:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2538:1-2561:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2562:1-2581:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2637:1-2651:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2654:1-2672:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2673:1-2688:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2765:1-2785:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2786:1-2801:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2804:1-2824:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2825:1-2840:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2991:1-3009:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:413-413)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2263-2263)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:560-560)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2469..2471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2469-2471)
  on lines 2473..2475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2473-2475)
  on lines 2477..2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2477-2478)
  on line 2487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2487-2487)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 2116..2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2116-2117)
  on line 2124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2124-2124)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2598..2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2598-2599)
  on line 2606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2606-2606)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2391..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2391-2393)
  on lines 2395..2396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2395-2396)
  on lines 2400..2403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2400-2403)
  on lines 2405..2407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2405-2407)
  on lines 2409..2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2409-2410)
  on lines 2414..2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2414-2417)
  on lines 2419..2421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2419-2421)
  on lines 2423..2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2423-2424)
  on lines 2428..2429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2428-2429)
  on line 2433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2433-2433)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2213..2214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2213-2214)
  on line 2218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2218-2218)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2284..2286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2284-2286)
  on lines 2288..2289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2288-2289)
  on lines 2293..2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2293-2296)
  on lines 2298..2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2298-2300)
  on lines 2302..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2302-2303)
  on lines 2307..2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2307-2310)
  on lines 2312..2314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2312-2314)
  on lines 2316..2317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2316-2317)
  on lines 2321..2322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2321-2322)
  on line 2326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2326-2326)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2163..2164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2163-2164)
  on line 2171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2171-2171)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2889..2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2889-2890)
  on line 2896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2896-2896)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2700..2701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2700-2701)
  on line 2707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2707-2707)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2963..2964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2963-2964)
  on line 2970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2970-2970)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2737..2738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2737-2738)
  on line 2744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2744-2744)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1414-1414)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1423-1423)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2852..2853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2852-2853)
  on line 2859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2859-2859)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1440..1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1440-1441)
  on line 1448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1448-1448)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:536-536)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:516-516)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2926..2927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2926-2927)
  on line 2933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2933-2933)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1405-1405)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2132-2132)
  on lines 2137..2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2137-2138)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2498..2499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2498-2499)
  on lines 2509..2510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2509-2510)
  on lines 2520..2521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2520-2521)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2337..2338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2337-2338)
  on lines 2348..2349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2348-2349)
  on lines 2359..2360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2359-2360)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2907 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2907-2907)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2718-2718)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2870-2870)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:3018-3018)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2944-2944)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2981-2981)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2755-2755)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:595-595)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 533
  dead: 653 (528 in uncalled functions)
  total lines: 1186
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2386:7-2386:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2387:9-2387:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2851:9-2851:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2597:11-2597:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2162:11-2162:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2869:9-2869:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2619:11-2619:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2184:11-2184:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2888:9-2888:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2209:11-2209:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2906:9-2906:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1004:10-1004:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2925:9-2925:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2231:11-2231:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2943:9-2943:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2699:9-2699:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2468:11-2468:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2962:9-2962:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2279:7-2279:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2280:9-2280:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2717:9-2717:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2980:9-2980:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2736:9-2736:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2495:9-2495:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2754:9-2754:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2506:11-2506:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2516:11-2516:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:3017:9-3017:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2517:13-2517:23)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:230:7-230:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2334:9-2334:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2115:11-2115:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2345:11-2345:21)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:1439:9-1439:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2131:7-2131:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2355:11-2355:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2356:13-2356:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product30.cil.c:2134:9-2134:20)
[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)
