./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_spec8_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_spec8_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_spec8_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_spec8_product20.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:268:5-288: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 '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:417:1-431:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:455:1-469:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:472:1-490:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:491:1-506:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:583:1-603:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:604:1-619:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:622:1-642:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:643:1-658:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:735:1-753:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:754:1-769:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:772:1-790:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:791:1-806:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:809:1-827:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:828:1-843:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:883:1-897:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:901:1-926:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:927:1-946:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:951:1-974:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:975:1-994:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1042:1-1066:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1076:1-1144:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1145:1-1213:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1842:1-1865:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1866:1-1885:1)
[Warning][Deadcode] Function 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2221:1-2248:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2249:1-2267:1)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2268:1-2276:1)
[Warning][Deadcode] Function 'isReadable' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2277:1-2296:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2297:1-2305:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2428:1-2438:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2517:1-2528:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2529:1-2540:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2803:1-2817:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2927:1-2936:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:850-850)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1567-1567)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2318 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2318-2318)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1791-1791)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1292..1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1292-1294)
  on lines 1296..1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1296-1297)
  on lines 1302..1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1302-1305)
  on lines 1307..1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1307-1309)
  on lines 1311..1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1311-1313)
  on lines 1315..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1315-1316)
  on lines 1321..1324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1321-1324)
  on lines 1326..1328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1326-1328)
  on lines 1330..1332 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1330-1332)
  on lines 1334..1335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1334-1335)
  on lines 1340..1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1340-1341)
  on line 1345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1345-1345)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1019 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1019-1019)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1428-1428)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1910-1910)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1695..1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1695-1697)
  on lines 1699..1700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1699-1700)
  on lines 1704..1707 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1704-1707)
  on lines 1709..1711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1709-1711)
  on lines 1713..1714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1713-1714)
  on lines 1718..1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1718-1721)
  on lines 1723..1725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1723-1725)
  on lines 1727..1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1727-1728)
  on lines 1732..1733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1732-1733)
  on line 1737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1737-1737)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1517..1518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1517-1518)
  on line 1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1522-1522)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1588..1590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1588-1590)
  on lines 1592..1593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1592-1593)
  on lines 1597..1600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1597-1600)
  on lines 1602..1604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1602-1604)
  on lines 1606..1607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1606-1607)
  on lines 1611..1614 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1611-1614)
  on lines 1616..1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1616-1618)
  on lines 1620..1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1620-1621)
  on lines 1625..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1625-1626)
  on line 1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1630-1630)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1475-1475)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 707..708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:707-708)
  on line 714 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:714-714)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 518..519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:518-519)
  on line 525 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:525-525)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 555..556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:555-556)
  on line 562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:562-562)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2856 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2856-2856)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2865-2865)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 670..671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:670-671)
  on line 677 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:677-677)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2882..2883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2882-2883)
  on line 2890 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2890-2890)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2847 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2847-2847)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1359..1360 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1359-1360)
  on lines 1367..1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1367-1369)
  on lines 1371..1372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1371-1372)
  on lines 1374..1375 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1374-1375)
  on lines 1382..1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1382-1384)
  on lines 1386..1387 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1386-1387)
  on lines 1389..1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1389-1390)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1222..1223 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1222-1223)
  on lines 1225..1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1225-1226)
  on lines 1233..1235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1233-1235)
  on lines 1237..1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1237-1238)
  on lines 1240..1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1240-1241)
  on lines 1248..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1248-1250)
  on lines 1252..1253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1252-1253)
  on lines 1255..1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1255-1256)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1029..1030 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1029-1030)
  on lines 1032..1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1032-1033)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1436-1436)
  on lines 1441..1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1441-1442)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1802..1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1802-1803)
  on lines 1813..1814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1813-1814)
  on lines 1824..1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1824-1825)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1641..1642 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1641-1642)
  on lines 1652..1653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1652-1653)
  on lines 1663..1664 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1663-1664)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 725 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:725-725)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:536-536)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:688-688)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:573-573)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2957-2957)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 539
  dead: 627 (456 in uncalled functions)
  total lines: 1166
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1690:7-1690:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1691:9-1691:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2472:7-2472:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:535:9-535:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:554:9-554:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1283:7-1283:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1923:11-1923:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1488:11-1488:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:572:9-572:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1288:11-1288:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1513:11-1513:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2881:9-2881:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1535:11-1535:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:2037:10-2037:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1583:7-1583:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1584:9-1584:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1352:7-1352:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:669:9-669:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1356:11-1356:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1799:9-1799:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:687:9-687:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1810:11-1810:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:706:9-706:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1820:11-1820:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1821:13-1821:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:724:9-724:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1638:9-1638:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1649:11-1649:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1218:7-1218:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1219:9-1219:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1026:7-1026:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1435:7-1435:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1659:11-1659:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1660:13-1660:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:1438:9-1438:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec8_product20.cil.c:517:9-517:20)
[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
