./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_spec7_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_spec7_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_spec7_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_spec7_product31.cil.c:1241:3-1262:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1298:3-1323:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1383:5-1403: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 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:186:1-196:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:275:1-286:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:287:1-298:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:580:1-594:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:774:1-788:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:810:1-825:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:902:1-922:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:923:1-938:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:941:1-961:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:962:1-977:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1170:1-1215:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1216:1-1271:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1272:1-1331:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1334:1-1436:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1437:1-1482:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1483:1-1528:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1640:1-1648:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1666:1-1680:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1683:1-1692:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1733:1-1747:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1751:1-1776:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1777:1-1796:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1801:1-1824:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1825:1-1844:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1848:1-1871:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1872:1-1891:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1892:1-1916:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1926:1-1994:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1995:1-2063:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2064:1-2119:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2129:1-2197:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2198:1-2253:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2257:1-2280:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2281:1-2300:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:389-389)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2417-2417)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1661-1661)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2600..2601 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2600-2601)
  on line 2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2641-2641)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 2697..2698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2697-2698)
  on line 2713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2713-2713)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2752..2753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2752-2753)
  on line 2760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2760-2760)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2545..2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2545-2547)
  on lines 2549..2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2549-2550)
  on lines 2554..2557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2554-2557)
  on lines 2559..2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2559-2561)
  on lines 2563..2564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2563-2564)
  on lines 2568..2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2568-2571)
  on lines 2573..2575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2573-2575)
  on lines 2577..2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2577-2578)
  on lines 2582..2583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2582-2583)
  on line 2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2587-2587)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2367..2368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2367-2368)
  on line 2372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2372-2372)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2438..2440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2438-2440)
  on lines 2442..2443 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2442-2443)
  on lines 2447..2450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2447-2450)
  on lines 2452..2454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2452-2454)
  on lines 2456..2457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2456-2457)
  on lines 2461..2464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2461-2464)
  on lines 2466..2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2466-2468)
  on lines 2470..2471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2470-2471)
  on lines 2475..2476 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2475-2476)
  on line 2480 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2480-2480)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2325-2325)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1026..1027 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1026-1027)
  on line 1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1033-1033)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 837..838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:837-838)
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:844-844)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 800..801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:800-801)
  on line 807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:807-807)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1100..1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1100-1101)
  on line 1107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1107-1107)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 874..875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:874-875)
  on line 881 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:881-881)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:633-633)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:642-642)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 989..990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:989-990)
  on line 996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:996-996)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 659..660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:659-660)
  on line 667 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:667-667)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1637-1637)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 1617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1617-1617)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1063..1064 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1063-1064)
  on line 1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1070-1070)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1137..1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1137-1138)
  on line 1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1144-1144)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:624-624)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2721-2721)
  on lines 2726..2727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2726-2727)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2652..2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2652-2653)
  on lines 2663..2664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2663-2664)
  on lines 2674..2675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2674-2675)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2491..2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2491-2492)
  on lines 2502..2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2502-2503)
  on lines 2513..2514 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2513-2514)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1044 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1044-1044)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:855-855)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1007 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1007-1007)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1155 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1155-1155)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1081-1081)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1118-1118)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:892-892)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1713-1713)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 581
  dead: 599 (476 in uncalled functions)
  total lines: 1180
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1154:9-1154:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:658:9-658:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2433:7-2433:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2434:9-2434:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2649:9-2649:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2660:11-2660:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:988:9-988:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2670:11-2670:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2671:13-2671:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2696:7-2696:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1006:9-1006:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2488:9-2488:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1025:9-1025:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2499:11-2499:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2720:7-2720:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2509:11-2509:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2723:9-2723:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2510:13-2510:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1043:9-1043:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:799:9-799:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2540:7-2540:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2541:9-2541:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1062:9-1062:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2751:11-2751:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1080:9-1080:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:836:9-836:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1099:9-1099:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2773:11-2773:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2338:11-2338:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:854:9-854:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:230:7-230:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1117:9-1117:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:873:9-873:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2363:11-2363:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:1136:9-1136:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2823:10-2823:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:891:9-891:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2599:11-2599:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec7_product31.cil.c:2385:11-2385:22)
[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
