./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_spec0_product35.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_spec0_product35.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_spec0_product35.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_spec0_product35.cil.c:312:3-333:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:369:3-394:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:454:5-474: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 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:51:1-65:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:201:1-209:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:241:1-286:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:287:1-342:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:343:1-402:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:405:1-507:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:508:1-553:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:554:1-599:1)
[Warning][Deadcode] Function 'select_one' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:625:1-634:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:903:1-917:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1129:1-1143:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1147:1-1172:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1173:1-1192:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1197:1-1220:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1221:1-1240:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1288:1-1312:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1322:1-1390:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1391:1-1459:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2510:1-2520:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2599:1-2610:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2611:1-2622:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2718:1-2732:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2754:1-2769:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2846:1-2866:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2867:1-2882:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2885:1-2905:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2906:1-2921:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:231-231)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1813-1813)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:222-222)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2037-2037)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1538..1540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1538-1540)
  on lines 1542..1543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1542-1543)
  on lines 1548..1551 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1548-1551)
  on lines 1553..1555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1553-1555)
  on lines 1557..1559 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1557-1559)
  on lines 1561..1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1561-1562)
  on lines 1567..1570 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1567-1570)
  on lines 1572..1574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1572-1574)
  on lines 1576..1578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1576-1578)
  on lines 1580..1581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1580-1581)
  on lines 1586..1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1586-1587)
  on line 1591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1591-1591)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 1265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1265-1265)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1674 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1674-1674)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 2109 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2109-2109)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 2156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2156-2156)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1941..1943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1941-1943)
  on lines 1945..1946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1945-1946)
  on lines 1950..1953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1950-1953)
  on lines 1955..1957 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1955-1957)
  on lines 1959..1960 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1959-1960)
  on lines 1964..1967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1964-1967)
  on lines 1969..1971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1969-1971)
  on lines 1973..1974 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1973-1974)
  on lines 1978..1979 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1978-1979)
  on line 1983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1983-1983)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1763..1764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1763-1764)
  on line 1768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1768-1768)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1834..1836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1834-1836)
  on lines 1838..1839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1838-1839)
  on lines 1843..1846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1843-1846)
  on lines 1848..1850 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1848-1850)
  on lines 1852..1853 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1852-1853)
  on lines 1857..1860 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1857-1860)
  on lines 1862..1864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1862-1864)
  on lines 1866..1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1866-1867)
  on lines 1871..1872 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1871-1872)
  on line 1876 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1876-1876)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1721-1721)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2970..2971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2970-2971)
  on line 2977 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2977-2977)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2781..2782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2781-2782)
  on line 2788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2788-2788)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 2744..2745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2744-2745)
  on line 2751 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2751-2751)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 3044..3045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3044-3045)
  on line 3051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3051-3051)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2818..2819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2818-2819)
  on line 2825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2825-2825)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:956-956)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:965-965)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2933..2934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2933-2934)
  on line 2940 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2940-2940)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 982..983 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:982-983)
  on line 990 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:990-990)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:198-198)
[Warning][Deadcode] Function 'isReadable__wrappee__Keys' has dead code:
  on line 178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:178-178)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 3007..3008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3007-3008)
  on line 3014 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3014-3014)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 3081..3082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3081-3082)
  on line 3088 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3088-3088)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:947-947)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1605..1606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1605-1606)
  on lines 1613..1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1613-1615)
  on lines 1617..1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1617-1618)
  on lines 1620..1621 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1620-1621)
  on lines 1628..1630 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1628-1630)
  on lines 1632..1633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1632-1633)
  on lines 1635..1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1635-1636)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1468..1469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1468-1469)
  on lines 1471..1472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1471-1472)
  on lines 1479..1481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1479-1481)
  on lines 1483..1484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1483-1484)
  on lines 1486..1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1486-1487)
  on lines 1494..1496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1494-1496)
  on lines 1498..1499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1498-1499)
  on lines 1501..1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1501-1502)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 1275..1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1275-1276)
  on lines 1278..1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1278-1279)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1682-1682)
  on lines 1687..1688 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1687-1688)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2117-2117)
  on lines 2122..2123 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2122-2123)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2048..2049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2048-2049)
  on lines 2059..2060 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2059-2060)
  on lines 2070..2071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2070-2071)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1887..1888 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1887-1888)
  on lines 1898..1899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1898-1899)
  on lines 1909..1910 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1909-1910)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2988 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2988-2988)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2799-2799)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2951 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2951-2951)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 3099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3099-3099)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 3025 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3025-3025)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 3062 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3062-3062)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2836 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2836-2836)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:655-655)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 685
  dead: 547 (355 in uncalled functions)
  total lines: 1232
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1829:7-1829:18)
[Warning][Deadcode][CWE-571] condition 'tmp' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2554:7-2554:10)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1830:9-1830:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3098:9-3098:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1598:7-1598:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1602:11-1602:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2045:9-2045:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2056:11-2056:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2066:11-2066:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2067:13-2067:23)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1884:9-1884:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2932:9-2932:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:981:9-981:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1895:11-1895:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1464:7-1464:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2116:7-2116:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1465:9-1465:19)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1272:7-1272:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1681:7-1681:18)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1905:11-1905:22)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2119:9-2119:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1906:13-1906:23)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1684:9-1684:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2950:9-2950:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1936:7-1936:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1937:9-1937:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2969:9-2969:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2987:9-2987:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2743:9-2743:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1529:7-1529:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3006:9-3006:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2169:11-2169:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1734:11-1734:22)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1534:11-1534:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3024:9-3024:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2780:9-2780:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1759:11-1759:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3043:9-3043:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2230:10-2230:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2798:9-2798:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:1781:11-1781:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3061:9-3061:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2817:9-2817:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:3080:9-3080:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_product35.cil.c:2835:9-2835: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
