./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_product27.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_product27.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_product27.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_product27.cil.c:2026:3-2047:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2083:3-2108:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2168:5-2188: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_spec4_product27.cil.c:60:1-74:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:324:1-333:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:387:1-401:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:405:1-430:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:431:1-450:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:455:1-478:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:479:1-498:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:546:1-570:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:580:1-648:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:649:1-717:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1460:1-1474:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1496:1-1511:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1588:1-1608:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1609:1-1624:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1627:1-1647:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1648:1-1663:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1666:1-1684:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1685:1-1700:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1703:1-1721:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1722:1-1737:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1924:1-1932:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1955:1-2000:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2001:1-2056:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2057:1-2116:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2119:1-2221:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2222:1-2267:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2268:1-2313:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2419:1-2429:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2508:1-2519:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2520:1-2531:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2782:1-2796:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:54-54)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1071-1071)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1945-1945)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1295-1295)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 796..798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:796-798)
  on lines 800..801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:800-801)
  on lines 806..809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:806-809)
  on lines 811..813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:811-813)
  on lines 815..817 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:815-817)
  on lines 819..820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:819-820)
  on lines 825..828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:825-828)
  on lines 830..832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:830-832)
  on lines 834..836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:834-836)
  on lines 838..839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:838-839)
  on lines 844..845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:844-845)
  on line 849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:849-849)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:523-523)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:932-932)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1367 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1367-1367)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1414-1414)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1199..1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1199-1201)
  on lines 1203..1204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1203-1204)
  on lines 1208..1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1208-1211)
  on lines 1213..1215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1213-1215)
  on lines 1217..1218 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1217-1218)
  on lines 1222..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1222-1225)
  on lines 1227..1229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1227-1229)
  on lines 1231..1232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1231-1232)
  on lines 1236..1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1236-1237)
  on line 1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1241-1241)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1021..1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1021-1022)
  on line 1026 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1026-1026)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1092..1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1092-1094)
  on lines 1096..1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1096-1097)
  on lines 1101..1104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1101-1104)
  on lines 1106..1108 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1106-1108)
  on lines 1110..1111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1110-1111)
  on lines 1115..1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1115-1118)
  on lines 1120..1122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1120-1122)
  on lines 1124..1125 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1124-1125)
  on lines 1129..1130 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1129-1130)
  on line 1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1134-1134)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:979-979)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1523..1524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1523-1524)
  on line 1530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1530-1530)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1486..1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1486-1487)
  on line 1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1493-1493)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1786..1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1786-1787)
  on line 1793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1793-1793)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1560..1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1560-1561)
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1567-1567)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2835 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2835-2835)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2844-2844)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2861..2862 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2861-2862)
  on line 2869 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2869-2869)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1921 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1921-1921)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1749..1750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1749-1750)
  on line 1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1756-1756)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1823..1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1823-1824)
  on line 1830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1830-1830)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2826-2826)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 863..864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:863-864)
  on lines 871..873 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:871-873)
  on lines 875..876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:875-876)
  on lines 878..879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:878-879)
  on lines 886..888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:886-888)
  on lines 890..891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:890-891)
  on lines 893..894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:893-894)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 726..727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:726-727)
  on lines 729..730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:729-730)
  on lines 737..739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:737-739)
  on lines 741..742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:741-742)
  on lines 744..745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:744-745)
  on lines 752..754 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:752-754)
  on lines 756..757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:756-757)
  on lines 759..760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:759-760)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 533..534 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:533-534)
  on lines 536..537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:536-537)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:940-940)
  on lines 945..946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:945-946)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1375-1375)
  on lines 1380..1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1380-1381)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1306..1307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1306-1307)
  on lines 1317..1318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1317-1318)
  on lines 1328..1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1328-1329)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1145..1146 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1145-1146)
  on lines 1156..1157 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1156-1157)
  on lines 1167..1168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1167-1168)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1541-1541)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1841 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1841-1841)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1767-1767)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1804-1804)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1578-1578)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:354-354)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2960-2960)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 624
  dead: 567 (383 in uncalled functions)
  total lines: 1191
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1142:9-1142:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1153:11-1153:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:722:7-722:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:723:9-723:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:530:7-530:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1374:7-1374:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:939:7-939:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1163:11-1163:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1377:9-1377:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1164:13-1164:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:942:9-942:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1194:7-1194:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1195:9-1195:19)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2860:9-2860:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:787:7-787:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1427:11-1427:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:992:11-992:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:792:11-792:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1017:11-1017:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2950:7-2950:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1485:9-1485:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1748:9-1748:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1039:11-1039: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_product27.cil.c:126:10-126:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1766:9-1766:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1522:9-1522:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1785:9-1785:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1087:7-1087:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1088:9-1088:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1540:9-1540:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:856:7-856:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:860:11-860:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1803:9-1803:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1559:9-1559:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1303:9-1303:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1822:9-1822:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1577:9-1577:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1314:11-1314:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1324:11-1324:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1840:9-1840:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:1325:13-1325:23)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec4_product27.cil.c:2463:7-2463:10)
[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
