./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_spec3_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_spec3_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_spec3_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_spec3_productSimulator.cil.c:490:3-511:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:547:3-572:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:632:5-652: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.268
[Info] vars: 28332, evals: 22839

[Info] |called|=0

Memory statistics: total=20413.72MB, max=251.12MB, minor=20407.80MB, major=313.59MB, promoted=307.66MB
    minor collections=9738  major collections=15 compactions=0

[Warning][Deadcode] Function 'cloneEmail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:252:1-260:1)
[Warning][Deadcode] Function 'prompt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:388:1-402:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_set' is uncalled: 21 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:419:1-464:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_free' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:465:1-520:1)
[Warning][Deadcode] Function '__utac__exception__cf_handler_reset' is uncalled: 24 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:521:1-580:1)
[Warning][Deadcode] Function '__utac__error_stack_mgt' is uncalled: 49 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:583:1-685:1)
[Warning][Deadcode] Function '__utac__get_this_arg' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:686:1-731:1)
[Warning][Deadcode] Function '__utac__get_this_argtype' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:732:1-777:1)
[Warning][Deadcode] Function 'createClient' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1147:1-1161:1)
[Warning][Deadcode] Function 'initEmail' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1364:1-1378:1)
[Warning][Deadcode] Function 'setEmailId' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1400:1-1415:1)
[Warning][Deadcode] Function 'getEmailSubject' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1492:1-1512:1)
[Warning][Deadcode] Function 'setEmailSubject' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1513:1-1528:1)
[Warning][Deadcode] Function 'getEmailBody' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1531:1-1551:1)
[Warning][Deadcode] Function 'setEmailBody' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1552:1-1567:1)
[Warning][Deadcode] Function 'initClient' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2051:1-2065:1)
[Warning][Deadcode] Function 'getClientName' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2069:1-2094:1)
[Warning][Deadcode] Function 'setClientName' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2095:1-2114:1)
[Warning][Deadcode] Function 'getClientOutbuffer' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2119:1-2142:1)
[Warning][Deadcode] Function 'setClientOutbuffer' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2143:1-2162:1)
[Warning][Deadcode] Function 'createClientAddressBookEntry' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2210:1-2234:1)
[Warning][Deadcode] Function 'getClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2244:1-2312:1)
[Warning][Deadcode] Function 'findClientAddressBookAlias' is uncalled: 39 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2313:1-2381:1)
[Warning][Deadcode] Function 'rjhToBob' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3250:1-3260:1)
[Warning][Deadcode] Function 'rjhKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3339:1-3350:1)
[Warning][Deadcode] Function 'bobKeyAddChuck' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3351:1-3362:1)
[Warning][Deadcode] Function '__automaton_fail' has dead code:
  on line 409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:409-409)
[Warning][Deadcode] Function 'createClientKeyringEntry' has dead code:
  on line 2735 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2735-2735)
[Warning][Deadcode] Function 'createEmail' has dead code:
  on line 273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:273-273)
[Warning][Deadcode] Function 'findPublicKey' has dead code:
  on line 2959 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2959-2959)
[Warning][Deadcode] Function 'getClientAddressBookAddress' has dead code:
  on lines 2460..2462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2460-2462)
  on lines 2464..2465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2464-2465)
  on lines 2470..2473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2470-2473)
  on lines 2475..2477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2475-2477)
  on lines 2479..2481 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2479-2481)
  on lines 2483..2484 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2483-2484)
  on lines 2489..2492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2489-2492)
  on lines 2494..2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2494-2496)
  on lines 2498..2500 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2498-2500)
  on lines 2502..2503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2502-2503)
  on lines 2508..2509 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2508-2509)
  on line 2513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2513-2513)
[Warning][Deadcode] Function 'getClientAddressBookSize' has dead code:
  on line 2187 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2187-2187)
[Warning][Deadcode] Function 'getClientAutoResponse' has dead code:
  on line 2596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2596-2596)
[Warning][Deadcode] Function 'getClientForwardReceiver' has dead code:
  on line 3031 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3031-3031)
[Warning][Deadcode] Function 'getClientId' has dead code:
  on line 3078 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3078-3078)
