./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_spec27_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_spec27_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_spec27_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_spec27_productSimulator.cil.c:126:3-147:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:183:3-208:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:268:5-288: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.292
[Info] vars: 42221, evals: 34565

[Info] |called|=0

Memory statistics: total=19811.03MB, max=251.12MB, minor=19802.47MB, major=340.78MB, promoted=332.23MB
    minor collections=9450  major collections=16 compactions=0

[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:55:1-100:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:101:1-156:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:157:1-216:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:219:1-321:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:322:1-367:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:368:1-413:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:426:1-440:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:591:1-605:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:609:1-634:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:635:1-654:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:659:1-682:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:683:1-702:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:750:1-774:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:784:1-852:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:853:1-921:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1973:1-1987:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2009:1-2024:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2101:1-2121:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2122:1-2137:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2140:1-2160:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2161:1-2176:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2719:1-2733:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3071:1-3081:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3160:1-3171:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3172:1-3183:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3451:1-3459:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:420-420)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 1275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1275-1275)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 3472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3472-3472)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 1499 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1499-1499)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 1000..1002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1000-1002)
  on lines 1004..1005 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1004-1005)
  on lines 1010..1013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1010-1013)
  on lines 1015..1017 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1015-1017)
  on lines 1019..1021 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1019-1021)
  on lines 1023..1024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1023-1024)
  on lines 1029..1032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1029-1032)
  on lines 1034..1036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1034-1036)
  on lines 1038..1040 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1038-1040)
  on lines 1042..1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1042-1043)
  on lines 1048..1049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1048-1049)
  on line 1053 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1053-1053)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 727 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:727-727)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 1136 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1136-1136)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 1571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1571-1571)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 1618 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1618-1618)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 1403..1405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1403-1405)
  on lines 1407..1408 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1407-1408)
  on lines 1412..1415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1412-1415)
  on lines 1417..1419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1417-1419)
  on lines 1421..1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1421-1422)
  on lines 1426..1429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1426-1429)
  on lines 1431..1433 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1431-1433)
  on lines 1435..1436 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1435-1436)
  on lines 1440..1441 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1440-1441)
  on line 1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1445-1445)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 1225..1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1225-1226)
  on line 1230 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1230-1230)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 1296..1298 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1296-1298)
  on lines 1300..1301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1300-1301)
  on lines 1305..1308 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1305-1308)
  on lines 1310..1312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1310-1312)
  on lines 1314..1315 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1314-1315)
  on lines 1319..1322 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1319-1322)
  on lines 1324..1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1324-1326)
  on lines 1328..1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1328-1329)
  on lines 1333..1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1333-1334)
  on line 1338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1338-1338)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 1183 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1183-1183)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 2225..2226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2225-2226)
  on line 2232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2232-2232)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 2036..2037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2036-2037)
  on line 2043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2043-2043)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1999..2000 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1999-2000)
  on line 2006 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2006-2006)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2299..2300 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2299-2300)
  on line 2306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2306-2306)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 2073..2074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2073-2074)
  on line 2080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2080-2080)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 2772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2772-2772)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2781-2781)
[Warning][Deadcode] Function 'incoming__before__Decrypt' has dead code:
  on line 2655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2655-2655)
  on line 2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2657-2657)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 2188..2189 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2188-2189)
  on line 2195 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2195-2195)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 2798..2799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2798-2799)
  on line 2806 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2806-2806)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 3448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3448-3448)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 3410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3410-3410)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 3430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3430-3430)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 2262..2263 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2262-2263)
  on line 2269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2269-2269)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2336..2337 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2336-2337)
  on line 2343 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2343-2343)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 2763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2763-2763)
[Warning][Deadcode] Function 'printMail' has dead code:
  on line 3398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3398-3398)
  on line 3400 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3400-3400)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:463-463)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 1067..1068 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1067-1068)
  on lines 1075..1077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1075-1077)
  on lines 1079..1080 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1079-1080)
  on lines 1082..1083 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1082-1083)
  on lines 1090..1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1090-1092)
  on lines 1094..1095 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1094-1095)
  on lines 1097..1098 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1097-1098)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 930..931 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:930-931)
  on lines 933..934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:933-934)
  on lines 941..943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:941-943)
  on lines 945..946 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:945-946)
  on lines 948..949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:948-949)
  on lines 956..958 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:956-958)
  on lines 960..961 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:960-961)
  on lines 963..964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:963-964)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 737..738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:737-738)
  on lines 740..741 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:740-741)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 1144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1144-1144)
  on lines 1149..1150 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1149-1150)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 1579 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1579-1579)
  on lines 1584..1585 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1584-1585)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 1510..1511 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1510-1511)
  on lines 1521..1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1521-1522)
  on lines 1532..1533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1532-1533)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 1349..1350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1349-1350)
  on lines 1360..1361 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1360-1361)
  on lines 1371..1372 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1371-1372)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 2243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2243-2243)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 2054 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2054-2054)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 2206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2206-2206)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2354-2354)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2280 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2280-2280)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2317-2317)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 2091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2091-2091)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 541 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:541-541)
  on line 558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:558-558)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 815
  dead: 550 (351 in uncalled functions)
  total lines: 1365
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1631:11-1631:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1196:11-1196:22)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Verify' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:3391:7-3391:32)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2187:9-2187:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1221:11-1221:22)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2797:9-2797:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2205:9-2205:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1692:10-1692:11)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2224:9-2224:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1243:11-1243:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2242:9-2242:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1291:7-1291:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1292:9-1292:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2261:9-2261:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2279:9-2279:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2298:9-2298:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2316:9-2316:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2335:9-2335:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1346:9-1346:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1357:11-1357:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2353:9-2353:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:926:7-926:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:927:9-927:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1367:11-1367:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1368:13-1368:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1398:7-1398:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1399:9-1399:19)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Verify' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:515:21-515:46)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Verify' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:517:23-517:50)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Sign' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:522:27-522:52)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:991:7-991:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:996:11-996:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1998:9-1998:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1060:7-1060:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1064:11-1064:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2035:9-2035:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1507:9-1507:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1518:11-1518:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2053:9-2053:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1528:11-1528:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1529:13-1529:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2072:9-2072:20)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Verify' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2648:7-2648:32)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:2090:9-2090:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1578:7-1578:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:734:7-734:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1143:7-1143:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1581:9-1581:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec27_productSimulator.cil.c:1146:9-1146: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)
