./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_spec8_product34.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_spec8_product34.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_product34.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_product34.cil.c:1326:3-1347:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1383:3-1408:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1468:5-1488: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_spec8_product34.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_spec8_product34.cil.c:82:1-91:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:145:1-159:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:163:1-188:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:189:1-208:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:213:1-236:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:237:1-256:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:304:1-328:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:338:1-406:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:407:1-475:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:669:1-692:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:693:1-712:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1255:1-1300:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1301:1-1356:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1357:1-1416:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1419:1-1521:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1522:1-1567:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1568:1-1613:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1729:1-1739:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1818:1-1829:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1830:1-1841:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2146:1-2160:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2344:1-2358:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2380:1-2395:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2472:1-2492:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2493:1-2508:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2511:1-2531:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2532:1-2547:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:3063:1-3071:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1201-1201)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:829-829)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:3084-3084)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1053-1053)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 554..556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:554-556)
  on lines 558..559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:558-559)
  on lines 564..567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:564-567)
  on lines 569..571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:569-571)
  on lines 573..575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:573-575)
  on lines 577..578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:577-578)
  on lines 583..586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:583-586)
  on lines 588..590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:588-590)
  on lines 592..594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:592-594)
  on lines 596..597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:596-597)
  on lines 602..603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:602-603)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:607-607)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on lines 273..274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:273-274)
  on line 281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:281-281)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1109..1110 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1109-1110)
  on line 1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1125-1125)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1164..1165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1164-1165)
  on line 1172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1172-1172)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 957..959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:957-959)
  on lines 961..962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:961-962)
  on lines 966..969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:966-969)
  on lines 971..973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:971-973)
  on lines 975..976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:975-976)
  on lines 980..983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:980-983)
  on lines 985..987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:985-987)
  on lines 989..990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:989-990)
  on lines 994..995 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:994-995)
  on line 999 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:999-999)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 779..780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:779-780)
  on line 784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:784-784)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 850..852 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:850-852)
  on lines 854..855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:854-855)
  on lines 859..862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:859-862)
  on lines 864..866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:864-866)
  on lines 868..869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:868-869)
  on lines 873..876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:873-876)
  on lines 878..880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:878-880)
  on lines 882..883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:882-883)
  on lines 887..888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:887-888)
  on line 892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:892-892)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:737-737)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2596..2597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2596-2597)
  on line 2603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2603-2603)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2407..2408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2407-2408)
  on line 2414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2414-2414)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2370..2371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2370-2371)
  on line 2377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2377-2377)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2670..2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2670-2671)
  on line 2677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2677-2677)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2444..2445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2444-2445)
  on line 2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2451-2451)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2199-2199)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2208-2208)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2559..2560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2559-2560)
  on line 2566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2566-2566)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2225..2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2225-2226)
  on line 2233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2233-2233)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 3060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:3060-3060)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 3040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:3040-3040)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2633..2634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2633-2634)
  on line 2640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2640-2640)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2707..2708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2707-2708)
  on line 2714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2714-2714)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2190-2190)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 621..622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:621-622)
  on lines 629..631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:629-631)
  on lines 633..634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:633-634)
  on lines 636..637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:636-637)
  on lines 644..646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:644-646)
  on lines 648..649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:648-649)
  on lines 651..652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:651-652)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 484..485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:484-485)
  on lines 487..488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:487-488)
  on lines 495..497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:495-497)
  on lines 499..500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:499-500)
  on lines 502..503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:502-503)
  on lines 510..512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:510-512)
  on lines 514..515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:514-515)
  on lines 517..518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:517-518)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 291..292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:291-292)
  on lines 294..295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:294-295)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1133 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1133-1133)
  on lines 1138..1139 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1138-1139)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1064..1065 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1064-1065)
  on lines 1075..1076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1075-1076)
  on lines 1086..1087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1086-1087)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 903..904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:903-904)
  on lines 914..915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:914-915)
  on lines 925..926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:925-926)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2614-2614)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2425-2425)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2577-2577)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2725-2725)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2651-2651)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2688-2688)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2462-2462)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:112-112)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 656
  dead: 568 (374 in uncalled functions)
  total lines: 1224
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1082:11-1082:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2576:9-2576:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1083:13-1083:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1108:7-1108:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2595:9-2595:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:900:9-900:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:272:11-272:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2613:9-2613:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:911:11-911:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2369:9-2369:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:480:7-480:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1132:7-1132:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:481:9-481:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:288:7-288:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:921:11-921:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1135:9-1135:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:922:13-922:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2632:9-2632:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:952:7-952:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:953:9-953:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1773:7-1773:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2650:9-2650:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2406:9-2406:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1163:11-1163:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2669:9-2669:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2424:9-2424:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:545:7-545:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1185:11-1185:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:750:11-750:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2687:9-2687:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2443:9-2443:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:550:11-550:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2706:9-2706:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:775:11-775:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2461:9-2461:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2724:9-2724:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:797:11-797:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2224:9-2224:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2773:10-2773:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:845:7-845:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:846:9-846:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:614:7-614:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:618:11-618:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1061:9-1061:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:2558:9-2558:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product34.cil.c:1072:11-1072:21)
[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
