./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_product33.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_product33.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_product33.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_product33.cil.c:153:3-174:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:210:3-235:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:295:5-315: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_spec27_product33.cil.c:60:1-74:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:82:1-127:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:128:1-183:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:184:1-243:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:246:1-348:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:349:1-394:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:395:1-440:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:580:1-590:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:669:1-680:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:681:1-692:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:891:1-899:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1168:1-1177:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1214:1-1228:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1250:1-1265:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1342:1-1362:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1363:1-1378:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1381:1-1401:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1402:1-1417:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1623:1-1637:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1641:1-1666:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1667:1-1686:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1691:1-1714:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1715:1-1734:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1738:1-1761:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1762:1-1781:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1782:1-1806:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1816:1-1884:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1885:1-1953:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1954:1-2009:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2019:1-2087:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2088:1-2143:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2864:1-2878:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:54-54)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2307 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2307-2307)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 912 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:912-912)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2531-2531)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2168-2168)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2603 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2603-2603)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 2642..2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2642-2643)
  on line 2650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2650-2650)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2435..2437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2435-2437)
  on lines 2439..2440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2439-2440)
  on lines 2444..2447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2444-2447)
  on lines 2449..2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2449-2451)
  on lines 2453..2454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2453-2454)
  on lines 2458..2461 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2458-2461)
  on lines 2463..2465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2463-2465)
  on lines 2467..2468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2467-2468)
  on lines 2472..2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2472-2473)
  on line 2477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2477-2477)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2257..2258 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2257-2258)
  on line 2262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2262-2262)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2328..2330 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2328-2330)
  on lines 2332..2333 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2332-2333)
  on lines 2337..2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2337-2340)
  on lines 2342..2344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2342-2344)
  on lines 2346..2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2346-2347)
  on lines 2351..2354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2351-2354)
  on lines 2356..2358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2356-2358)
  on lines 2360..2361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2360-2361)
  on lines 2365..2366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2365-2366)
  on line 2370 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2370-2370)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2215-2215)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1466..1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1466-1467)
  on line 1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1473-1473)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1277..1278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1277-1278)
  on line 1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1284-1284)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1240..1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1240-1241)
  on line 1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1247-1247)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1540..1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1540-1541)
  on line 1547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1547-1547)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1314..1315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1314-1315)
  on line 1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1321-1321)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2917 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2917-2917)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2926 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2926-2926)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1429..1430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1429-1430)
  on line 1436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1436-1436)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2943..2944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2943-2944)
  on line 2951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2951-2951)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:888-888)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:868-868)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1503..1504 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1503-1504)
  on line 1510 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1510-1510)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1577..1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1577-1578)
  on line 1584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1584-1584)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2908-2908)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2176-2176)
  on lines 2181..2182 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2181-2182)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2611 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2611-2611)
  on lines 2616..2617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2616-2617)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2542..2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2542-2543)
  on lines 2553..2554 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2553-2554)
  on lines 2564..2565 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2564-2565)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2381..2382 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2381-2382)
  on lines 2392..2393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2392-2393)
  on lines 2403..2404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2403-2404)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1484-1484)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1295-1295)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1447-1447)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1595-1595)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1521 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1521-1521)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1558-1558)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1332-1332)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1198-1198)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 625
  dead: 580 (457 in uncalled functions)
  total lines: 1205
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1428:9-1428:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2539:9-2539:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2550:11-2550:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1446:9-1446:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:624:7-624:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2560:11-2560:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2561:13-2561:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1465:9-1465:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:955:10-955:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2378:9-2378:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1483:9-1483:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1239:9-1239:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2389:11-2389:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1502:9-1502:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2610:7-2610:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2175:7-2175:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2399:11-2399:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2613:9-2613:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2400:13-2400:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2178:9-2178:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1520:9-1520:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1276:9-1276:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2430:7-2430:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2431:9-2431:19)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2942:9-2942:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1539:9-1539:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2641:11-2641:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1294:9-1294:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1557:9-1557:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1313:9-1313:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2663:11-2663:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2228:11-2228:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1576:9-1576:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1331:9-1331:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2253:11-2253:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:1594:9-1594:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2275:11-2275:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2323:7-2323:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_product33.cil.c:2324:9-2324:19)
[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
