./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_spec4_product32.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_spec4_product32.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_spec4_product32.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_spec4_product32.cil.c:2168:3-2189:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2225:3-2250:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2310:5-2330: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 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:127:1-141:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:145:1-170:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:171:1-190:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:195:1-218:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:219:1-238:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:286:1-310:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:320:1-388:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:389:1-457:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1086:1-1109:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1110:1-1129:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1294:1-1304:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1383:1-1394:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1395:1-1406:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1508:1-1535:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1536:1-1554:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1555:1-1573:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1574:1-1587:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1617:1-1625:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1855:1-1869:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2075:1-2089:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2097:1-2142:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2143:1-2198:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2199:1-2258:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2261:1-2363:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2364:1-2409:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2410:1-2455:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2683:1-2697:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2700:1-2718:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2719:1-2734:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2811:1-2831:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2832:1-2847:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2850:1-2870:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2871:1-2886:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:3037:1-3055:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1490-1490)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:811-811)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1638-1638)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1035-1035)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 536..538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:536-538)
  on lines 540..541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:540-541)
  on lines 546..549 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:546-549)
  on lines 551..553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:551-553)
  on lines 555..557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:555-557)
  on lines 559..560 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:559-560)
  on lines 565..568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:565-568)
  on lines 570..572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:570-572)
  on lines 574..576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:574-576)
  on lines 578..579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:578-579)
  on lines 584..585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:584-585)
  on line 589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:589-589)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:263-263)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:672-672)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1154-1154)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 939..941 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:939-941)
  on lines 943..944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:943-944)
  on lines 948..951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:948-951)
  on lines 953..955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:953-955)
  on lines 957..958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:957-958)
  on lines 962..965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:962-965)
  on lines 967..969 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:967-969)
  on lines 971..972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:971-972)
  on lines 976..977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:976-977)
  on line 981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:981-981)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 761..762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:761-762)
  on line 766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:766-766)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 832..834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:832-834)
  on lines 836..837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:836-837)
  on lines 841..844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:841-844)
  on lines 846..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:846-848)
  on lines 850..851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:850-851)
  on lines 855..858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:855-858)
  on lines 860..862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:860-862)
  on lines 864..865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:864-865)
  on lines 869..870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:869-870)
  on line 874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:874-874)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:719-719)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2935..2936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2935-2936)
  on line 2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2942-2942)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2746..2747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2746-2747)
  on line 2753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2753-2753)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 3009..3010 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:3009-3010)
  on line 3016 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:3016-3016)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2783..2784 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2783-2784)
  on line 2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2790-2790)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1908-1908)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1917-1917)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2898..2899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2898-2899)
  on line 2905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2905-2905)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1934..1935 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1934-1935)
  on line 1942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1942-1942)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1614-1614)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1594-1594)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2972..2973 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2972-2973)
  on line 2979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2979-2979)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1899-1899)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 603..604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:603-604)
  on lines 611..613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:611-613)
  on lines 615..616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:615-616)
  on lines 618..619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:618-619)
  on lines 626..628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:626-628)
  on lines 630..631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:630-631)
  on lines 633..634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:633-634)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 466..467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:466-467)
  on lines 469..470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:469-470)
  on lines 477..479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:477-479)
  on lines 481..482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:481-482)
  on lines 484..485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:484-485)
  on lines 492..494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:492-494)
  on lines 496..497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:496-497)
  on lines 499..500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:499-500)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 273..274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:273-274)
  on lines 276..277 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:276-277)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:680-680)
  on lines 685..686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:685-686)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1046..1047 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1046-1047)
  on lines 1057..1058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1057-1058)
  on lines 1068..1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1068-1069)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 885..886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:885-886)
  on lines 896..897 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:896-897)
  on lines 907..908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:907-908)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2953-2953)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2764-2764)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2916-2916)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:3064-3064)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2990-2990)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 3027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:3027-3027)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2801-2801)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:94-94)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 602
  dead: 608 (426 in uncalled functions)
  total lines: 1210
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:882:9-882:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:893:11-893:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:462:7-462:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:463:9-463:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:270:7-270:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:679:7-679:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:903:11-903:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:904:13-904:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:682:9-682:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:934:7-934:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:935:9-935:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2897:9-2897:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2915:9-2915:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:527:7-527:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1167:11-1167:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2934:9-2934:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:732:11-732:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:532:11-532:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2952:9-2952:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:757:11-757:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2971:9-2971:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:779:11-779:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2496:10-2496:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2989:9-2989:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2745:9-2745:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:3008:9-3008:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2763:9-2763:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:827:7-827:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:828:9-828:19)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1933:9-1933:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:3026:9-3026:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:596:7-596:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2782:9-2782:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:600:11-600:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1338:7-1338:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1043:9-1043:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:2800:9-2800:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1054:11-1054:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:3063:9-3063:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1064:11-1064:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product32.cil.c:1065:13-1065:23)
[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
