./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_spec3_product32.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_spec3_product32.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_spec3_product32.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_spec3_product32.cil.c:2818:3-2839:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2875:3-2900:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2960:5-2980: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 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:73:1-82:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:344:1-358:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:543:1-557:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:867:1-881:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:885:1-910:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:911:1-930:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:935:1-958:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:959:1-978:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1026:1-1050:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1060:1-1128:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1129:1-1197:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1826:1-1849:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1850:1-1869:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2015:1-2025:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2104:1-2115:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2116:1-2127:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2210:1-2237:1)
[Warning][Deadcode] Function 'printMail__wrappee__AddressBook' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2238:1-2256:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2257:1-2275:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2276:1-2289:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2319:1-2327:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2351:1-2365:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2368:1-2386:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2387:1-2402:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2479:1-2499:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2500:1-2515:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2518:1-2538:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2539:1-2554:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2705:1-2723:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2747:1-2792:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2793:1-2848:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2849:1-2908:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2911:1-3013:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:3014:1-3059:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:3060:1-3105:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 54 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:54-54)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1551-1551)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2340-2340)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1775-1775)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1276..1278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1276-1278)
  on lines 1280..1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1280-1281)
  on lines 1286..1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1286-1289)
  on lines 1291..1293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1291-1293)
  on lines 1295..1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1295-1297)
  on lines 1299..1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1299-1300)
  on lines 1305..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1305-1308)
  on lines 1310..1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1310-1312)
  on lines 1314..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1314-1316)
  on lines 1318..1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1318-1319)
  on lines 1324..1325 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1324-1325)
  on line 1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1329-1329)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1003-1003)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1412-1412)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1894-1894)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1679..1681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1679-1681)
  on lines 1683..1684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1683-1684)
  on lines 1688..1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1688-1691)
  on lines 1693..1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1693-1695)
  on lines 1697..1698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1697-1698)
  on lines 1702..1705 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1702-1705)
  on lines 1707..1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1707-1709)
  on lines 1711..1712 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1711-1712)
  on lines 1716..1717 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1716-1717)
  on line 1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1721-1721)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1501..1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1501-1502)
  on line 1506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1506-1506)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1572..1574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1572-1574)
  on lines 1576..1577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1576-1577)
  on lines 1581..1584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1581-1584)
  on lines 1586..1588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1586-1588)
  on lines 1590..1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1590-1591)
  on lines 1595..1598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1595-1598)
  on lines 1600..1602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1600-1602)
  on lines 1604..1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1604-1605)
  on lines 1609..1610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1609-1610)
  on line 1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1614-1614)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1459 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1459-1459)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2603..2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2603-2604)
  on line 2610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2610-2610)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2414..2415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2414-2415)
  on line 2421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2421-2421)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2677..2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2677-2678)
  on line 2684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2684-2684)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2451..2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2451-2452)
  on line 2458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2458-2458)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:397-397)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:406-406)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2566..2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2566-2567)
  on line 2573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2573-2573)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 423..424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:423-424)
  on line 431 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:431-431)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2316-2316)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2296-2296)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2640..2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2640-2641)
  on line 2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2647-2647)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:388-388)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1343..1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1343-1344)
  on lines 1351..1353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1351-1353)
  on lines 1355..1356 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1355-1356)
  on lines 1358..1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1358-1359)
  on lines 1366..1368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1366-1368)
  on lines 1370..1371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1370-1371)
  on lines 1373..1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1373-1374)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1206..1207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1206-1207)
  on lines 1209..1210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1209-1210)
  on lines 1217..1219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1217-1219)
  on lines 1221..1222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1221-1222)
  on lines 1224..1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1224-1225)
  on lines 1232..1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1232-1234)
  on lines 1236..1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1236-1237)
  on lines 1239..1240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1239-1240)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1013..1014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1013-1014)
  on lines 1016..1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1016-1017)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1420-1420)
  on lines 1425..1426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1425-1426)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1786..1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1786-1787)
  on lines 1797..1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1797-1798)
  on lines 1808..1809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1808-1809)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1625..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1625-1626)
  on lines 1636..1637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1636-1637)
  on lines 1647..1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1647-1648)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2621-2621)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2432-2432)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2584-2584)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2732 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2732-2732)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2658-2658)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2695-2695)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2469-2469)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 103 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:103-103)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 617
  dead: 608 (426 in uncalled functions)
  total lines: 1225
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:608:10-608:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1519:11-1519:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2565:9-2565:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1567:7-1567:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2583:9-2583:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1568:9-1568:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1336:7-1336:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2602:9-2602:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1340:11-1340:21)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2059:7-2059:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1783:9-1783:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2620:9-2620:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1794:11-1794:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2639:9-2639:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1804:11-1804:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1805:13-1805:23)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:422:9-422:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2657:9-2657:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2413:9-2413:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1622:9-1622:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2676:9-2676:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1633:11-1633:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2431:9-2431:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1202:7-1202:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1203:9-1203:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1010:7-1010:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1419:7-1419:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1643:11-1643:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1644:13-1644:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1422:9-1422:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2694:9-2694:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2450:9-2450:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1674:7-1674:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1675:9-1675:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2468:9-2468:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:2731:9-2731:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1267:7-1267:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1907:11-1907:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1472:11-1472:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1272:11-1272:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product32.cil.c:1497:11-1497: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
