./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Warning][Deadcode] Function "__VERIFIER_error" will never be called: 1LoC (includes/sv-comp.c:2:1-2:36)
[Warning][Deadcode] Function "__VERIFIER_assume" will never be called: 1LoC (includes/sv-comp.c:9:1-9:89)
[Warning][Deadcode] Function "__VERIFIER_nondet_bool" will never be called: 1LoC (includes/sv-comp.c:15:1-15:57)
[Warning][Deadcode] Function "__VERIFIER_nondet_char" will never be called: 1LoC (includes/sv-comp.c:16:1-16:55)
[Warning][Deadcode] Function "__VERIFIER_nondet_int" will never be called: 1LoC (includes/sv-comp.c:18:1-18:52)
[Warning][Deadcode] Function "__VERIFIER_nondet_float" will never be called: 1LoC (includes/sv-comp.c:19:1-19:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_double" will never be called: 1LoC (includes/sv-comp.c:20:1-20:61)
[Warning][Deadcode] Function "__VERIFIER_nondet_long" will never be called: 1LoC (includes/sv-comp.c:22:1-22:55)
[Warning][Deadcode] Function "__VERIFIER_nondet_pchar" will never be called: 1LoC (includes/sv-comp.c:23:1-23:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_short" will never be called: 1LoC (includes/sv-comp.c:26:1-26:58)
[Warning][Deadcode] Function "__VERIFIER_nondet_uchar" will never be called: 1LoC (includes/sv-comp.c:29:1-29:74)
[Warning][Deadcode] Function "__VERIFIER_nondet_uint" will never be called: 1LoC (includes/sv-comp.c:30:1-30:71)
[Warning][Deadcode] Function "__VERIFIER_nondet_ulong" will never be called: 1LoC (includes/sv-comp.c:31:1-31:74)
[Warning][Deadcode] Function "__VERIFIER_nondet_unsigned" will never be called: 1LoC (includes/sv-comp.c:32:1-32:67)
[Warning][Deadcode] Function "__VERIFIER_nondet_ushort" will never be called: 1LoC (includes/sv-comp.c:33:1-33:77)
[Warning][Deadcode] Function "__VERIFIER_nondet_pointer" will never be called: 1LoC (includes/sv-comp.c:35:1-35:60)
[Warning][Race] Memory location numberOfSeatsSold@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:717:5-717:22 (race with conf. 110):
  read with [region:{numberOfSeatsSold},
           mhp:{tid=[main], {salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64}}] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:722:5-722:47)
  read with [region:{numberOfSeatsSold}, mhp:{tid=[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]}, thread:[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:722:5-722:47)
  read with [region:{numberOfSeatsSold}, mhp:{tid=[main]; created={[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]}}, thread:[main]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:752:3-752:45)
  write with [region:{numberOfSeatsSold}, mhp:{tid=[main], {salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64}}, lock:{[__VERIFIER_atomic]}] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:729:7-729:49)
  write with [region:{numberOfSeatsSold}, mhp:{tid=[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]}, lock:{[__VERIFIER_atomic]}, thread:[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:729:7-729:49)
[Warning][Race] Memory location stopSales@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:718:5-718:14 (race with conf. 110):
  read with [region:{stopSales}, mhp:{tid=[main], {salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64}}] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:721:7-721:17)
  read with [region:{stopSales}, mhp:{tid=[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]}, thread:[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:721:7-721:17)
  write with [region:{stopSales}, mhp:{tid=[main], {salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64}}, lock:{[__VERIFIER_atomic]}] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:725:7-725:20)
  write with [region:{stopSales}, mhp:{tid=[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]}, lock:{[__VERIFIER_atomic]}, thread:[main, salethread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:747:5-747:64]] (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/airline-10.i:725:7-725:20)
SV-COMP result: unknown

Summary for all memory locations:
	safe:            0
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           2
