./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/email_spec6_productSimulator.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/email_spec6_productSimulator.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_spec6_productSimulator.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_spec6_productSimulator.cil.c:189:3-210:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:246:3-271:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:331:5-351: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] couldn't parse entry: find uuid

[Info] runtime: 00:00:10.277
[Info] vars: 27569, evals: 22105

[Info] |called|=0

Memory statistics: total=20769.04MB, max=251.12MB, minor=20763.12MB, major=321.21MB, promoted=315.29MB
    minor collections=9908  major collections=16 compactions=0

[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:118:1-163:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:164:1-219:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:220:1-279:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:282:1-384:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:385:1-430:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:431:1-476:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:668:1-676:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:840:1-854:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:858:1-883:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:884:1-903:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:908:1-931:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:932:1-951:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:999:1-1023:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1033:1-1101:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1102:1-1170:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1892:1-1906:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2339:1-2349:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2428:1-2439:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2440:1-2451:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2552:1-2566:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2588:1-2603:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2680:1-2700:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2701:1-2716:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2719:1-2739:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2740:1-2755:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:3293:1-3307:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:698-698)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1524-1524)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:689-689)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1748-1748)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1249..1251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1249-1251)
  on lines 1253..1254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1253-1254)
  on lines 1259..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1259-1262)
  on lines 1264..1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1264-1266)
  on lines 1268..1270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1268-1270)
  on lines 1272..1273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1272-1273)
  on lines 1278..1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1278-1281)
  on lines 1283..1285 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1283-1285)
  on lines 1287..1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1287-1289)
  on lines 1291..1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1291-1292)
  on lines 1297..1298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1297-1298)
  on line 1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1302-1302)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:976-976)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1385-1385)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1820-1820)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1867-1867)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1652..1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1652-1654)
  on lines 1656..1657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1656-1657)
  on lines 1661..1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1661-1664)
  on lines 1666..1668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1666-1668)
  on lines 1670..1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1670-1671)
  on lines 1675..1678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1675-1678)
  on lines 1680..1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1680-1682)
  on lines 1684..1685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1684-1685)
  on lines 1689..1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1689-1690)
  on line 1694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1694-1694)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1474..1475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1474-1475)
  on line 1479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1479-1479)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1545..1547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1545-1547)
  on lines 1549..1550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1549-1550)
  on lines 1554..1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1554-1557)
  on lines 1559..1561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1559-1561)
  on lines 1563..1564 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1563-1564)
  on lines 1568..1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1568-1571)
  on lines 1573..1575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1573-1575)
  on lines 1577..1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1577-1578)
  on lines 1582..1583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1582-1583)
  on line 1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1587-1587)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1432-1432)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2804..2805 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2804-2805)
  on line 2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2811-2811)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2615..2616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2615-2616)
  on line 2622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2622-2622)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2578..2579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2578-2579)
  on line 2585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2585-2585)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2878..2879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2878-2879)
  on line 2885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2885-2885)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2652..2653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2652-2653)
  on line 2659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2659-2659)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 3346 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:3346-3346)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 3355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:3355-3355)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2767..2768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2767-2768)
  on line 2774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2774-2774)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on line 3380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:3380-3380)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 661 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:661-661)
  on line 663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:663-663)
  on line 665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:665-665)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:627-627)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:647-647)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2841..2842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2841-2842)
  on line 2848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2848-2848)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2915..2916 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2915-2916)
  on line 2922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2922-2922)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 3337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:3337-3337)
[Warning][Deadcode] Function 'outgoing__before__AddressBook' has dead code:
  on line 3020 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:3020-3020)
  on line 3022 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:3022-3022)
[Warning][Deadcode] Function 'printMail__before__Sign' has dead code:
  on line 548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:548-548)
  on line 550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:550-550)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:713-713)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1316..1317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1316-1317)
  on lines 1324..1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1324-1326)
  on lines 1328..1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1328-1329)
  on lines 1331..1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1331-1332)
  on lines 1339..1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1339-1341)
  on lines 1343..1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1343-1344)
  on lines 1346..1347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1346-1347)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1179..1180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1179-1180)
  on lines 1182..1183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1182-1183)
  on lines 1190..1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1190-1192)
  on lines 1194..1195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1194-1195)
  on lines 1197..1198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1197-1198)
  on lines 1205..1207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1205-1207)
  on lines 1209..1210 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1209-1210)
  on lines 1212..1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1212-1213)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 986..987 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:986-987)
  on lines 989..990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:989-990)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1393 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1393-1393)
  on lines 1398..1399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1398-1399)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1828-1828)
  on lines 1833..1834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1833-1834)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1759..1760 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1759-1760)
  on lines 1770..1771 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1770-1771)
  on lines 1781..1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1781-1782)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1598..1599 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1598-1599)
  on lines 1609..1610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1609-1610)
  on lines 1620..1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1620-1621)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2822 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2822-2822)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2633-2633)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2785 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2785-2785)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2933-2933)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2859-2859)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2896-2896)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2670-2670)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:783-783)
  on line 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:799-799)
  on line 808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:808-808)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 823
  dead: 551 (351 in uncalled functions)
  total lines: 1374
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2784:9-2784:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2803:9-2803:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2821:9-2821:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2840:9-2840:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1309:7-1309:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1313:11-1313:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1756:9-1756:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2858:9-2858:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1767:11-1767:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2877:9-2877:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1777:11-1777:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1778:13-1778:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2895:9-2895:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2914:9-2914:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1827:7-1827:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:983:7-983:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1392:7-1392:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2932:9-2932:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1830:9-1830:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1395:9-1395:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:3013:7-3013:33)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1880:11-1880:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1445:11-1445:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1470:11-1470:22)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:541:7-541:33)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1958:10-1958:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1492:11-1492:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2577:9-2577:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1540:7-1540:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1541:9-1541:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2614:9-2614:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:654:7-654:33)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2632:9-2632:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2651:9-2651:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1595:9-1595:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2669:9-2669:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1606:11-1606:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1175:7-1175:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1176:9-1176:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1616:11-1616:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1617:13-1617:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1647:7-1647:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1648:9-1648:19)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Encrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:747:7-747:35)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Decrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:752:11-752:39)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Encrypt' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:755:13-755:39)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Encrypt' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:757:15-757:43)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Keys' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:775:29-775:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1240:7-1240:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:1245:11-1245:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec6_productSimulator.cil.c:2766:9-2766:20)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
