./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_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_spec11_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_spec11_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_spec11_product22.cil.c:2197:3-2218:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2254:3-2279:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2339:5-2359: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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:186:1-194:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:388:1-402:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:772:1-786:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:790:1-815:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:816:1-835:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:840:1-863:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:864:1-883:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:887:1-910:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:911:1-930:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:931:1-955:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:965:1-1033:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1034:1-1102:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1103:1-1158:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1168:1-1236:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1237:1-1292:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1932:1-1942:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2021:1-2032:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2033:1-2044:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2126:1-2171:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2172:1-2227:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2228:1-2287:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2290:1-2392:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2393:1-2438:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2439:1-2484:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2487:1-2496:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2534:1-2548:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2570:1-2585:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2662:1-2682:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2683:1-2698:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2701:1-2721:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2722:1-2737:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2814:1-2832:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2833:1-2848:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2851:1-2869:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2870:1-2885:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2888:1-2906:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2907:1-2922:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1828-1828)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1456-1456)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:207-207)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1639..1640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1639-1640)
  on lines 1662..1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1662-1664)
  on lines 1666..1668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1666-1668)
  on lines 1670..1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1670-1671)
  on line 1680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1680-1680)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1317-1317)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1752-1752)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1791..1792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1791-1792)
  on line 1799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1799-1799)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1584..1586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1584-1586)
  on lines 1588..1589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1588-1589)
  on lines 1593..1596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1593-1596)
  on lines 1598..1600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1598-1600)
  on lines 1602..1603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1602-1603)
  on lines 1607..1610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1607-1610)
  on lines 1612..1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1612-1614)
  on lines 1616..1617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1616-1617)
  on lines 1621..1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1621-1622)
  on line 1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1626-1626)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1406..1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1406-1407)
  on line 1411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1411-1411)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1477..1479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1477-1479)
  on lines 1481..1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1481-1482)
  on lines 1486..1489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1486-1489)
  on lines 1491..1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1491-1493)
  on lines 1495..1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1495-1496)
  on lines 1500..1503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1500-1503)
  on lines 1505..1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1505-1507)
  on lines 1509..1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1509-1510)
  on lines 1514..1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1514-1515)
  on line 1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1519-1519)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1364-1364)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2786..2787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2786-2787)
  on line 2793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2793-2793)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2597..2598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2597-2598)
  on line 2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2604-2604)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2560..2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2560-2561)
  on line 2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2567-2567)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2634..2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2634-2635)
  on line 2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2641-2641)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:441-441)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 450 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:450-450)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2749..2750 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2749-2750)
  on line 2756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2756-2756)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 467..468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:467-468)
  on line 475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:475-475)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:183-183)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 163 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:163-163)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:432-432)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1325-1325)
  on lines 1330..1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1330-1331)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1760-1760)
  on lines 1765..1766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1765-1766)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1691..1692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1691-1692)
  on lines 1702..1703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1702-1703)
  on lines 1713..1714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1713-1714)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1530..1531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1530-1531)
  on lines 1541..1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1541-1542)
  on lines 1552..1553 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1552-1553)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2804-2804)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2615-2615)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2767-2767)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2652-2652)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2517-2517)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 528
  dead: 620 (499 in uncalled functions)
  total lines: 1148
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1688:9-1688:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1976:7-1976:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2596:9-2596:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1699:11-1699:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1709:11-1709:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1710:13-1710:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2614:9-2614:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2633:9-2633:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1527:9-1527:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1538:11-1538:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2651:9-2651:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1759:7-1759:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1324:7-1324:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1548:11-1548:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1762:9-1762:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1549:13-1549:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1327:9-1327:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1579:7-1579:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1580:9-1580:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1790:11-1790:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1812:11-1812:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1377:11-1377:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:466:9-466:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1402:11-1402:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2748:9-2748:20)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1638:11-1638:48)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2766:9-2766:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1424:11-1424:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2785:9-2785:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1661:11-1661:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1472:7-1472:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2803:9-2803:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:1473:9-1473:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:2559:9-2559:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_product22.cil.c:570:10-570: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
