./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_spec3_product31.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_spec3_product31.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_spec3_product31.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_spec3_product31.cil.c:1513:3-1534:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1570:3-1595:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1655:5-1675: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 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:78:1-92:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:96:1-121:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:122:1-141:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:146:1-169:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:170:1-189:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:193:1-216:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:217:1-236:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:237:1-261:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:271:1-339:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:340:1-408:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:409:1-464:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:474:1-542:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:543:1-598:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:602:1-625:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:626:1-645:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1258:1-1268:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1347:1-1358:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1359:1-1370:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1442:1-1487:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1488:1-1543:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1544:1-1603:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1606:1-1708:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1709:1-1754:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1755:1-1800:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1803:1-1812:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2249:1-2263:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2504:1-2518:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2540:1-2555:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2632:1-2652:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2653:1-2668:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2671:1-2691:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2692:1-2707:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:3004:1-3012:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:3030:1-3044:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1842-1842)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 762 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:762-762)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:3025-3025)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 945..946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:945-946)
  on line 986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:986-986)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1042..1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1042-1043)
  on line 1058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1058-1058)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1097..1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1097-1098)
  on line 1105 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1105-1105)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 890..892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:890-892)
  on lines 894..895 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:894-895)
  on lines 899..902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:899-902)
  on lines 904..906 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:904-906)
  on lines 908..909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:908-909)
  on lines 913..916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:913-916)
  on lines 918..920 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:918-920)
  on lines 922..923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:922-923)
  on lines 927..928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:927-928)
  on line 932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:932-932)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 712..713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:712-713)
  on line 717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:717-717)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 783..785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:783-785)
  on lines 787..788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:787-788)
  on lines 792..795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:792-795)
  on lines 797..799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:797-799)
  on lines 801..802 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:801-802)
  on lines 806..809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:806-809)
  on lines 811..813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:811-813)
  on lines 815..816 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:815-816)
  on lines 820..821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:820-821)
  on line 825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:825-825)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:670-670)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2756..2757 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2756-2757)
  on line 2763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2763-2763)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2567..2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2567-2568)
  on line 2574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2574-2574)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2530..2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2530-2531)
  on line 2537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2537-2537)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2830..2831 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2830-2831)
  on line 2837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2837-2837)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2604..2605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2604-2605)
  on line 2611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2611-2611)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2302-2302)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2311-2311)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2719..2720 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2719-2720)
  on line 2726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2726-2726)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2328..2329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2328-2329)
  on line 2336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2336-2336)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 3001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:3001-3001)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2981-2981)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2793..2794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2793-2794)
  on line 2800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2800-2800)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2867..2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2867-2868)
  on line 2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2874-2874)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2293-2293)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1066-1066)
  on lines 1071..1072 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1071-1072)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 997..998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:997-998)
  on lines 1008..1009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1008-1009)
  on lines 1019..1020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1019-1020)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 836..837 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:836-837)
  on lines 847..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:847-848)
  on lines 858..859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:858-859)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2774-2774)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2585-2585)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2737-2737)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2885-2885)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2811-2811)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2848-2848)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2622-2622)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1833-1833)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 600
  dead: 599 (476 in uncalled functions)
  total lines: 1199
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2810:9-2810:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:844:11-844:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2566:9-2566:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1065:7-1065:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:854:11-854:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:855:13-855:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2829:9-2829:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1068:9-1068:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2584:9-2584:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:885:7-885:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:886:9-886:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2847:9-2847:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2603:9-2603:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1096:11-1096:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2327:9-2327:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2866:9-2866:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2621:9-2621:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1118:11-1118:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:683:11-683:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2884:9-2884:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:708:11-708:22)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:944:11-944:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:730:11-730:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2718:9-2718:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:778:7-778:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:779:9-779:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1885:10-1885:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2736:9-2736:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1302:7-1302:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:994:9-994:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2755:9-2755:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1005:11-1005:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2773:9-2773:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1015:11-1015:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2529:9-2529:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1016:13-1016:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:2792:9-2792:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:1041:7-1041:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product31.cil.c:833:9-833:19)
[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
