./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_spec0_productSimulator.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_spec0_productSimulator.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_productSimulator.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_productSimulator.cil.c:3175:3-3196:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3232:3-3257:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3317:5-3337: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

[Info] runtime: 00:00:10.315
[Info] vars: 41132, evals: 32901

[Info] |called|=0

Memory statistics: total=19782.81MB, max=281.26MB, minor=19774.70MB, major=341.53MB, promoted=333.42MB
    minor collections=9436  major collections=15 compactions=0

[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:545:1-559:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:753:1-767:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:798:1-812:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:816:1-841:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:842:1-861:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:866:1-889:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:890:1-909:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:957:1-981:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:991:1-1059:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1060:1-1128:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1858:1-1872:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1894:1-1909:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1986:1-2006:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2007:1-2022:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2025:1-2045:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2046:1-2061:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2408:1-2418:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2497:1-2508:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2509:1-2520:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3073:1-3081:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3104:1-3149:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3150:1-3205:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3206:1-3265:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3268:1-3370:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3371:1-3416:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3417:1-3462:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:774-774)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1482-1482)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3094-3094)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1706-1706)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1207..1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1207-1209)
  on lines 1211..1212 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1211-1212)
  on lines 1217..1220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1217-1220)
  on lines 1222..1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1222-1224)
  on lines 1226..1228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1226-1228)
  on lines 1230..1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1230-1231)
  on lines 1236..1239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1236-1239)
  on lines 1241..1243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1241-1243)
  on lines 1245..1247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1245-1247)
  on lines 1249..1250 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1249-1250)
  on lines 1255..1256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1255-1256)
  on line 1260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1260-1260)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:934-934)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1343-1343)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1778-1778)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1825 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1825-1825)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1610..1612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1610-1612)
  on lines 1614..1615 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1614-1615)
  on lines 1619..1622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1619-1622)
  on lines 1624..1626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1624-1626)
  on lines 1628..1629 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1628-1629)
  on lines 1633..1636 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1633-1636)
  on lines 1638..1640 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1638-1640)
  on lines 1642..1643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1642-1643)
  on lines 1647..1648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1647-1648)
  on line 1652 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1652-1652)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1432..1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1432-1433)
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1437-1437)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1503..1505 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1503-1505)
  on lines 1507..1508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1507-1508)
  on lines 1512..1515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1512-1515)
  on lines 1517..1519 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1517-1519)
  on lines 1521..1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1521-1522)
  on lines 1526..1529 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1526-1529)
  on lines 1531..1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1531-1533)
  on lines 1535..1536 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1535-1536)
  on lines 1540..1541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1540-1541)
  on line 1545 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1545-1545)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1390-1390)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2110..2111 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2110-2111)
  on line 2117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2117-2117)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1921..1922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1921-1922)
  on line 1928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1928-1928)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1884..1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1884-1885)
  on line 1891 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1891-1891)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2184..2185 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2184-2185)
  on line 2191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2191-2191)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1958..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1958-1959)
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1965-1965)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:598-598)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:607-607)
[Warning][Deadcode] Function 'incoming__before__Verify' has dead code:
  on line 453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:453-453)
  on line 455 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:455-455)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2073..2074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2073-2074)
  on line 2080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2080-2080)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 624..625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:624-625)
  on line 632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:632-632)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 3070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3070-3070)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 3032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3032-3032)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 3052 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:3052-3052)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2147..2148 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2147-2148)
  on line 2154 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2154-2154)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2221..2222 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2221-2222)
  on line 2228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2228-2228)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:589-589)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 70 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:70-70)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1274..1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1274-1275)
  on lines 1282..1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1282-1284)
  on lines 1286..1287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1286-1287)
  on lines 1289..1290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1289-1290)
  on lines 1297..1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1297-1299)
  on lines 1301..1302 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1301-1302)
  on lines 1304..1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1304-1305)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 1137..1138 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1137-1138)
  on lines 1140..1141 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1140-1141)
  on lines 1148..1150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1148-1150)
  on lines 1152..1153 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1152-1153)
  on lines 1155..1156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1155-1156)
  on lines 1163..1165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1163-1165)
  on lines 1167..1168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1167-1168)
  on lines 1170..1171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1170-1171)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 944..945 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:944-945)
  on lines 947..948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:947-948)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1351 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1351-1351)
  on lines 1356..1357 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1356-1357)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1786-1786)
  on lines 1791..1792 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1791-1792)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1717..1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1717-1718)
  on lines 1728..1729 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1728-1729)
  on lines 1739..1740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1739-1740)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1556..1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1556-1557)
  on lines 1567..1568 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1567-1568)
  on lines 1578..1579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1578-1579)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2128-2128)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1939-1939)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2091-2091)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2239-2239)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2165-2165)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2202 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2202-2202)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1976-1976)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:165-165)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 813
  dead: 547 (351 in uncalled functions)
  total lines: 1360
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1957:9-1957:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1975:9-1975:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:623:9-623:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1553:9-1553:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1564:11-1564:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1133:7-1133:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1134:9-1134:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1574:11-1574:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1575:13-1575:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2648:10-2648:11)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1605:7-1605:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1606:9-1606:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2072:9-2072:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2090:9-2090:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1198:7-1198:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1203:11-1203:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2109:9-2109:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2127:9-2127:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2146:9-2146:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Forward' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2751:23-2751:49)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2164:9-2164:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2183:9-2183:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1267:7-1267:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2201:9-2201:20)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1271:11-1271:21)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1714:9-1714:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2220:9-2220:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1725:11-1725:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1735:11-1735:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:2238:9-2238:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1736:13-1736:23)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1785:7-1785:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:941:7-941:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1350:7-1350:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1788:9-1788:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1353:9-1353:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1838:11-1838:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1403:11-1403:22)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Forward' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:446:7-446:33)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1428:11-1428:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1883:9-1883:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1450:11-1450:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1920:9-1920:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1498:7-1498:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1499:9-1499:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec0_productSimulator.cil.c:1938:9-1938: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)
