./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_spec9_product20.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_spec9_product20.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_spec9_product20.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_spec9_product20.cil.c:1606:3-1627:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1663:3-1688:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1748:5-1768: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_spec9_product20.cil.c:64:1-73:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:225:1-235:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:314:1-325:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:326:1-337:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:478:1-492:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:496:1-521:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:522:1-541:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:546:1-569:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:570:1-589:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:637:1-661:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:671:1-739:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:740:1-808:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1437:1-1460:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1461:1-1480:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1535:1-1580:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1581:1-1636:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1637:1-1696:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1699:1-1801:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1802:1-1847:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1848:1-1893:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1905:1-1932:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1933:1-1951:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1952:1-1960:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1961:1-1980:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1981:1-1989:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2192:1-2206:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2328:1-2342:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2345:1-2363:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2364:1-2379:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2456:1-2476:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2477:1-2492:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2495:1-2515:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2516:1-2531:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2608:1-2626:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2627:1-2642:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2645:1-2663:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2664:1-2679:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2682:1-2700:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2701:1-2716:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2947:1-2961:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2942-2942)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1162 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1162-1162)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2002-2002)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1386 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1386-1386)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 887..889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:887-889)
  on lines 891..892 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:891-892)
  on lines 897..900 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:897-900)
  on lines 902..904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:902-904)
  on lines 906..908 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:906-908)
  on lines 910..911 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:910-911)
  on lines 916..919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:916-919)
  on lines 921..923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:921-923)
  on lines 925..927 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:925-927)
  on lines 929..930 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:929-930)
  on lines 935..936 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:935-936)
  on line 940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:940-940)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:614-614)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1023-1023)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1505-1505)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1290..1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1290-1292)
  on lines 1294..1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1294-1295)
  on lines 1299..1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1299-1302)
  on lines 1304..1306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1304-1306)
  on lines 1308..1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1308-1309)
  on lines 1313..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1313-1316)
  on lines 1318..1320 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1318-1320)
  on lines 1322..1323 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1322-1323)
  on lines 1327..1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1327-1328)
  on line 1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1332-1332)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1112..1113 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1112-1113)
  on line 1117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1117-1117)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1183..1185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1183-1185)
  on lines 1187..1188 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1187-1188)
  on lines 1192..1195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1192-1195)
  on lines 1197..1199 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1197-1199)
  on lines 1201..1202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1201-1202)
  on lines 1206..1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1206-1209)
  on lines 1211..1213 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1211-1213)
  on lines 1215..1216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1215-1216)
  on lines 1220..1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1220-1221)
  on line 1225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1225-1225)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1070-1070)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2580..2581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2580-2581)
  on line 2587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2587-2587)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2391..2392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2391-2392)
  on line 2398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2398-2398)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2428..2429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2428-2429)
  on line 2435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2435-2435)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2245 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2245-2245)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2254-2254)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2543..2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2543-2544)
  on line 2550 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2550-2550)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2271..2272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2271-2272)
  on line 2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2279-2279)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2236-2236)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 954..955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:954-955)
  on lines 962..964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:962-964)
  on lines 966..967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:966-967)
  on lines 969..970 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:969-970)
  on lines 977..979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:977-979)
  on lines 981..982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:981-982)
  on lines 984..985 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:984-985)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 817..818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:817-818)
  on lines 820..821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:820-821)
  on lines 828..830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:828-830)
  on lines 832..833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:832-833)
  on lines 835..836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:835-836)
  on lines 843..845 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:843-845)
  on lines 847..848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:847-848)
  on lines 850..851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:850-851)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 624..625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:624-625)
  on lines 627..628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:627-628)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1031-1031)
  on lines 1036..1037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1036-1037)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1397..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1397-1398)
  on lines 1408..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1408-1409)
  on lines 1419..1420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1419-1420)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1236..1237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1236-1237)
  on lines 1247..1248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1247-1248)
  on lines 1258..1259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1258-1259)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2598-2598)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2409-2409)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2561-2561)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2446-2446)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 94 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:94-94)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 539
  dead: 627 (456 in uncalled functions)
  total lines: 1166
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2560:9-2560:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1233:9-1233:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2579:9-2579:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1244:11-1244:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:813:7-813:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:814:9-814:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:621:7-621:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1030:7-1030:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2597:9-2597:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1254:11-1254:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1255:13-1255:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1033:9-1033:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1285:7-1285:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1286:9-1286:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2390:9-2390:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:878:7-878:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2408:9-2408:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1518:11-1518:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1083:11-1083:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:883:11-883:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2427:9-2427:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1108:11-1108:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2445:9-2445:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1130:11-1130:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1178:7-1178:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1179:9-1179:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2757:10-2757:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:947:7-947:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:951:11-951:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1394:9-1394:19)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2270:9-2270:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1405:11-1405:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:2542:9-2542:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:269:7-269:10)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1415:11-1415:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec9_product20.cil.c:1416:13-1416:23)
[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
