./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_product15.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_product15.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_product15.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_product15.cil.c:2579:3-2600:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2636:3-2661:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2721:5-2741: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 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:71:1-85:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:88:1-106:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:107:1-122:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:199:1-219:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:220:1-235:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:238:1-258:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:259:1-274:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:351:1-369:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:370:1-385:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:388:1-406:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:407:1-422:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:425:1-443:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:444:1-459:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:635:1-649:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:774:1-788:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:792:1-817:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:818:1-837:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:842:1-865:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:866:1-885:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:889:1-912:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:913:1-932:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:933:1-957:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:967:1-1035:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1036:1-1104:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1105:1-1160:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1170:1-1238:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1239:1-1294:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1733:1-1756:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1757:1-1776:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1935:1-1945:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2024:1-2035:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2036:1-2047:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2168:1-2195:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2196:1-2214:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2215:1-2223:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2224:1-2243:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2244:1-2252:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2486:1-2500:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2508:1-2553:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2554:1-2609:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2610:1-2669:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2672:1-2774:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2775:1-2820:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2821:1-2866:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2869:1-2878:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2161-2161)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1458-1458)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2265-2265)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1641..1642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1641-1642)
  on lines 1664..1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1664-1666)
  on lines 1668..1670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1668-1670)
  on lines 1672..1673 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1672-1673)
  on line 1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1682-1682)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 1311..1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1311-1312)
  on line 1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1319-1319)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1793..1794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1793-1794)
  on line 1801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1801-1801)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1586..1588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1586-1588)
  on lines 1590..1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1590-1591)
  on lines 1595..1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1595-1598)
  on lines 1600..1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1600-1602)
  on lines 1604..1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1604-1605)
  on lines 1609..1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1609-1612)
  on lines 1614..1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1614-1616)
  on lines 1618..1619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1618-1619)
  on lines 1623..1624 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1623-1624)
  on line 1628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1628-1628)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1408..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1408-1409)
  on line 1413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1413-1413)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1479..1481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1479-1481)
  on lines 1483..1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1483-1484)
  on lines 1488..1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1488-1491)
  on lines 1493..1495 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1493-1495)
  on lines 1497..1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1497-1498)
  on lines 1502..1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1502-1505)
  on lines 1507..1509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1507-1509)
  on lines 1511..1512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1511-1512)
  on lines 1516..1517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1516-1517)
  on line 1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1521-1521)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1358..1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1358-1359)
  on line 1366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1366-1366)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 323..324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:323-324)
  on line 330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:330-330)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 134..135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:134-135)
  on line 141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:141-141)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 171..172 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:171-172)
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:178-178)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:688-688)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:697-697)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 286..287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:286-287)
  on line 293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:293-293)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 714..715 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:714-715)
  on line 722 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:722-722)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 679 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:679-679)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1327-1327)
  on lines 1332..1333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1332-1333)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1693..1694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1693-1694)
  on lines 1704..1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1704-1705)
  on lines 1715..1716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1715-1716)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1532..1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1532-1533)
  on lines 1543..1544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1543-1544)
  on lines 1554..1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1554-1555)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:341-341)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 152 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:152-152)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:304-304)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:189-189)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2899-2899)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 460
  dead: 674 (558 in uncalled functions)
  total lines: 1134
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1663:11-1663:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1474:7-1474:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1475:9-1475:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1979:7-1979:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1690:9-1690:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1701:11-1701:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:2308:10-2308:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1711:11-1711:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1712:13-1712:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:285:9-285:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:303:9-303:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1529:9-1529:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1310:11-1310:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1540:11-1540:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:322:9-322:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1326:7-1326:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1550:11-1550:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1551:13-1551:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1329:9-1329:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:340:9-340:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1581:7-1581:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1582:9-1582:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1792:11-1792:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1357:11-1357:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:133:9-133:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:713:9-713:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1814:11-1814:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1379:11-1379:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1404:11-1404:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:170:9-170: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_product15.cil.c:1640:11-1640:48)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:188:9-188:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product15.cil.c:1426:11-1426: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
