./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_spec1_product30.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_spec1_product30.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_product30.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_product30.cil.c:618:3-639:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:675:3-700:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:760:5-780: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 'printMail__wrappee__Keys' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:75:1-102:1)
[Warning][Deadcode] Function 'printMail__wrappee__AutoResponder' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.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_spec1_product30.cil.c:122:1-140:1)
[Warning][Deadcode] Function 'printMail' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:141:1-154:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:184:1-192:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:363:1-373:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:452:1-463:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:464:1-475:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:547:1-592:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:593:1-648:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:649:1-708:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:711:1-813:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:814:1-859:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:860:1-905:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:928:1-942:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:946:1-971:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:972:1-991:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:996:1-1019:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1020:1-1039:1)
[Warning][Deadcode] Function 'getClientAddressBookSize' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1043:1-1066:1)
[Warning][Deadcode] Function 'setClientAddressBookSize' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1067:1-1086:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1087:1-1111:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1121:1-1189:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1190:1-1258:1)
[Warning][Deadcode] Function 'setClientAddressBookAlias' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1259:1-1314:1)
[Warning][Deadcode] Function 'getClientAddressBookAddress' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1324:1-1392:1)
[Warning][Deadcode] Function 'setClientAddressBookAddress' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1393:1-1448:1)
[Warning][Deadcode] Function 'getClientForwardReceiver' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1887:1-1910:1)
[Warning][Deadcode] Function 'setClientForwardReceiver' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1911:1-1930:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2153:1-2167:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2345:1-2359:1)
[Warning][Deadcode] Function 'getEmailId' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2362:1-2380:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2381:1-2396:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2473:1-2493:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2494:1-2509:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2512:1-2532:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2533:1-2548:1)
[Warning][Deadcode] Function 'isVerified' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2699:1-2717:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2745:1-2754:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2996:1-3010:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2740-2740)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1612-1612)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:205-205)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on lines 1818..1820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1818-1820)
  on lines 1822..1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1822-1824)
  on lines 1826..1827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1826-1827)
  on line 1836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1836-1836)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on lines 1465..1466 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1465-1466)
  on line 1473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1473-1473)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on lines 1947..1948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1947-1948)
  on line 1955 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1955-1955)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1740..1742 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1740-1742)
  on lines 1744..1745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1744-1745)
  on lines 1749..1752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1749-1752)
  on lines 1754..1756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1754-1756)
  on lines 1758..1759 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1758-1759)
  on lines 1763..1766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1763-1766)
  on lines 1768..1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1768-1770)
  on lines 1772..1773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1772-1773)
  on lines 1777..1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1777-1778)
  on line 1782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1782-1782)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1562..1563 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1562-1563)
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1567-1567)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1633..1635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1633-1635)
  on lines 1637..1638 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1637-1638)
  on lines 1642..1645 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1642-1645)
  on lines 1647..1649 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1647-1649)
  on lines 1651..1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1651-1652)
  on lines 1656..1659 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1656-1659)
  on lines 1661..1663 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1661-1663)
  on lines 1665..1666 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1665-1666)
  on lines 1670..1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1670-1671)
  on line 1675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1675-1675)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on lines 1512..1513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1512-1513)
  on line 1520 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1520-1520)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2597..2598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2597-2598)
  on line 2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2604-2604)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2408..2409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2408-2409)
  on line 2415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2415-2415)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2671..2672 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2671-2672)
  on line 2678 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2678-2678)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2445..2446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2445-2446)
  on line 2452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2452-2452)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2206-2206)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2215 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2215-2215)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2560..2561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2560-2561)
  on line 2567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2567-2567)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2232..2233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2232-2233)
  on line 2240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2240-2240)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 181 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.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_spec1_product30.cil.c:161-161)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2634..2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2634-2635)
  on line 2641 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2641-2641)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2197 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2197-2197)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1481-1481)
  on lines 1486..1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1486-1487)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1847..1848 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1847-1848)
  on lines 1858..1859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1858-1859)
  on lines 1869..1870 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1869-1870)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1686..1687 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1686-1687)
  on lines 1697..1698 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1697-1698)
  on lines 1708..1709 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1708-1709)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2615-2615)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2426 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2426-2426)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2578-2578)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2726 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2726-2726)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2652-2652)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2689 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2689-2689)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2463-2463)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2775-2775)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 525
  dead: 653 (528 in uncalled functions)
  total lines: 1178
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1558:11-1558:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2577:9-2577:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2596:9-2596:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1580:11-1580:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2614:9-2614:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2633:9-2633:20)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1817:11-1817:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1628:7-1628:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1629:9-1629:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2651:9-2651:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2407:9-2407:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1844:9-1844:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2670:9-2670:20)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:407:7-407:10)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2425:9-2425:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1855:11-1855:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2688:9-2688:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2444:9-2444:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1865:11-1865:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1866:13-1866:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2462:9-2462:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1683:9-1683:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1464:11-1464:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2725:9-2725:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1694:11-1694:21)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1480:7-1480:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1704:11-1704:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1705:13-1705:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1483:9-1483:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2231:9-2231:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1735:7-1735:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1736:9-1736:19)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1946:11-1946:22)
[Warning][Deadcode][CWE-570] condition 'handle == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1511:11-1511:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2818:10-2818:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1968:11-1968:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:1533:11-1533:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec1_product30.cil.c:2559:9-2559: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
