./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_spec27_product24.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_spec27_product24.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_spec27_product24.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_spec27_product24.cil.c:2621:3-2642:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2678:3-2703:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2763:5-2783: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 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:143:1-151:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:182:1-196:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:218:1-233:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:310:1-330:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:331:1-346:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:349:1-369:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:370:1-385:1)
[Warning][Deadcode] Function 'isEncrypted' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:388:1-406:1)
[Warning][Deadcode] Function 'setEmailIsEncrypted' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:407:1-422:1)
[Warning][Deadcode] Function 'getEmailEncryptionKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:425:1-443:1)
[Warning][Deadcode] Function 'setEmailEncryptionKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:444:1-459:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:607:1-621:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:651:1-665:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:669:1-694:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:695:1-714:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:719:1-742:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:743:1-762:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:766:1-789:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:790:1-809:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:810:1-834:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:844:1-912:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:913:1-981:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:982:1-1037:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1047:1-1115:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1116:1-1171:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1830:1-1844:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2356:1-2366:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2445:1-2456:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2457:1-2468:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2550:1-2595:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2596:1-2651:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2652:1-2711:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2714:1-2816:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2817:1-2862:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2863:1-2908:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2920:1-2929:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2915 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2915-2915)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1335-1335)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:164-164)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1559-1559)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1196-1196)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1631 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1631-1631)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1670..1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1670-1671)
  on line 1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1678-1678)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1463..1465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1463-1465)
  on lines 1467..1468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1467-1468)
  on lines 1472..1475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1472-1475)
  on lines 1477..1479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1477-1479)
  on lines 1481..1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1481-1482)
  on lines 1486..1489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1486-1489)
  on lines 1491..1493 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1491-1493)
  on lines 1495..1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1495-1496)
  on lines 1500..1501 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1500-1501)
  on line 1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1505-1505)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1285..1286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1285-1286)
  on line 1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1290-1290)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1356..1358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1356-1358)
  on lines 1360..1361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1360-1361)
  on lines 1365..1368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1365-1368)
  on lines 1370..1372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1370-1372)
  on lines 1374..1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1374-1375)
  on lines 1379..1382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1379-1382)
  on lines 1384..1386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1384-1386)
  on lines 1388..1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1388-1389)
  on lines 1393..1394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1393-1394)
  on line 1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1398-1398)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1235..1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1235-1236)
  on line 1243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1243-1243)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 245..246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:245-246)
  on line 252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:252-252)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 208..209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:208-209)
  on line 215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:215-215)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 508..509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:508-509)
  on line 515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:515-515)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 282..283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:282-283)
  on line 289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:289-289)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1883-1883)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1892-1892)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1909-1910)
  on line 1917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1917-1917)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:140-140)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 471..472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:471-472)
  on line 478 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:478-478)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 545..546 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:545-546)
  on line 552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:552-552)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1874-1874)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1204 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1204-1204)
  on lines 1209..1210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1209-1210)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1639 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1639-1639)
  on lines 1644..1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1644-1645)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1570..1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1570-1571)
  on lines 1581..1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1581-1582)
  on lines 1592..1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1592-1593)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1409..1410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1409-1410)
  on lines 1420..1421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1420-1421)
  on lines 1431..1432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1431-1432)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:263-263)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:563-563)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:489-489)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 526 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:526-526)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:300-300)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2950-2950)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2001-2001)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 559
  dead: 602 (485 in uncalled functions)
  total lines: 1161
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1406:9-1406:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:488:9-488:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:244:9-244:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1417:11-1417:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:507:9-507:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1638:7-1638:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1203:7-1203:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:262:9-262:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1427:11-1427:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1641:9-1641:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1428:13-1428:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1206:9-1206:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:525:9-525:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:281:9-281:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1458:7-1458:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1459:9-1459:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:544:9-544:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1669:11-1669:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1234:11-1234:22)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1991:7-1991:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:299:9-299:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:562:9-562:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1691:11-1691:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1256:11-1256:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1281:11-1281:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2076:10-2076:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1303:11-1303:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1351:7-1351:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1352:9-1352:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:2400:7-2400:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1567:9-1567:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1578:11-1578:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:207:9-207:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1588:11-1588:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1589:13-1589:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:470:9-470:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product24.cil.c:1908:9-1908:21)
[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
