./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_spec3_product28.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_spec3_product28.cil.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:357:3-378:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:414:3-439:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:499:5-519: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 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:75:1-102:1)
[Warning][Deadcode] Function 'printMail__wrappee__Encrypt' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:103:1-121:1)
[Warning][Deadcode] Function 'printMail__wrappee__Sign' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:122:1-140:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:141:1-154:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:184:1-192:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:286:1-331:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:332:1-387:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:388:1-447:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:450:1-552:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:553:1-598:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:599:1-644:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:674:1-688:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:692:1-717:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:718:1-737:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:742:1-765:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:766:1-785:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:789:1-812:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:813:1-832:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:833:1-857:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:867:1-935:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:936:1-1004:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1005:1-1060:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1070:1-1138:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1139:1-1194:1)
[Warning][Deadcode] Function 'getClientAutoResponse' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1198:1-1221:1)
[Warning][Deadcode] Function 'setClientAutoResponse' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1222:1-1241:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1633:1-1656:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1657:1-1676:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1840:1-1850:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1929:1-1940:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1941:1-1952:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2020:1-2034:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2037:1-2055:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2056:1-2071:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2148:1-2168:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2169:1-2184:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2187:1-2207:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2208:1-2223:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2374:1-2392:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2624:1-2638:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2641:1-2650:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2822:1-2836:1)
[Warning][Deadcode] Function 'queue' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2850:1-2859:1)
[Warning][Deadcode] Function 'get_queued_client' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2869:1-2877:1)
[Warning][Deadcode] Function 'get_queued_email' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2878:1-2886:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:276-276)
[Warning][Deadcode] Function 'bobToRjh' has dead code:
  on lines 1832..1834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1832-1834)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1358-1358)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:205-205)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1541..1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1541-1542)
  on lines 1555..1556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1555-1556)
  on lines 1563..1566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1563-1566)
  on lines 1568..1570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1568-1570)
  on lines 1572..1573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1572-1573)
  on lines 1577..1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1577-1578)
  on line 1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1582-1582)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1688..1690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1688-1690)
  on lines 1692..1694 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1692-1694)
  on lines 1696..1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1696-1697)
  on line 1701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1701-1701)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1486..1488 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1486-1488)
  on lines 1490..1491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1490-1491)
  on lines 1495..1498 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1495-1498)
  on lines 1500..1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1500-1502)
  on lines 1504..1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1504-1505)
  on lines 1509..1512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1509-1512)
  on lines 1514..1516 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1514-1516)
  on lines 1518..1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1518-1519)
  on lines 1523..1524 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1523-1524)
  on line 1528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1528-1528)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1308..1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1308-1309)
  on line 1313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1313-1313)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1379..1381 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1379-1381)
  on lines 1383..1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1383-1384)
  on lines 1388..1391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1388-1391)
  on lines 1393..1395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1393-1395)
  on lines 1397..1398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1397-1398)
  on lines 1402..1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1402-1405)
  on lines 1407..1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1407-1409)
  on lines 1411..1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1411-1412)
  on lines 1416..1417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1416-1417)
  on line 1421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1421-1421)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1257..1259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1257-1259)
  on lines 1261..1262 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1261-1262)
  on line 1266 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1266-1266)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2271..2273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2271-2273)
  on lines 2275..2276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2275-2276)
  on line 2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2279-2279)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2082..2084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2082-2084)
  on lines 2086..2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2086-2087)
  on line 2090 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2090-2090)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2345..2347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2345-2347)
  on lines 2349..2350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2349-2350)
  on line 2353 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2353-2353)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2119..2121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2119-2121)
  on lines 2123..2124 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2123-2124)
  on line 2127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2127-2127)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2234..2236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2234-2236)
  on lines 2238..2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2238-2239)
  on line 2242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2242-2242)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2901..2902 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2901-2902)
  on line 2909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2909-2909)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:181-181)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 161 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:161-161)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2308..2310 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2308-2310)
  on lines 2312..2313 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2312-2313)
  on line 2316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2316-2316)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2866 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2866-2866)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1593..1594 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1593-1594)
  on lines 1604..1605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1604-1605)
  on lines 1615..1616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1615-1616)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1432..1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1432-1433)
  on lines 1443..1444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1443-1444)
  on lines 1454..1455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1454-1455)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on lines 2289..2290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2289-2290)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on lines 2100..2101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2100-2101)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on lines 2252..2253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2252-2253)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on lines 2400..2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2400-2401)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on lines 2326..2327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2326-2327)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on lines 2363..2364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2363-2364)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on lines 2137..2138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2137-2138)
[Warning][Deadcode] Function 'sign' has dead code:
  on line 2932 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2932-2932)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2671-2671)
[Warning][Deadcode] Function 'verify' has dead code:
  on line 2968 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2968-2968)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 451
  dead: 720 (557 in uncalled functions)
  total lines: 1171
[Warning][Deadcode][CWE-571] condition 'sent_signed == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:241:7-241:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2249:7-2249:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1450:11-1450:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1451:13-1451:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2267:7-2267:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1684:7-1684:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1481:7-1481:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1482:9-1482:19)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1253:9-1253:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2286:7-2286:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2304:7-2304:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1714:11-1714:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1279:11-1279:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2323:7-2323:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2078:7-2078:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1304:11-1304:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2341:7-2341:18)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2900:9-2900:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2097:7-2097:18)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring0_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1540:11-1540:48)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2360:7-2360:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2115:7-2115:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1326:11-1326:22)
[Warning][Deadcode][CWE-571] condition 'tmp___1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1828:7-1828:14)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1549:9-1549:20)
[Warning][Deadcode][CWE-570] condition '! privkey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2931:7-2931:16)
[Warning][Deadcode][CWE-570] condition 'userid == __ste_Client_Keyring1_User1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1554:13-1554:50)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2134:7-2134:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1374:7-1374:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1375:9-1375:19)
[Warning][Deadcode][CWE-571] condition 'tmp___0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2965:9-2965:16)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2397:7-2397:18)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1884:7-1884:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1590:9-1590:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1601:11-1601:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2449:10-2449:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1611:11-1611:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1612:13-1612:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1429:9-1429:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:2230:7-2230:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_product28.cil.c:1440:11-1440:21)
[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)