[Warning][Deadcode] Function 'getClientKeyringPublicKey' has dead code:
  on lines 2863..2865 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2863-2865)
  on lines 2867..2868 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2867-2868)
  on lines 2872..2875 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2872-2875)
  on lines 2877..2879 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2877-2879)
  on lines 2881..2882 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2881-2882)
  on lines 2886..2889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2886-2889)
  on lines 2891..2893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2891-2893)
  on lines 2895..2896 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2895-2896)
  on lines 2900..2901 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2900-2901)
  on line 2905 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2905-2905)
[Warning][Deadcode] Function 'getClientKeyringSize' has dead code:
  on lines 2685..2686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2685-2686)
  on line 2690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2690-2690)
[Warning][Deadcode] Function 'getClientKeyringUser' has dead code:
  on lines 2756..2758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2756-2758)
  on lines 2760..2761 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2760-2761)
  on lines 2765..2768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2765-2768)
  on lines 2770..2772 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2770-2772)
  on lines 2774..2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2774-2775)
  on lines 2779..2782 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2779-2782)
  on lines 2784..2786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2784-2786)
  on lines 2788..2789 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2788-2789)
  on lines 2793..2794 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2793-2794)
  on line 2798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2798-2798)
[Warning][Deadcode] Function 'getClientPrivateKey' has dead code:
  on line 2643 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2643-2643)
[Warning][Deadcode] Function 'getEmailEncryptionKey' has dead code:
  on lines 1616..1617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1616-1617)
  on line 1623 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1623-1623)
[Warning][Deadcode] Function 'getEmailFrom' has dead code:
  on lines 1427..1428 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1427-1428)
  on line 1434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1434-1434)
[Warning][Deadcode] Function 'getEmailId' has dead code:
  on lines 1390..1391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1390-1391)
  on line 1397 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1397-1397)
[Warning][Deadcode] Function 'getEmailSignKey' has dead code:
  on lines 1690..1691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1690-1691)
  on line 1697 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1697-1697)
[Warning][Deadcode] Function 'getEmailTo' has dead code:
  on lines 1464..1465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1464-1465)
  on line 1471 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1471-1471)
[Warning][Deadcode] Function 'get_queued_client' has dead code:
  on line 1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1200-1200)
[Warning][Deadcode] Function 'get_queued_email' has dead code:
  on line 1209 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1209-1209)
[Warning][Deadcode] Function 'isEncrypted' has dead code:
  on lines 1579..1580 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1579-1580)
  on line 1586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1586-1586)
[Warning][Deadcode] Function 'isKeyPairValid' has dead code:
  on lines 1226..1227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1226-1227)
  on line 1234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1234-1234)
[Warning][Deadcode] Function 'isReadable' has dead code:
  on line 249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:249-249)
[Warning][Deadcode] Function 'isReadable__before__Encrypt' has dead code:
  on line 211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:211-211)
[Warning][Deadcode] Function 'isReadable__role__Encrypt' has dead code:
  on line 231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:231-231)
[Warning][Deadcode] Function 'isSigned' has dead code:
  on lines 1653..1654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1653-1654)
  on line 1660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1660-1660)
[Warning][Deadcode] Function 'isVerified' has dead code:
  on lines 1727..1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1727-1728)
  on line 1734 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1734-1734)
[Warning][Deadcode] Function 'is_queue_empty' has dead code:
  on line 1191 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1191-1191)
[Warning][Deadcode] Function 'outgoing' has dead code:
  on line 962 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:962-962)
  on line 964 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:964-964)
[Warning][Deadcode] Function 'printMail__before__Verify' has dead code:
  on line 168 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:168-168)
  on line 170 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:170-170)
[Warning][Deadcode] Function 'select_one' has dead code:
  on line 288 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:288-288)
[Warning][Deadcode] Function 'setClientAddressBookAddress' has dead code:
  on lines 2527..2528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2527-2528)
  on lines 2535..2537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2535-2537)
  on lines 2539..2540 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2539-2540)
  on lines 2542..2543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2542-2543)
  on lines 2550..2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2550-2552)
  on lines 2554..2555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2554-2555)
  on lines 2557..2558 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2557-2558)
[Warning][Deadcode] Function 'setClientAddressBookAlias' has dead code:
  on lines 2390..2391 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2390-2391)
  on lines 2393..2394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2393-2394)
  on lines 2401..2403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2401-2403)
  on lines 2405..2406 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2405-2406)
  on lines 2408..2409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2408-2409)
  on lines 2416..2418 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2416-2418)
  on lines 2420..2421 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2420-2421)
  on lines 2423..2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2423-2424)
