./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_spec27_product35.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_spec27_product35.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_spec27_product35.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_spec27_product35.cil.c:1383:3-1404:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1440:3-1465:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1525:5-1545: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:184:1-192:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:210:1-224:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:255:1-269:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:273:1-298:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:299:1-318:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:323:1-346:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:347:1-366:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:414:1-438:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:448:1-516:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:517:1-585:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1312:1-1357:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1358:1-1413:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1414:1-1473:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1476:1-1578:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1579:1-1624:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1625:1-1670:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1685:1-1694:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1731:1-1745:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1767:1-1782:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1859:1-1879:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1880:1-1895:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1898:1-1918:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1919:1-1934:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2357:1-2371:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2701:1-2711:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2790:1-2801:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2802:1-2813:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1677-1677)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:939-939)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:205-205)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1163-1163)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 664..666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:664-666)
  on lines 668..669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:668-669)
  on lines 674..677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:674-677)
  on lines 679..681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:679-681)
  on lines 683..685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:683-685)
  on lines 687..688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:687-688)
  on lines 693..696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:693-696)
  on lines 698..700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:698-700)
  on lines 702..704 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:702-704)
  on lines 706..707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:706-707)
  on lines 712..713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:712-713)
  on line 717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:717-717)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:391-391)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:800-800)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1235-1235)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1282 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1282-1282)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1067..1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1067-1069)
  on lines 1071..1072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1071-1072)
  on lines 1076..1079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1076-1079)
  on lines 1081..1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1081-1083)
  on lines 1085..1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1085-1086)
  on lines 1090..1093 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1090-1093)
  on lines 1095..1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1095-1097)
  on lines 1099..1100 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1099-1100)
  on lines 1104..1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1104-1105)
  on line 1109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1109-1109)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 889..890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:889-890)
  on line 894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:894-894)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 960..962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:960-962)
  on lines 964..965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:964-965)
  on lines 969..972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:969-972)
  on lines 974..976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:974-976)
  on lines 978..979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:978-979)
  on lines 983..986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:983-986)
  on lines 988..990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:988-990)
  on lines 992..993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:992-993)
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:997-998)
  on line 1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1002-1002)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:847-847)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1983..1984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1983-1984)
  on line 1990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1990-1990)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1794..1795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1794-1795)
  on line 1801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1801-1801)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1757..1758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1757-1758)
  on line 1764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1764-1764)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2057..2058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2057-2058)
  on line 2064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2064-2064)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1831..1832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1831-1832)
  on line 1838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1838-1838)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2410-2410)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2419-2419)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1946..1947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1946-1947)
  on line 1953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1953-1953)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2436..2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2436-2437)
  on line 2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2444-2444)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:181-181)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:161-161)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2020..2021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2020-2021)
  on line 2027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2027-2027)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2094..2095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2094-2095)
  on line 2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2101-2101)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2401-2401)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 731..732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:731-732)
  on lines 739..741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:739-741)
  on lines 743..744 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:743-744)
  on lines 746..747 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:746-747)
  on lines 754..756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:754-756)
  on lines 758..759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:758-759)
  on lines 761..762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:761-762)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 594..595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:594-595)
  on lines 597..598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:597-598)
  on lines 605..607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:605-607)
  on lines 609..610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:609-610)
  on lines 612..613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:612-613)
  on lines 620..622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:620-622)
  on lines 624..625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:624-625)
  on lines 627..628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:627-628)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 401..402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:401-402)
  on lines 404..405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:404-405)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:808-808)
  on lines 813..814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:813-814)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1243-1243)
  on lines 1248..1249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1248-1249)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1174..1175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1174-1175)
  on lines 1185..1186 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1185-1186)
  on lines 1196..1197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1196-1197)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1013..1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1013-1014)
  on lines 1024..1025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1024-1025)
  on lines 1035..1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1035-1036)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2001-2001)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1812-1812)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1964-1964)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2112-2112)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2038-2038)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2075-2075)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1849-1849)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1715-1715)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 690
  dead: 547 (355 in uncalled functions)
  total lines: 1237
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:907:11-907:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1945:9-1945:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1963:9-1963:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:955:7-955:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:956:9-956:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:724:7-724:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1982:9-1982:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:728:11-728:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1171:9-1171:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2000:9-2000:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2941:10-2941:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1756:9-1756:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1182:11-1182:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2019:9-2019:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1192:11-1192:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1193:13-1193:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2037:9-2037:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1793:9-1793:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1010:9-1010:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2056:9-2056:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1021:11-1021:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1811:9-1811:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:590:7-590:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1242:7-1242:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:591:9-591:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:398:7-398:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:807:7-807:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1031:11-1031:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1245:9-1245:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1032:13-1032:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:810:9-810:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2074:9-2074:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1830:9-1830:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1062:7-1062:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1063:9-1063:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2093:9-2093:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2745:7-2745:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1848:9-1848:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2111:9-2111:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:2435:9-2435:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:655:7-655:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:1295:11-1295:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:860:11-860:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:660:11-660:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product35.cil.c:885:11-885:22)
[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)
