./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_spec11_product30.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_spec11_product30.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1647:3-1668:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1704:3-1729:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1789:5-1809: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 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:253:1-267:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:670:1-684:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:715:1-729:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:732:1-750:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:751:1-766:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:843:1-863:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:864:1-879:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:882:1-902:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:903:1-918:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1069:1-1087:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1107:1-1134:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1135:1-1153:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1154:1-1172:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1173:1-1186:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1216:1-1224:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1245:1-1254:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1383:1-1393:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1472:1-1483:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1484:1-1495:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1576:1-1621:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1622:1-1677:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1678:1-1737:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1740:1-1842:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1843:1-1888:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1889:1-1934:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1952:1-1966:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1970:1-1995:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1996:1-2015:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2020:1-2043:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2044:1-2063:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2067:1-2090:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2091:1-2110:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2111:1-2135:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2145:1-2213:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2214:1-2282:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2283:1-2338:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2348:1-2416:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2417:1-2472:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2911:1-2934:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2935:1-2954:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1566-1566)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2636-2636)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1237-1237)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2842..2844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2842-2844)
  on lines 2846..2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2846-2848)
  on lines 2850..2851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2850-2851)
  on line 2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2860-2860)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 2489..2490 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2489-2490)
  on line 2497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2497-2497)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2971..2972 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2971-2972)
  on line 2979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2979-2979)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2764..2766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2764-2766)
  on lines 2768..2769 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2768-2769)
  on lines 2773..2776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2773-2776)
  on lines 2778..2780 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2778-2780)
  on lines 2782..2783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2782-2783)
  on lines 2787..2790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2787-2790)
  on lines 2792..2794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2792-2794)
  on lines 2796..2797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2796-2797)
  on lines 2801..2802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2801-2802)
  on line 2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2806-2806)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2586..2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2586-2587)
  on line 2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2591-2591)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2657..2659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2657-2659)
  on lines 2661..2662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2661-2662)
  on lines 2666..2669 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2666-2669)
  on lines 2671..2673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2671-2673)
  on lines 2675..2676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2675-2676)
  on lines 2680..2683 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2680-2683)
  on lines 2685..2687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2685-2687)
  on lines 2689..2690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2689-2690)
  on lines 2694..2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2694-2695)
  on line 2699 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2699-2699)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 2536..2537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2536-2537)
  on line 2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2544-2544)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 967..968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:967-968)
  on line 974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:974-974)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 778..779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:778-779)
  on line 785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:785-785)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1041..1042 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1041-1042)
  on line 1048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1048-1048)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 815..816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:815-816)
  on line 822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:822-822)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:306-306)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:315-315)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 930..931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:930-931)
  on line 937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:937-937)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 332..333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:332-333)
  on line 340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:340-340)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1213-1213)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1193 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1193-1193)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1004..1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1004-1005)
  on line 1011 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1011-1011)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:297-297)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2505-2505)
  on lines 2510..2511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2510-2511)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2871..2872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2871-2872)
  on lines 2882..2883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2882-2883)
  on lines 2893..2894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2893-2894)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2710..2711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2710-2711)
  on lines 2721..2722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2721-2722)
  on lines 2732..2733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2732-2733)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:985-985)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 796 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:796-796)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:948-948)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1096-1096)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1022-1022)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1059-1059)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:833-833)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1275-1275)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 523
  dead: 653 (528 in uncalled functions)
  total lines: 1176
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2841:11-2841:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2652:7-2652:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2653:9-2653:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:832:9-832:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1095:9-1095:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1427:7-1427:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2868:9-2868:19)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:331:9-331:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2879:11-2879:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2889:11-2889:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2890:13-2890:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2707:9-2707:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2488:11-2488:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2718:11-2718:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:929:9-929:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2504:7-2504:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2728:11-2728:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2729:13-2729:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2507:9-2507:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:947:9-947:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2759:7-2759:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2760:9-2760:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:966:9-966:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2970:11-2970:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2535:11-2535:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:984:9-984:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2992:11-2992:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:492:10-492:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2557:11-2557:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1003:9-1003:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2582:11-2582:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1021:9-1021:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:777:9-777:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1040:9-1040:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:795:9-795:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:2604:11-2604:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:1058:9-1058:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product30.cil.c:814:9-814:20)
[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
