./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_spec8_product22.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_spec8_product22.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_spec8_product22.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_spec8_product22.cil.c:1084:3-1105:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1141:3-1166:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1226:5-1246: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_spec8_product22.cil.c:188:1-198:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:277:1-288:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:289:1-300:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:398:1-412:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:434:1-449:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:526:1-546:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:547:1-562:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:565:1-585:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:586:1-601:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:678:1-696:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:697:1-712:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:715:1-733:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:734:1-749:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:752:1-770:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:771:1-786:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1013:1-1058:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1059:1-1114:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1115:1-1174:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1177:1-1279:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1280:1-1325:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1326:1-1371:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1383:1-1397:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1577:1-1591:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1706:1-1715:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1754:1-1768:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1772:1-1797:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1798:1-1817:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1822:1-1845:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1846:1-1865:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1869:1-1892:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1893:1-1912:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1913:1-1937:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1947:1-2015:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2016:1-2084:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2085:1-2140:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2150:1-2218:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2219:1-2274:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2883:1-2891:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1378-1378)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2438 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2438-2438)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2904-2904)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 2621..2622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2621-2622)
  on lines 2644..2646 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2644-2646)
  on lines 2648..2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2648-2650)
  on lines 2652..2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2652-2653)
  on line 2662 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2662-2662)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2299-2299)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2734-2734)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2773..2774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2773-2774)
  on line 2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2781-2781)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2566..2568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2566-2568)
  on lines 2570..2571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2570-2571)
  on lines 2575..2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2575-2578)
  on lines 2580..2582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2580-2582)
  on lines 2584..2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2584-2585)
  on lines 2589..2592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2589-2592)
  on lines 2594..2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2594-2596)
  on lines 2598..2599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2598-2599)
  on lines 2603..2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2603-2604)
  on line 2608 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2608-2608)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2388..2389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2388-2389)
  on line 2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2393-2393)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2459..2461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2459-2461)
  on lines 2463..2464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2463-2464)
  on lines 2468..2471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2468-2471)
  on lines 2473..2475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2473-2475)
  on lines 2477..2478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2477-2478)
  on lines 2482..2485 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2482-2485)
  on lines 2487..2489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2487-2489)
  on lines 2491..2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2491-2492)
  on lines 2496..2497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2496-2497)
  on line 2501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2501-2501)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2346-2346)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 650..651 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:650-651)
  on line 657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:657-657)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 461..462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:461-462)
  on line 468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:468-468)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 424..425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:424-425)
  on line 431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:431-431)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 498..499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:498-499)
  on line 505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:505-505)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1630-1630)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1639-1639)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 613..614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:613-614)
  on line 620 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:620-620)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1656..1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1656-1657)
  on line 1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1664-1664)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2880 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2880-2880)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2860-2860)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1621-1621)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2307-2307)
  on lines 2312..2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2312-2313)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2742-2742)
  on lines 2747..2748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2747-2748)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2673..2674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2673-2674)
  on lines 2684..2685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2684-2685)
  on lines 2695..2696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2695-2696)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2512..2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2512-2513)
  on lines 2523..2524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2523-2524)
  on lines 2534..2535 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2534-2535)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:668-668)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:479-479)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:631-631)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:516-516)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1736 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1736-1736)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 538
  dead: 620 (499 in uncalled functions)
  total lines: 1158
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2794:11-2794:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2359:11-2359:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2384:11-2384:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:612:9-612:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2620:11-2620:48)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2406:11-2406:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:630:9-630:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:649:9-649:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2643:11-2643:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2454:7-2454:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2455:9-2455:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:667:9-667:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:423:9-423:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2670:9-2670:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2681:11-2681:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:460:9-460:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2691:11-2691:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2692:13-2692:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:478:9-478:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2509:9-2509:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:497:9-497:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2520:11-2520:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2741:7-2741:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2306:7-2306:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2530:11-2530:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2744:9-2744:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2531:13-2531:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:515:9-515:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2309:9-2309:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2561:7-2561:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2562:9-2562:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:232:7-232:10)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:1655:9-1655:21)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:2772:11-2772:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product22.cil.c:827:10-827:11)
[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
