./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_spec1_product16.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_spec1_product16.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_spec1_product16.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_spec1_product16.cil.c:1694:3-1715:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1751:3-1776:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1836:5-1856: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
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:89:1-103:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:125:1-140:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:217:1-237:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:238:1-253:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:256:1-276:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:277:1-292:1)
[Warning][Deadcode] Function 'isSigned' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:369:1-387:1)
[Warning][Deadcode] Function 'setEmailIsSigned' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:388:1-403:1)
[Warning][Deadcode] Function 'getEmailSignKey' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:406:1-424:1)
[Warning][Deadcode] Function 'setEmailSignKey' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:425:1-440:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:443:1-461:1)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:462:1-477:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:494:1-503:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:557:1-571:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:575:1-600:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:601:1-620:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:625:1-648:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:649:1-668:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:672:1-695:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:696:1-715:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:716:1-740:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:750:1-818:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:819:1-887:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:888:1-943:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:953:1-1021:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1022:1-1077:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1081:1-1104:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1105:1-1124:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1623:1-1668:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1669:1-1724:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1725:1-1784:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1787:1-1889:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1890:1-1935:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1936:1-1981:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2340:1-2350:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2429:1-2440:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2441:1-2452:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2598:1-2606:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2771:1-2785:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 1613 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1613-1613)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1241 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1241-1241)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 2619 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2619-2619)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1424..1425 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1424-1425)
  on lines 1447..1449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1447-1449)
  on lines 1451..1453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1451-1453)
  on lines 1455..1456 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1455-1456)
  on line 1465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1465-1465)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on lines 1521..1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1521-1522)
  on line 1537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1537-1537)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1576..1577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1576-1577)
  on line 1584 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1584-1584)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1369..1371 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1369-1371)
  on lines 1373..1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1373-1374)
  on lines 1378..1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1378-1381)
  on lines 1383..1385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1383-1385)
  on lines 1387..1388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1387-1388)
  on lines 1392..1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1392-1395)
  on lines 1397..1399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1397-1399)
  on lines 1401..1402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1401-1402)
  on lines 1406..1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1406-1407)
  on line 1411 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1411-1411)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1191..1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1191-1192)
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1196-1196)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1262..1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1262-1264)
  on lines 1266..1267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1266-1267)
  on lines 1271..1274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1271-1274)
  on lines 1276..1278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1276-1278)
  on lines 1280..1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1280-1281)
  on lines 1285..1288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1285-1288)
  on lines 1290..1292 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1290-1292)
  on lines 1294..1295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1294-1295)
  on lines 1299..1300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1299-1300)
  on line 1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1304-1304)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1133..1134 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1133-1134)
  on line 1149 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1149-1149)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 341..342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:341-342)
  on line 348 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:348-348)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 152..153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:152-153)
  on line 159 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:159-159)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 115..116 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:115-116)
  on line 122 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:122-122)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 189..190 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:189-190)
  on line 196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:196-196)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2824-2824)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2833 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2833-2833)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 304..305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:304-305)
  on line 311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:311-311)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2850..2851 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2850-2851)
  on line 2858 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2858-2858)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 2595 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2595-2595)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 2575 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2575-2575)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2815-2815)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1545-1545)
  on lines 1550..1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1550-1551)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1476..1477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1476-1477)
  on lines 1487..1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1487-1488)
  on lines 1498..1499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1498-1499)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1315..1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1315-1316)
  on lines 1326..1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1326-1327)
  on lines 1337..1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1337-1338)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:359-359)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:170-170)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:322-322)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:207-207)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:524-524)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 492
  dead: 639 (518 in uncalled functions)
  total lines: 1131
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1597:11-1597:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1162:11-1162:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1187:11-1187:22)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1423:11-1423:48)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2849:9-2849:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1209:11-1209:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1446:11-1446:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:303:9-303:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1257:7-1257:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1258:9-1258:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:321:9-321:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2031:10-2031:11)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1473:9-1473:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:340:9-340:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1484:11-1484:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1494:11-1494:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:358:9-358:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1495:13-1495:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:114:9-114:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1520:7-1520:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1312:9-1312:19)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:2384:7-2384:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1323:11-1323:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:151:9-151:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1544:7-1544:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1333:11-1333:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1547:9-1547:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1334:13-1334:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:169:9-169:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1364:7-1364:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1365:9-1365:19)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1132:7-1132:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:188:9-188:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:1575:11-1575:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product16.cil.c:206:9-206: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)