[Warning][Deadcode] Function 'setClientAddressBookSize' has dead code:
  on lines 2197..2198 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2197-2198)
  on lines 2200..2201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2200-2201)
[Warning][Deadcode] Function 'setClientAutoResponse' has dead code:
  on line 2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2604-2604)
  on lines 2609..2610 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2609-2610)
[Warning][Deadcode] Function 'setClientForwardReceiver' has dead code:
  on line 3039 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3039-3039)
  on lines 3044..3045 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3044-3045)
[Warning][Deadcode] Function 'setClientKeyringPublicKey' has dead code:
  on lines 2970..2971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2970-2971)
  on lines 2981..2982 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2981-2982)
  on lines 2992..2993 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2992-2993)
[Warning][Deadcode] Function 'setClientKeyringUser' has dead code:
  on lines 2809..2810 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2809-2810)
  on lines 2820..2821 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2820-2821)
  on lines 2831..2832 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2831-2832)
[Warning][Deadcode] Function 'setEmailEncryptionKey' has dead code:
  on line 1634 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1634-1634)
[Warning][Deadcode] Function 'setEmailFrom' has dead code:
  on line 1445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1445-1445)
[Warning][Deadcode] Function 'setEmailIsEncrypted' has dead code:
  on line 1597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1597-1597)
[Warning][Deadcode] Function 'setEmailIsSignatureVerified' has dead code:
  on line 1745 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1745-1745)
[Warning][Deadcode] Function 'setEmailIsSigned' has dead code:
  on line 1671 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1671-1671)
[Warning][Deadcode] Function 'setEmailSignKey' has dead code:
  on line 1708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1708-1708)
[Warning][Deadcode] Function 'setEmailTo' has dead code:
  on line 1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1482-1482)
[Warning][Deadcode] Function 'valid_product' has dead code:
  on line 362 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:362-362)
  on line 383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:383-383)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 828
  dead: 550 (351 in uncalled functions)
  total lines: 1378
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2387:9-2387:19)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2827:11-2827:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2828:13-2828:23)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2858:7-2858:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1444:9-1444:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2859:9-2859:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1463:9-1463:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1481:9-1481:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2451:7-2451:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2456:11-2456:21)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Sign' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:955:7-955:30)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1578:9-1578:20)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2520:7-2520:18)
[Warning][Deadcode][CWE-571] condition 'index == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2524:11-2524:21)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1596:9-1596:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2967:9-2967:19)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Sign' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:161:7-161:30)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1615:9-1615:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2978:11-2978:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2988:11-2988:22)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2989:13-2989:23)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1633:9-1633:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1652:9-1652:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1670:9-1670:20)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3038:7-3038:18)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2194:7-2194:18)
[Warning][Deadcode][CWE-570] condition 'handle == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2603:7-2603:18)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3041:9-3041:20)
[Warning][Deadcode][CWE-571] condition 'handle == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2606:9-2606:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1689:9-1689:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1707:9-1707:20)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1726:9-1726:20)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:3091:11-3091:22)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2656:11-2656:22)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1744:9-1744:20)
[Warning][Deadcode][CWE-570] condition '! privateKey' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1225:9-1225:21)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2681:11-2681:22)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Sign' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:337:19-337:44)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Verify' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:342:23-342:50)
[Warning][Deadcode][CWE-571] condition '__SELECTED_FEATURE_Sign' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:345:25-345:48)
[Warning][Deadcode][CWE-570] condition '! __SELECTED_FEATURE_Sign' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:347:27-347:52)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1804:10-1804:11)
[Warning][Deadcode][CWE-571] condition 'handle == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2703:11-2703:22)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2751:7-2751:18)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2752:9-2752:19)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1389:9-1389:20)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2806:9-2806:19)
[Warning][Deadcode][CWE-571] condition 'index == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2817:11-2817:21)
[Warning][Deadcode][CWE-571] condition 'handle == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:2386:7-2386:18)
[Warning][Deadcode][CWE-570] condition 'handle == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/product-lines/email_spec3_productSimulator.cil.c:1426:9-1426: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)
