./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_spec11_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_spec11_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_spec11_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_spec11_productSimulator.cil.c:1204:3-1225:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1261:3-1286:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1346:5-1366: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.298
[Info] vars: 52404, evals: 41709

[Info] |called|=0

Memory statistics: total=20008.70MB, max=288.79MB, minor=20000.02MB, major=372.15MB, promoted=363.46MB
    minor collections=9544  major collections=16 compactions=0


[Info] runtime: 00:00:20.427
[Info] vars: 52404, evals: 41709

[Info] |called|=0

Memory statistics: total=40855.49MB, max=439.21MB, minor=40845.33MB, major=578.41MB, promoted=568.24MB
    minor collections=19485  major collections=17 compactions=0

[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:545:1-559:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:926:1-936:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1015:1-1026:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1027:1-1038:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1133:1-1178:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1179:1-1234:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1235:1-1294:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1297:1-1399:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1400:1-1445:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1446:1-1491:1)
[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1674:1-1682:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1706:1-1720:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1742:1-1757:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1834:1-1854:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1855:1-1870:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1873:1-1893:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1894:1-1909:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2097:1-2111:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2397:1-2411:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2415:1-2440:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2441:1-2460:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2465:1-2488:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2489:1-2508:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2556:1-2580:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2590:1-2658:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2659:1-2727:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 2384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2384-2384)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 3081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3081-3081)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 1695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1695-1695)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 3305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3305-3305)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2806..2808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2806-2808)
  on lines 2810..2811 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2810-2811)
  on lines 2816..2819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2816-2819)
  on lines 2821..2823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2821-2823)
  on lines 2825..2827 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2825-2827)
  on lines 2829..2830 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2829-2830)
  on lines 2835..2838 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2835-2838)
  on lines 2840..2842 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2840-2842)
  on lines 2844..2846 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2844-2846)
  on lines 2848..2849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2848-2849)
  on lines 2854..2855 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2854-2855)
  on line 2859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2859-2859)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 2533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2533-2533)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2942 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2942-2942)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 3377 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3377-3377)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 3424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3424-3424)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 3209..3211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3209-3211)
  on lines 3213..3214 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3213-3214)
  on lines 3218..3221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3218-3221)
  on lines 3223..3225 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3223-3225)
  on lines 3227..3228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3227-3228)
  on lines 3232..3235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3232-3235)
  on lines 3237..3239 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3237-3239)
  on lines 3241..3242 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3241-3242)
  on lines 3246..3247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3246-3247)
  on line 3251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3251-3251)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 3031..3032 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3031-3032)
  on line 3036 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3036-3036)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 3102..3104 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3102-3104)
  on lines 3106..3107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3106-3107)
  on lines 3111..3114 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3111-3114)
  on lines 3116..3118 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3116-3118)
  on lines 3120..3121 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3120-3121)
  on lines 3125..3128 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3125-3128)
  on lines 3130..3132 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3130-3132)
  on lines 3134..3135 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3134-3135)
  on lines 3139..3140 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3139-3140)
  on line 3144 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3144-3144)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2989 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2989-2989)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1958..1959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1958-1959)
  on line 1965 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1965-1965)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1769..1770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1769-1770)
  on line 1776 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1776-1776)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1732..1733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1732-1733)
  on line 1739 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1739-1739)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 2032..2033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2032-2033)
  on line 2039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2039-2039)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1806..1807 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1806-1807)
  on line 1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1813-1813)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_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_spec11_productSimulator.cil.c:607-607)
[Warning][Deadcode] Function 'incoming__before__Forward' has dead code:
  on line 415 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:415-415)
  on line 417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:417-417)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1921..1922 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1921-1922)
  on line 1928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1928-1928)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 624..625 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:624-625)
  on line 632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:632-632)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1671-1671)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 1633 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1633-1633)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 1653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1653-1653)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1995..1996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1995-1996)
  on line 2002 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2002-2002)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 2069..2070 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2069-2070)
  on line 2076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2076-2076)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 589 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_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_spec11_productSimulator.cil.c:70-70)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2873..2874 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2873-2874)
  on lines 2881..2883 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2881-2883)
  on lines 2885..2886 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2885-2886)
  on lines 2888..2889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2888-2889)
  on lines 2896..2898 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2896-2898)
  on lines 2900..2901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2900-2901)
  on lines 2903..2904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2903-2904)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2736..2737 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2736-2737)
  on lines 2739..2740 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2739-2740)
  on lines 2747..2749 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2747-2749)
  on lines 2751..2752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2751-2752)
  on lines 2754..2755 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2754-2755)
  on lines 2762..2764 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2762-2764)
  on lines 2766..2767 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2766-2767)
  on lines 2769..2770 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2769-2770)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2543..2544 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2543-2544)
  on lines 2546..2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2546-2547)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2950 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2950-2950)
  on lines 2955..2956 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2955-2956)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 3385 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3385-3385)
  on lines 3390..3391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3390-3391)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 3316..3317 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3316-3317)
  on lines 3327..3328 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3327-3328)
  on lines 3338..3339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3338-3339)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 3155..3156 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3155-3156)
  on lines 3166..3167 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3166-3167)
  on lines 3177..3178 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3177-3178)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1976-1976)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1787 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1787-1787)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1939-1939)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 2087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2087-2087)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 2013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2013-2013)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 2050 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2050-2050)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1824-1824)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 165 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:165-165)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 814
  dead: 547 (351 in uncalled functions)
  total lines: 1361
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2031:9-2031:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3384:7-3384:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2540:7-2540:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2949:7-2949:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3387:9-3387:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2952:9-2952:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2049:9-2049:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2068:9-2068:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:623:9-623:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2086:9-2086:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3437:11-3437:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3002:11-3002:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3027:11-3027:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2152:10-2152:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3049:11-3049:22)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_AutoResponder' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2183:15-2183:47)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3097:7-3097:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3098:9-3098:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1731:9-1731:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3152:9-3152:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1768:9-1768:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3163:11-3163:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2732:7-2732:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2733:9-2733:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1786:9-1786:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3173:11-3173:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3174:13-3174:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1805:9-1805:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3204:7-3204:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3205:9-3205:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1823:9-1823:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2797:7-2797:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2802:11-2802:21)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_AutoResponder' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:408:7-408:39)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1920:9-1920:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1938:9-1938:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2866:7-2866:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2870:11-2870:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1957:9-1957:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3313:9-3313:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1975:9-1975:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3324:11-3324:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3334:11-3334:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:3335:13-3335:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:1994:9-1994:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec11_productSimulator.cil.c:2012:9-2012: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)
