How to read the tables?
Meaning of the model-checker's resultsModel-checker on the instrumented program | Observed state in Litmus | Picture |
VERIFICATION FAILED | YES | ![]() |
VERIFICATION SUCCESSFUL | NO | ![]() |
Reading the results in the experiments tables
The table below is an excerpt of former results we obtained for x86/podwr experiments.
- In the first column, we can read the name of the original Litmus test (with a link to the file), and the expected violation cycle. The second column gathers the results of the model-checkers for SC. As we are interested in WMM bugs, the verification for SC should be
.
- The three next columns concern TSO model. The last column tells which result we should get for this program under TSO, namely
. We see in the third column that Satabs indeed finds the correct result when checking the instrumented program. ESBMC in this example is missing the counterexample. Threader is either returning an error, or killed by timeout (here, it is an error).
- Note that there are two columns for TSO results: in the first one, we instrument all the delays; in the second one, we instrument only one delay per cycle.
- We also experiment under PSO, RMO and Power, and with additional model-checkers: additional columns of results (and expected results) appear after TSO's columns.
Name | SC | TSO (all delay/cyc) | TSO (1 delay/cyc) | Expected (TSO) | ... |
x86/podwr000 Fre PodWR Fre PodWR |
SatAbs: ![]() 0.60sec ESBMC: ![]() Threader: ![]() ... |
Cycles SatAbs: ![]() 3.94sec (x6.56) ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 491.99sec ... |
Cycles SatAbs: ![]() 2.43sec (x4.05) ESBMC: ![]() Threader: ERROR/TIMEOUT[1] 182.60sec ... |
![]() |
... |
ppc/podrwposwr (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests involving pairs showing that Power can reorder read-read pairs. Therefore they should answer Yes in litmus terms, or Verification Failed in verification terms as soon as the model is Power.
Name | SC | CAV'11 | TSO (all delay/cyc) | TSO (1 delay/cyc) | TSO (opt delay/cyc) | Expected (TSO) | PSO (all delay/cyc) | PSO (1 delay/cyc) | PSO (opt delay/cyc) | Expected (PSO) | RMO (all delay/cyc) | RMO (1 delay/cyc) | RMO (opt delay/cyc) | Expected (RMO) | Power (all delay/cyc) | Power (1 delay/cyc) | Power (opt delay/cyc) | Expected (Power) |
ppc/podrwposwr000 |
SatAbs: ![]() 0.45sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.00sec ESBMC: 0.07sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 2.78sec (x6.17) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.19sec Threader-monolithic: ERROR/TIMEOUT[130] 896.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.38sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 29.83sec (x66.28) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 395.60sec Checkfence: 0.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.00sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.29sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 32.57sec (x72.37) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 363.36sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 894.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.03sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 29.12sec (x64.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 361.35sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 896.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.81sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 31.05sec (x69.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 438.98sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 877.66sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 29.91sec (x66.46) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 375.95sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 895.73sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.72sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 28.16sec (x62.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 343.40sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 894.75sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.10sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 84.06sec (x186.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 495.46sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 23.74sec (x52.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 403.70sec Threader-owicki-gries: ERROR/TIMEOUT[1] 386.85sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 515.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 23.04sec (x51.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 517.49sec Threader-owicki-gries: ERROR/TIMEOUT[1] 523.47sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 538.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 828.93sec (x1842.06) Satabs-prefix-first: ERROR/TIMEOUT[130] 922.01sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 497.58sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.59sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 30.66sec (x68.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 528.00sec Threader-owicki-gries: ERROR/TIMEOUT[1] 503.97sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 534.60sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 23.08sec (x51.28) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 525.33sec Threader-owicki-gries: ERROR/TIMEOUT[1] 453.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 405.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr001 |
SatAbs: ![]() 3.85sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 257.53sec Checkfence: 0.00sec ESBMC: 0.09sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 9.01sec (x2.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 414.72sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.59sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 144.97sec (x37.65) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 407.84sec Checkfence: 0.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.38sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 171.48sec (x44.54) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 389.50sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.57sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.25sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 148.17sec (x38.48) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 348.03sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.57sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.72sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 139.84sec (x36.32) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 322.36sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 143.29sec (x37.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 402.34sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 143.31sec (x37.22) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 415.93sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.37sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.84sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1013.05sec (x263.12) Satabs-prefix-first: ERROR/TIMEOUT[130] 922.19sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 364.26sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.78sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 86.39sec (x22.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 393.30sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 603.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 511.20sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 454.73sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 86.75sec (x22.53) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 351.10sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 511.26sec Threader-owicki-gries: ERROR/TIMEOUT[1] 438.70sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 593.85sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1052.83sec (x273.46) Satabs-prefix-first: ERROR/TIMEOUT[130] 933.28sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 497.83sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.96sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 83.84sec (x21.77) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 384.86sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[1] 591.20sec Threader-owicki-gries: ERROR/TIMEOUT[1] 470.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 470.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 87.65sec (x22.76) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 437.20sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 624.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 629.70sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 628.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr002 |
SatAbs: ![]() 1.10sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 294.34sec Checkfence: 0.00sec ESBMC: 0.09sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 6.27sec (x5.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 440.65sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.06sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.63sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 131.23sec (x119.30) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 365.05sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.34sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 134.16sec (x121.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 366.31sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.16sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.29sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 109.39sec (x99.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 348.27sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.66sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 124.23sec (x112.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 335.55sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.06sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 127.23sec (x115.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 358.46sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.48sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.24sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 131.93sec (x119.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 270.79sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.20sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.96sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1101.50sec (x1001.36) Satabs-prefix-first: ERROR/TIMEOUT[130] 960.22sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 574.00sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.57sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 59.10sec (x53.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 399.28sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 464.54sec Threader-owicki-gries: ERROR/TIMEOUT[1] 543.80sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 511.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 57.97sec (x52.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 342.07sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 479.84sec Threader-owicki-gries: ERROR/TIMEOUT[1] 632.51sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 521.58sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1297.11sec (x1179.19) Satabs-prefix-first: ERROR/TIMEOUT[130] 913.81sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 539.71sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 897.09sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.47sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 46.19sec (x41.99) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 392.24sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 581.01sec Threader-owicki-gries: ERROR/TIMEOUT[1] 589.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 515.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 43.07sec (x39.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 345.29sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 633.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 523.59sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 623.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr003 |
SatAbs: ![]() 0.79sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 327.26sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 14.30sec (x18.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 402.44sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 300.31sec (x380.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 304.92sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.12sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.52sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 350.59sec (x443.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 362.19sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 348.83sec (x441.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 314.26sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.90sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 346.05sec (x438.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 405.93sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.20sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.38sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 332.27sec (x420.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 402.28sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.70sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.36sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 318.33sec (x402.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 304.82sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.52sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1029.88sec (x1303.64) Satabs-prefix-first: ERROR/TIMEOUT[130] 936.55sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 537.70sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.11sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 59.83sec (x75.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 262.68sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 464.19sec Threader-owicki-gries: ERROR/TIMEOUT[1] 593.31sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 613.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 62.90sec (x79.62) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 395.22sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 601.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 593.64sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 454.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1290.80sec (x1633.92) Satabs-prefix-first: ERROR/TIMEOUT[130] 932.17sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 514.78sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 895.86sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.60sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 81.12sec (x102.68) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 421.37sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 461.99sec Threader-owicki-gries: ERROR/TIMEOUT[1] 483.54sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 456.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 72.90sec (x92.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 385.27sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 506.49sec Threader-owicki-gries: ERROR/TIMEOUT[1] 572.15sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 457.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr004 |
SatAbs: ![]() 0.50sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.07sec |
Cycles
SatAbs: ![]() 1.86sec (x3.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 25.91sec (x51.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 277.32sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.35sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.39sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 25.86sec (x51.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 294.93sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.98sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.05sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 25.40sec (x50.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 355.04sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 23.77sec (x47.54) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 354.72sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 896.94sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.19sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 25.36sec (x50.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 345.46sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.59sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.15sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 26.99sec (x53.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 339.66sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.20sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.98sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 206.46sec (x412.92) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.23sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.04sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.60sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 12.71sec (x25.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[1] 420.72sec Threader-owicki-gries: ERROR/TIMEOUT[1] 420.36sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 328.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 12.67sec (x25.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 304.87sec Threader-owicki-gries: ERROR/TIMEOUT[1] 344.63sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 334.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 96.94sec (x193.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 896.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 13.49sec (x26.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 295.81sec Threader-owicki-gries: ERROR/TIMEOUT[1] 418.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 368.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 14.32sec (x28.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 366.69sec Threader-owicki-gries: ERROR/TIMEOUT[1] 338.17sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 376.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr005 |
SatAbs: ![]() 1.27sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 36.51sec (x28.74) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 460.69sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 2.07sec (x1.62) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 253.77sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 2.15sec (x1.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 231.18sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 2.91sec (x2.29) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 235.58sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 2.17sec (x1.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 151.09sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.15sec (x1.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.59sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.07sec (x1.62) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 233.91sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 3.64sec (x2.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 292.34sec Threader-owicki-gries: ERROR/TIMEOUT[1] 390.86sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 390.60sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.83sec (x3.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 392.32sec Threader-owicki-gries: ERROR/TIMEOUT[1] 336.75sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 392.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.78sec (x2.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 310.71sec Threader-owicki-gries: ERROR/TIMEOUT[1] 333.24sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 306.84sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 3.55sec (x2.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.04sec Threader-monolithic: ERROR/TIMEOUT[1] 275.95sec Threader-owicki-gries: ERROR/TIMEOUT[1] 335.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 378.84sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.87sec (x3.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 271.49sec Threader-owicki-gries: ERROR/TIMEOUT[1] 308.19sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 308.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.69sec (x2.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 306.84sec Threader-owicki-gries: ERROR/TIMEOUT[1] 294.36sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 291.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr006 |
SatAbs: ![]() 3.17sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 202.89sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 7.28sec (x2.29) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 313.69sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.69sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: ![]() 138.96sec (x43.83) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 389.51sec Checkfence: 0.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.09sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 144.91sec (x45.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 422.05sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.16sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 154.67sec (x48.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 373.00sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 895.79sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.90sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 145.29sec (x45.83) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 387.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.00sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.39sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 146.31sec (x46.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 311.21sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.99sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 147.66sec (x46.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 395.73sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.26sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 601.09sec (x189.61) Satabs-prefix-first: ERROR/TIMEOUT[130] 914.44sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 498.33sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.22sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 39.95sec (x12.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 321.61sec ESBMC: 0.19sec Threader-monolithic: ERROR/TIMEOUT[1] 486.78sec Threader-owicki-gries: ERROR/TIMEOUT[1] 422.88sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 425.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 38.68sec (x12.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 237.60sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 427.26sec Threader-owicki-gries: ERROR/TIMEOUT[1] 359.89sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 500.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1025.98sec (x323.65) Satabs-prefix-first: ERROR/TIMEOUT[130] CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 547.65sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.11sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.59sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 63.84sec (x20.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 368.66sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 489.64sec Threader-owicki-gries: ERROR/TIMEOUT[1] 494.25sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 485.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 66.00sec (x20.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 334.32sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 371.88sec Threader-owicki-gries: ERROR/TIMEOUT[1] 460.26sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 459.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr007 |
SatAbs: ![]() 5.41sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 345.38sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 171.91sec (x31.77) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 439.44sec ESBMC: 0.14sec Threader-monolithic: ERROR/TIMEOUT[130] 895.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.81sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 26.96sec (x4.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 306.55sec Checkfence: 0.00sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 26.28sec (x4.85) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 261.35sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 26.51sec (x4.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 316.25sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
![]() |
Cycles
SatAbs: ![]() 26.53sec (x4.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 266.60sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 27.39sec (x5.06) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 295.15sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 25.45sec (x4.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 318.76sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 319.72sec (x59.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 290.85sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 437.55sec Threader-owicki-gries: ERROR/TIMEOUT[1] 485.24sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 438.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 374.35sec (x69.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 267.91sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 411.82sec Threader-owicki-gries: ERROR/TIMEOUT[1] 488.43sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 494.96sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 360.68sec (x66.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 332.35sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 475.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 496.97sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 495.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 362.47sec (x67.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 323.94sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 496.19sec Threader-owicki-gries: ERROR/TIMEOUT[1] 409.32sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 458.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 365.89sec (x67.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 286.37sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 361.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 500.36sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 451.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 348.95sec (x64.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 347.86sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 495.31sec Threader-owicki-gries: ERROR/TIMEOUT[1] 446.60sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 416.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr008 |
SatAbs: ![]() 12.00sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 244.84sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 9.32sec (x.77) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 320.08sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.57sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 9.82sec (x.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 323.60sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 8.67sec (x.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.33sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 9.01sec (x.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 332.93sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 9.32sec (x.77) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 320.58sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 8.60sec (x.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 303.93sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 8.33sec (x.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 316.13sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 73.91sec (x6.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 243.94sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 415.02sec Threader-owicki-gries: ERROR/TIMEOUT[1] 499.69sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 427.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 71.62sec (x5.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 321.34sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 410.65sec Threader-owicki-gries: ERROR/TIMEOUT[1] 476.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 496.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 72.50sec (x6.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 333.42sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 422.30sec Threader-owicki-gries: ERROR/TIMEOUT[1] 362.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 361.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 733.08sec (x61.09) Satabs-prefix-first: ERROR/TIMEOUT[130] 969.09sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 401.29sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 896.20sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.65sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 71.21sec (x5.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 347.60sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 482.70sec Threader-owicki-gries: ERROR/TIMEOUT[1] 497.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 332.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 79.15sec (x6.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 336.55sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 482.21sec Threader-owicki-gries: ERROR/TIMEOUT[1] 398.26sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 338.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr009 |
SatAbs: ![]() 2.12sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 4.04sec (x1.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.20sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.07sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 1.72sec (x.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 255.66sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 1.81sec (x.85) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 254.57sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 1.46sec (x.68) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 249.39sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 1.75sec (x.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 252.12sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 1.79sec (x.84) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 253.69sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 1.63sec (x.76) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 228.37sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 25.63sec (x12.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 302.92sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 393.27sec Threader-owicki-gries: ERROR/TIMEOUT[1] 283.32sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 389.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 24.74sec (x11.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 271.21sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 297.71sec Threader-owicki-gries: ERROR/TIMEOUT[1] 259.83sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 364.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 31.37sec (x14.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 229.10sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 365.15sec Threader-owicki-gries: ERROR/TIMEOUT[1] 299.71sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 390.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 43.89sec (x20.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 317.96sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.58sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.82sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 30.40sec (x14.33) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 290.01sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 328.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 346.51sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 380.89sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 30.55sec (x14.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 247.43sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 384.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 391.74sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 386.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr010 |
SatAbs: ![]() 1.78sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 270.62sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 5.18sec (x2.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 487.03sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.52sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 124.55sec (x69.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 377.38sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.14sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 149.72sec (x84.11) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 326.65sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.22sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 146.04sec (x82.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 338.29sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.77sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.79sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 138.94sec (x78.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 387.73sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 896.89sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.73sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 158.04sec (x88.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 375.49sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 896.95sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 158.14sec (x88.84) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 388.00sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.09sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.09sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 784.73sec (x440.85) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 413.87sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 897.12sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 39.33sec (x22.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 367.70sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 496.60sec Threader-owicki-gries: ERROR/TIMEOUT[1] 495.19sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 494.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 42.87sec (x24.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 339.71sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 438.97sec Threader-owicki-gries: ERROR/TIMEOUT[1] 484.03sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 467.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 912.53sec (x512.65) Satabs-prefix-first: ERROR/TIMEOUT[130] 933.45sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 539.53sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.89sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 32.74sec (x18.39) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 313.82sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 496.68sec Threader-owicki-gries: ERROR/TIMEOUT[1] 486.63sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 496.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 33.43sec (x18.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 308.68sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 461.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 449.87sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 422.72sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr011 |
SatAbs: ![]() 3.40sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 338.21sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 4.56sec (x1.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 501.65sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 17.46sec (x5.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 296.85sec Checkfence: 0.01sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 15.93sec (x4.68) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 307.03sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: ![]() 16.32sec (x4.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 315.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 16.95sec (x4.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 323.00sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 15.79sec (x4.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 316.26sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 16.32sec (x4.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 305.22sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 62.50sec (x18.38) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 298.01sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 437.73sec Threader-owicki-gries: ERROR/TIMEOUT[1] 361.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 385.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 68.17sec (x20.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 343.73sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 397.70sec Threader-owicki-gries: ERROR/TIMEOUT[1] 499.21sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 346.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 68.60sec (x20.17) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 313.18sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 414.26sec Threader-owicki-gries: ERROR/TIMEOUT[1] 494.27sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 487.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 70.12sec (x20.62) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 269.61sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 439.20sec Threader-owicki-gries: ERROR/TIMEOUT[1] 428.69sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 356.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 76.04sec (x22.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 249.67sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 363.30sec Threader-owicki-gries: ERROR/TIMEOUT[1] 435.72sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 386.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 76.40sec (x22.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 314.70sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 412.40sec Threader-owicki-gries: ERROR/TIMEOUT[1] 496.62sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 450.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr012 |
SatAbs: ![]() 7.56sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 228.40sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 5.32sec (x.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 295.08sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 897.56sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.59sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 15.02sec (x1.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 230.59sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 13.89sec (x1.83) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 252.39sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 13.94sec (x1.84) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 281.48sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 13.80sec (x1.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 301.51sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 14.00sec (x1.85) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 307.81sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 13.80sec (x1.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 268.61sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 55.97sec (x7.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 234.78sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 415.59sec Threader-owicki-gries: ERROR/TIMEOUT[1] 426.19sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 390.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 54.83sec (x7.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 238.39sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 358.59sec Threader-owicki-gries: ERROR/TIMEOUT[1] 356.21sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 442.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 56.38sec (x7.45) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 255.05sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 490.86sec Threader-owicki-gries: ERROR/TIMEOUT[1] 425.26sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 481.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 407.09sec (x53.84) Satabs-prefix-first: ERROR/TIMEOUT[130] 960.15sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 269.47sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.48sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 69.85sec (x9.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 279.68sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 332.99sec Threader-owicki-gries: ERROR/TIMEOUT[1] 342.52sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 331.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 48.71sec (x6.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 218.97sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 333.74sec Threader-owicki-gries: ERROR/TIMEOUT[1] 332.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 330.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr013 |
SatAbs: ![]() 0.79sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 207.34sec Checkfence: 0.01sec ESBMC: 0.06sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 8.15sec (x10.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 308.08sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.59sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.60sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 140.68sec (x178.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 272.56sec Checkfence: 0.01sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.49sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 142.51sec (x180.39) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 266.10sec ESBMC: 0.05sec Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 120.67sec (x152.74) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 266.14sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 896.95sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.97sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 130.51sec (x165.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 269.35sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.54sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 121.09sec (x153.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 267.56sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 175.94sec (x222.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 389.07sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.38sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] Satabs-prefix-first: ERROR/TIMEOUT[130] 916.18sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 519.18sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[130] 894.92sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.24sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.52sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 52.80sec (x66.83) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 327.56sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 406.35sec Threader-owicki-gries: ERROR/TIMEOUT[1] 484.35sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 436.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 51.95sec (x65.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 336.78sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 392.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 406.68sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 430.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 1006.46sec (x1274.00) Satabs-prefix-first: ERROR/TIMEOUT[130] 916.80sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 429.79sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 43.00sec (x54.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 331.95sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 349.22sec Threader-owicki-gries: ERROR/TIMEOUT[1] 345.74sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 348.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 43.29sec (x54.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 272.58sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 409.41sec Threader-owicki-gries: ERROR/TIMEOUT[1] 363.56sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 419.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr014 |
SatAbs: ![]() 4.91sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 268.93sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 122.24sec (x24.89) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 357.68sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 896.81sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.01sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 12.74sec (x2.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 318.53sec Checkfence: 0.00sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
Cycles
SatAbs: ![]() 12.84sec (x2.61) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 319.01sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 12.25sec (x2.49) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 313.22sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.01sec |
![]() |
Cycles
SatAbs: ![]() 13.17sec (x2.68) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 218.09sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 12.77sec (x2.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 321.17sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 12.72sec (x2.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 351.05sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 236.82sec (x48.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 316.09sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 493.73sec Threader-owicki-gries: ERROR/TIMEOUT[1] 455.66sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 444.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 223.24sec (x45.46) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 373.03sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 347.32sec Threader-owicki-gries: ERROR/TIMEOUT[1] 373.68sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 452.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 225.36sec (x45.89) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 347.27sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 494.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 489.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 471.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 291.69sec (x59.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 346.18sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 480.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 468.55sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 462.36sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 322.33sec (x65.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 350.34sec ESBMC: 0.12sec Threader-monolithic: ERROR/TIMEOUT[1] 353.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 491.50sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 370.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 336.41sec (x68.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 272.80sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 433.17sec Threader-owicki-gries: ERROR/TIMEOUT[1] 497.53sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 443.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
ppc/podrwposwr015 |
SatAbs: ![]() 4.28sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 322.54sec Checkfence: 0.01sec ESBMC: 0.08sec Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 13.63sec (x3.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 431.64sec ESBMC: 0.13sec Threader-monolithic: ERROR/TIMEOUT[130] 896.86sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.01sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 8.21sec (x1.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 238.18sec Checkfence: 0.01sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 8.20sec (x1.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 331.20sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.13sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
Cycles
SatAbs: ![]() 8.54sec (x1.99) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 330.27sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[2] 0.00sec |
![]() |
Cycles
SatAbs: ![]() 8.51sec (x1.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 227.49sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.13sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 7.79sec (x1.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 321.38sec ESBMC: 0.09sec Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 10.44sec (x2.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 329.65sec ESBMC: 0.07sec Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 56.42sec (x13.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 316.43sec ESBMC: 0.08sec Threader-monolithic: ERROR/TIMEOUT[1] 491.23sec Threader-owicki-gries: ERROR/TIMEOUT[1] 488.23sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 495.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 56.88sec (x13.28) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 346.41sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 357.18sec Threader-owicki-gries: ERROR/TIMEOUT[1] 347.85sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 351.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 55.62sec (x12.99) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 258.06sec ESBMC: 0.10sec Threader-monolithic: ERROR/TIMEOUT[1] 495.86sec Threader-owicki-gries: ERROR/TIMEOUT[1] 496.76sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 399.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 774.96sec (x181.06) Satabs-prefix-first: ERROR/TIMEOUT[130] 956.46sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 383.24sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.15sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 66.54sec (x15.54) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 331.15sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 484.91sec Threader-owicki-gries: ERROR/TIMEOUT[1] 477.16sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 448.21sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 67.66sec (x15.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 329.12sec ESBMC: 0.11sec Threader-monolithic: ERROR/TIMEOUT[1] 483.51sec Threader-owicki-gries: ERROR/TIMEOUT[1] 467.94sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 475.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |