./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/08_rand_cas.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/08_rand_cas.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/pthread-ext/08_rand_cas.i


--------------------------------------------------------------------------------


[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] function PseudoRandomUsingAtomic_nextInt uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     reach_error
[Info]     __VERIFIER_atomic_CAS
[Info]     calculateNext
[Info]     __VERIFIER_nondet_int
[Info]   "up":
[Info]     PseudoRandomUsingAtomic__threadmain
[Info]     thr1
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain for:
[Info] abort, reach_error, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, read, nexts, casret, nextInt_return, r, v, calculateNext_return, s2, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (int )m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:704:2-704:7)
[Info][Witness] unassume invariant: init == 1 && 1 == init (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:753:1-756:1)
[Info][Witness] unassume invariant: 1 == init (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:755:2-755:13)
[Info][Witness] unassume invariant: (int )m == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:709:2-709:7)
[Info][Witness] unassume invariant: ((((n == 10 && 10 == n) && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:726:1-742:1)
[Info][Witness] unassume invariant: (((10 == n && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:8-729:9)
[Info][Witness] unassume invariant: (((10 == n && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:730:3-730:28)
[Info][Witness] unassume invariant: (((10 == n && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:731:3-731:14)
[Info][Witness] unassume invariant: (((10 == n && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:732:3-732:26)
[Info][Witness] unassume invariant: calculateNext_return != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:697:8-697:64)
[Info][Witness] unassume invariant: ((((nexts != 0 && 10 == n) && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:733:3-733:30)
[Info][Witness] unassume invariant: (((((10 == n && (long long )nexts - (long long )read >= 0LL) && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (0LL - (long long )nexts) + (long long )read >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:8-734:24)
[Info][Witness] unassume invariant: ((((nexts != 0 && 10 == n) && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:8-734:24)
[Info][Witness] unassume invariant: (unsigned long )v == (unsigned long )(& seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:711:1-725:1)
[Info][Witness] unassume invariant: (unsigned long )v == (unsigned long )(& seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:717:5-717:12)
[Info][Witness] unassume invariant: (unsigned long )v == (unsigned long )(& seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:719:3-719:17)
[Info][Witness] unassume invariant: (unsigned long )v == (unsigned long )(& seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:719:3-719:17)
[Info][Witness] unassume invariant: (unsigned long )v == (unsigned long )(& seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:723:3-723:9)
[Info][Witness] unassume invariant: (((((((casret == 0 || casret == 1) && 10 == n) && (2147483648LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (2147483647LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (2147483649LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (2147483648LL + (long long )casret) + (long long )nextInt_return >= 0LL) && casret <= 1) && 0 <= casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:735:3-735:50)
[Info][Witness] unassume invariant: ((((n == 10 && 10 == n) && (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:6-736:17)
[Info][Witness] unassume invariant: (10 == n && nextInt_return <= 9) && -9 <= nextInt_return (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:8-729:9)
[Info][Witness] unassume invariant: (((((nexts != 0 && n == 10) && 10 == n) && (2147483648LL - (long long )casret) - (long long )nextInt_return >= 0LL) && (2147483646LL + (long long )casret) - (long long )nextInt_return >= 0LL) && (2147483649LL - (long long )casret) + (long long )nextInt_return >= 0LL) && (2147483647LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:6-736:17)
[Info][Witness] unassume invariant: (10 == n && nextInt_return <= 9) && -9 <= nextInt_return (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:737:4-737:30)
[Info][Witness] unassume invariant: myrand <= 9 && -9 <= myrand (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:760:2-760:46)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:74:1-78:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:79:1-83:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:84:1-88:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:89:1-93:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:94:1-98:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'PseudoRandomUsingAtomic_monitor' has dead code:
  on line 752 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:752-752)
[Warning][Deadcode] Function 'main' has dead code:
  on line 786 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:786-786)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 59
  dead: 7 (5 in uncalled functions)
  total lines: 66
[Warning][Race] Memory location seed (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:700:14-700:18)
  write with [region:{seed}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & *v) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:719:3-719:17)
  write with [region:{seed}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:13-785:43]] (conf. 110)  (exp: & *v) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:719:3-719:17)
  write with region:{seed} (conf. 110)  (exp: & seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:755:2-755:13)
  write with [region:{seed}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:13-785:43]] (conf. 110)  (exp: & seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:755:2-755:13)
  read with [region:{seed}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & *v) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:717:5-717:12)
  read with [region:{seed}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:13-785:43]] (conf. 110)  (exp: & *v) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:717:5-717:12)
  read with [region:{seed}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:731:3-731:14)
  read with [region:{seed}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:13-785:43]] (conf. 110)  (exp: & seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:731:3-731:14)
  read with [region:{seed}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:748:7-748:23)
  read with [region:{seed}, lock:{[__VERIFIER_atomic]}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:13-785:43]] (conf. 110)  (exp: & seed) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:748:7-748:23)
[Warning][Deadcode][CWE-570] condition '! (myrand <= 10)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:761:7-761:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:8-785:9)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:17:73-17:74)
[Warning][Race] Memory location state (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:763:14-763:23)
  write with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:771:3-771:12)
  write with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:13-785:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:771:3-771:12)
  read with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:769:2-769:8)
  read with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:13-785:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:769:2-769:8)
  read with region:{state} (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:775:2-775:8)
  read with [region:{state}, thread:[main, thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:785:13-785:43]] (conf. 110)  (exp: & state) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:775:2-775:8)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:8-729:9)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:745:8-745:9)
[Success][Witness] invariant confirmed: v == & seed (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:719:3)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:737:4)
[Success][Witness] invariant confirmed: (2147483649LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:737:4)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:737:4)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:737:4)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:737:4)
[Success][Witness] invariant confirmed: n == 10 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:737:4)
[Success][Witness] invariant confirmed: nexts != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:737:4)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:731:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:731:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:731:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:731:3)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:731:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:733:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:733:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:733:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:733:3)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:733:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:735:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:735:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:735:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:735:3)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:735:3)
[Success][Witness] invariant confirmed: nexts != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:735:3)
[Success][Witness] invariant confirmed: 1 == init (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:756:1)
[Success][Witness] invariant confirmed: v == & seed (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:725:1)
[Warning][Witness] invariant unconfirmed: (int )m == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:705:1)
[Success][Witness] invariant confirmed: -9 <= myrand (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:761:4)
[Success][Witness] invariant confirmed: myrand <= 9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:761:4)
[Success][Witness] invariant confirmed: v == & seed (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:723:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:730:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:730:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:730:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:730:3)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:730:3)
[Warning][Witness] invariant unconfirmed: (int )m == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:710:1)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:732:3)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:732:3)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:732:3)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:732:3)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:732:3)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:5)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:5)
[Success][Witness] invariant confirmed: nexts != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:5)
[Success][Witness] invariant confirmed: 1 == init (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:755:2)
[Success][Witness] invariant confirmed: init == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:755:2)
[Success][Witness] invariant confirmed: -9 <= nextInt_return (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:741:2)
[Success][Witness] invariant confirmed: nextInt_return <= 9 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:741:2)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:741:2)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:36)
[Success][Witness] invariant confirmed: (0LL - (long long )nexts) + (long long )read >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:36)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:36)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:36)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:36)
[Success][Witness] invariant confirmed: (long long )nexts - (long long )read >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:36)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:734:36)
[Success][Witness] invariant confirmed: v == & seed (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:717:2)
[Success][Witness] invariant confirmed: 0 <= casret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:3)
[Success][Witness] invariant confirmed: casret <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:3)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:3)
[Success][Witness] invariant confirmed: (2147483649LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:3)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:3)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:3)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:3)
[Success][Witness] invariant confirmed: casret == 0 || casret == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:736:3)
[Success][Witness] invariant confirmed: calculateNext_return != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:698:2)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:2)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )casret) + (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:2)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:2)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )casret) - (long long )nextInt_return >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:2)
[Success][Witness] invariant confirmed: 10 == n (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:2)
[Success][Witness] invariant confirmed: n == 10 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-ext/08_rand_cas.i:729:2)
[Info][Witness] witness validation summary:
  confirmed: 73
  unconfirmed: 2
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 75
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 1
  vulnerable: 0
  unsafe: 2
  total memory locations: 3
