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 ... |
![]() |
... |
x86/safe (tooling date Sun Jan 22 02:23:23 GMT 2012)
This family corresponds to litmus tests involving only safe x86 relations. Therefore they should answer No in litmus terms, or Verification Successful in verification terms, if the model is x86/TSO.
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) |
x86/safe000 |
SatAbs: ![]() 0.37sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[137] 192.08sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 5.71sec (x15.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 699.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 653.16sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 652.39sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.04sec (x5.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[137] 286.06sec Checkfence: 0.00sec ESBMC: ![]() 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 MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.01sec (x5.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 304.34sec ESBMC: ![]() 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): ![]() |
Cycles
SatAbs: ![]() 2.11sec (x5.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[137] 268.03sec ESBMC: ![]() 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): ![]() |
![]() |
Cycles
SatAbs: ![]() 1.89sec (x5.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 301.30sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 1.95sec (x5.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 295.30sec ESBMC: ![]() 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: ![]() 2.23sec (x6.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 312.40sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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: ERROR/TIMEOUT[130] 666.53sec (x1801.43) Satabs-prefix-first: ERROR/TIMEOUT[130] 603.05sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 669.05sec Threader-owicki-gries: ERROR/TIMEOUT[130] 724.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 636.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 42.08sec (x113.72) Satabs-prefix-first: ERROR/TIMEOUT[130] 615.33sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 717.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 768.02sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 751.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 39.33sec (x106.29) Satabs-prefix-first: ERROR/TIMEOUT[130] 688.85sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 742.96sec Threader-owicki-gries: ERROR/TIMEOUT[130] 703.22sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 772.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 37.44sec (x101.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 823.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 673.67sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 718.72sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 55.73sec (x150.62) Satabs-prefix-first: ERROR/TIMEOUT[130] 791.43sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 24.90sec (x67.29) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 304.63sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 381.28sec Threader-owicki-gries: ERROR/TIMEOUT[1] 355.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 459.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe001 |
SatAbs: ![]() 1.20sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 3.54sec (x2.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.83sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.72sec (x2.26) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 261.79sec Checkfence: 0.01sec ESBMC: ![]() 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): ![]() |
Cycles
SatAbs: ![]() 2.65sec (x2.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 279.29sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.63sec (x2.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 276.30sec ESBMC: ![]() 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 MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 16.79sec (x13.99) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 317.66sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.07sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 14.18sec (x11.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 314.23sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.65sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.12sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 14.85sec (x12.37) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 371.32sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 845.47sec Threader-owicki-gries: ERROR/TIMEOUT[130] 894.94sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 136.75sec (x113.95) Satabs-prefix-first: ERROR/TIMEOUT[130] 909.69sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 55.49sec (x46.24) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.19sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 17.95sec (x14.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 399.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 872.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 890.87sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 24.10sec (x20.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.76sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 59.33sec (x49.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 13.72sec (x11.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 365.72sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe002 |
SatAbs: ![]() 3.52sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 6.61sec (x1.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 4.26sec (x1.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 295.66sec Checkfence: 0.01sec ESBMC: ![]() 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 MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 3.77sec (x1.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 297.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec 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): ![]() |
Cycles
SatAbs: ![]() 4.11sec (x1.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 293.56sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.16sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 11.48sec (x3.26) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 301.09sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 261.63sec Threader-owicki-gries: ERROR/TIMEOUT[1] 253.60sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 190.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 10.42sec (x2.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 232.51sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 235.77sec Threader-owicki-gries: ERROR/TIMEOUT[1] 251.15sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 230.76sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 11.09sec (x3.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 299.46sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 180.04sec Threader-owicki-gries: ERROR/TIMEOUT[1] 185.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 236.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 104.01sec (x29.54) Satabs-prefix-first: ERROR/TIMEOUT[130] 914.62sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.58sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.58sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 88.68sec (x25.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 13.14sec (x3.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 337.40sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 255.77sec Threader-owicki-gries: ERROR/TIMEOUT[1] 248.93sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 259.87sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 28.22sec (x8.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.05sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.49sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 61.35sec (x17.42) Satabs-prefix-first: ERROR/TIMEOUT[130] 903.64sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.90sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.97sec (x3.11) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 249.89sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 250.04sec Threader-owicki-gries: ERROR/TIMEOUT[1] 235.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 231.94sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe003 |
SatAbs: ![]() 0.47sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 1.88sec (x4.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 418.16sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.22sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.15sec (x4.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 241.65sec Checkfence: 0.01sec ESBMC: ![]() 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): ![]() |
Cycles
SatAbs: ![]() 2.11sec (x4.48) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 254.20sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec 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): ![]() |
Cycles
SatAbs: ![]() 2.18sec (x4.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 228.34sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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): ![]() |
![]() |
Cycles
SatAbs: ![]() 212.12sec (x451.31) Satabs-prefix-first: ERROR/TIMEOUT[130] 902.23sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 330.86sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.80sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.77sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 205.52sec (x437.27) Satabs-prefix-first: ERROR/TIMEOUT[130] 903.20sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 385.02sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.22sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.01sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 175.85sec (x374.14) Satabs-prefix-first: ERROR/TIMEOUT[130] 904.23sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 405.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.47sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 892.36sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 985.21sec (x2096.19) Satabs-prefix-first: ERROR/TIMEOUT[130] 917.86sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 308.83sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.02sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 200.72sec (x427.06) Satabs-prefix-first: ERROR/TIMEOUT[130] 902.06sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 354.43sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.07sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.11sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.81sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 179.15sec (x381.17) Satabs-prefix-first: ERROR/TIMEOUT[130] 902.06sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 346.94sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.32sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 21.66sec (x46.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 484.16sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.15sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.49sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 196.95sec (x419.04) Satabs-prefix-first: ERROR/TIMEOUT[130] 901.09sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 408.64sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.64sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 28.66sec (x60.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 233.77sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 478.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 466.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 449.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe004 |
SatAbs: ![]() 0.89sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 2.58sec (x2.89) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 406.82sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.25sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.23sec (x2.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 214.72sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec 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): ![]() |
Cycles
SatAbs: ![]() 2.79sec (x3.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 209.86sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec 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): ![]() |
Cycles
SatAbs: ![]() 2.85sec (x3.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 261.14sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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): ![]() |
![]() |
Cycles
SatAbs: ![]() 412.59sec (x463.58) Satabs-prefix-first: ERROR/TIMEOUT[130] 906.44sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 433.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.63sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 170.63sec (x191.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 399.56sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 13.24sec (x14.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 350.60sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.20sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 527.47sec (x592.66) Satabs-prefix-first: ERROR/TIMEOUT[130] 907.94sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 464.66sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.29sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.32sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 190.71sec (x214.28) Satabs-prefix-first: ERROR/TIMEOUT[130] 905.33sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 399.78sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.19sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 13.72sec (x15.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 342.14sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 19.79sec (x22.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 522.02sec ESBMC: ![]() 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 |
Cycles
SatAbs: ![]() 164.63sec (x184.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 424.06sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 13.87sec (x15.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 264.58sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.08sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe005 |
SatAbs: ![]() 3.51sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 2.80sec (x.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 340.89sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 4.42sec (x1.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 332.01sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 4.60sec (x1.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 252.78sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.12sec 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[1] 0.12sec |
Cycles
SatAbs: ![]() 4.43sec (x1.26) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 328.43sec ESBMC: ![]() 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[1] 0.10sec |
![]() |
Cycles
SatAbs: ![]() 10.41sec (x2.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 336.39sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 254.02sec Threader-owicki-gries: ERROR/TIMEOUT[1] 209.36sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 226.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 13.27sec (x3.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 277.09sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 219.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 264.46sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 187.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 11.06sec (x3.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 324.93sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 190.83sec Threader-owicki-gries: ERROR/TIMEOUT[1] 207.73sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 196.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 11.04sec (x3.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 334.46sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 258.53sec Threader-owicki-gries: ERROR/TIMEOUT[1] 258.23sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 259.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.74sec (x3.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 276.40sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 231.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 176.70sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 264.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.68sec (x3.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 354.85sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 210.25sec Threader-owicki-gries: ERROR/TIMEOUT[1] 215.78sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 259.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 962.22sec (x274.13) Satabs-prefix-first: ERROR/TIMEOUT[130] 929.98sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 441.12sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.70sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.74sec (x3.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 341.96sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 233.90sec Threader-owicki-gries: ERROR/TIMEOUT[1] 259.64sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 258.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 9.73sec (x2.77) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 293.83sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 233.91sec Threader-owicki-gries: ERROR/TIMEOUT[1] 236.72sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 184.84sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe006 |
SatAbs: ![]() 0.20sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 5.32sec (x26.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.49sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.63sec (x3.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.59sec (x2.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.61sec (x3.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 0.72sec (x3.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.10sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.10sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.52sec (x2.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() 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: ![]() 0.67sec (x3.35) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 12.91sec (x64.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 8.91sec (x44.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 256.02sec Threader-owicki-gries: ERROR/TIMEOUT[1] 369.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 328.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 8.82sec (x44.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 296.84sec Threader-owicki-gries: ERROR/TIMEOUT[1] 295.87sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 259.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 14.57sec (x72.85) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 8.54sec (x42.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 335.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 277.29sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 256.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 13.14sec (x65.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 289.16sec Threader-owicki-gries: ERROR/TIMEOUT[1] 260.50sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 282.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe007 |
SatAbs: ![]() 0.38sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 18.32sec (x48.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 345.64sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.96sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.97sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.68sec (x4.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 200.98sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.95sec (x2.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.70sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.89sec (x2.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.05sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 0.77sec (x2.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 190.94sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.81sec (x2.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 211.68sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.85sec (x2.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.63sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 150.87sec (x397.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 34.08sec (x89.68) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 300.53sec Threader-owicki-gries: ERROR/TIMEOUT[1] 303.76sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 299.82sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 34.47sec (x90.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 300.41sec Threader-owicki-gries: ERROR/TIMEOUT[1] 302.19sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 300.70sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 142.28sec (x374.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.84sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.79sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.87sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 26.94sec (x70.89) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 305.52sec Threader-owicki-gries: ERROR/TIMEOUT[1] 302.04sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 300.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 40.52sec (x106.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 202.20sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 297.39sec Threader-owicki-gries: ERROR/TIMEOUT[1] 295.99sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 298.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe008 |
SatAbs: ![]() 0.30sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 6.28sec (x20.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 290.74sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.76sec (x5.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 208.31sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.74sec (x5.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 207.41sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.71sec (x5.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 214.03sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 11.82sec (x39.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 221.64sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.49sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.11sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 12.06sec (x40.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 223.49sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.68sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.20sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 13.89sec (x46.30) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 220.43sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 142.47sec (x474.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 294.02sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.63sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 14.11sec (x47.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 241.12sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.46sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 12.28sec (x40.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 251.52sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.86sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.64sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 22.97sec (x76.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 312.83sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.61sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.58sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.10sec (x33.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 221.40sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.50sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.52sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 25.56sec (x85.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.44sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 295.68sec Threader-owicki-gries: ERROR/TIMEOUT[1] 294.53sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 294.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe009 |
SatAbs: ![]() 0.36sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 5.30sec (x14.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.25sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.23sec (x6.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 184.69sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.12sec (x5.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 185.11sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.18sec (x6.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 185.66sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 2.06sec (x5.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 202.75sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.01sec (x5.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.31sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 1.81sec (x5.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 204.87sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 237.07sec (x658.52) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.79sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 31.91sec (x88.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.56sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 21.70sec (x60.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 293.78sec Threader-owicki-gries: ERROR/TIMEOUT[1] 294.32sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 294.95sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 154.33sec (x428.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.69sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.63sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 25.17sec (x69.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 33.71sec (x93.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.96sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 291.47sec Threader-owicki-gries: ERROR/TIMEOUT[1] 291.78sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 292.86sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe010 |
SatAbs: ![]() 0.21sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 1.58sec (x7.52) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.54sec (x2.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.52sec (x2.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.64sec (x3.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 5.02sec (x23.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.73sec (x17.76) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.36sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.43sec (x16.33) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.21sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.02sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 7.68sec (x36.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.22sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.24sec (x20.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.03sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.18sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 895.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.37sec (x20.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.21sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 3.38sec (x16.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.28sec (x20.38) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.20sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.05sec (x19.28) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.11sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe011 |
SatAbs: ![]() 1.08sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 2.55sec (x2.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 306.75sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.98sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.80sec (x1.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.49sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.88sec (x1.74) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.24sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.93sec (x1.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 193.84sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 31.82sec (x29.46) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 286.95sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 10.41sec (x9.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 235.62sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.59sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 9.33sec (x8.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 219.78sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 148.13sec (x137.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 299.86sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.68sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.77sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.91sec (x10.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 231.68sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.52sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.55sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 11.62sec (x10.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 232.44sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.38sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.22sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 6.15sec (x5.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 336.39sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.54sec (x9.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 232.21sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.25sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 9.10sec (x8.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 221.66sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe012 |
SatAbs: ![]() 2.08sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 23.55sec (x11.32) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 268.44sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.22sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.73sec (x.83) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 202.87sec Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.85sec (x.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 204.72sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.87sec (x.89) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.79sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 6.36sec (x3.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.81sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 165.12sec Threader-owicki-gries: ERROR/TIMEOUT[1] 165.46sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 165.36sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 6.37sec (x3.06) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.86sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 165.47sec Threader-owicki-gries: ERROR/TIMEOUT[1] 166.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 164.79sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 6.99sec (x3.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.52sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 165.33sec Threader-owicki-gries: ERROR/TIMEOUT[1] 165.69sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 164.90sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 190.51sec (x91.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.78sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.65sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 22.68sec (x10.90) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 300.55sec Threader-owicki-gries: ERROR/TIMEOUT[1] 299.93sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 299.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 6.55sec (x3.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 202.17sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 165.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 165.18sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 165.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 138.12sec (x66.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.70sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.69sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.73sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 28.54sec (x13.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 298.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 298.42sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 300.94sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 42.77sec (x20.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.65sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 296.54sec Threader-owicki-gries: ERROR/TIMEOUT[1] 295.49sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 297.88sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe013 |
SatAbs: ![]() 1.87sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 5.70sec (x3.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 290.92sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 3.98sec (x2.12) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 216.48sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec 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[1] 0.07sec |
Cycles
SatAbs: ![]() 3.97sec (x2.12) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 209.54sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 4.10sec (x2.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.22sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.08sec |
![]() |
Cycles
SatAbs: ![]() 5.59sec (x2.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 209.21sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 164.02sec Threader-owicki-gries: ERROR/TIMEOUT[1] 163.20sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 163.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 5.36sec (x2.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 202.95sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 164.39sec Threader-owicki-gries: ERROR/TIMEOUT[1] 162.95sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 164.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 6.05sec (x3.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.26sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 163.91sec Threader-owicki-gries: ERROR/TIMEOUT[1] 163.76sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 164.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 62.99sec (x33.68) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 235.46sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.10sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.37sec (x2.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.18sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 163.97sec Threader-owicki-gries: ERROR/TIMEOUT[1] 164.57sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 164.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.64sec (x3.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.99sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 163.86sec Threader-owicki-gries: ERROR/TIMEOUT[1] 165.19sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 164.80sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 250.52sec (x133.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 315.04sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.58sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.60sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.65sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.61sec (x3.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.06sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 159.88sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.72sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 160.33sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.25sec (x2.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.40sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 157.47sec Threader-owicki-gries: ERROR/TIMEOUT[1] 157.46sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.78sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe014 |
SatAbs: ![]() 0.56sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 2.40sec (x4.28) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.52sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.93sec (x3.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.99sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.87sec (x3.33) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 187.62sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.98sec (x3.53) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 188.26sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 1.97sec (x3.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 187.35sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.19sec (x3.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 187.93sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 1.89sec (x3.37) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 186.81sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 446.84sec (x797.92) Satabs-prefix-first: ERROR/TIMEOUT[130] 906.47sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.93sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.37sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 18.99sec (x33.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 323.01sec Threader-owicki-gries: ERROR/TIMEOUT[1] 321.32sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 323.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 56.99sec (x101.76) Satabs-prefix-first: ERROR/TIMEOUT[130] 902.78sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 231.89sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.75sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 8.80sec (x15.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.68sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 15.25sec (x27.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 321.96sec Threader-owicki-gries: ERROR/TIMEOUT[1] 321.31sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 322.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 21.23sec (x37.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 321.56sec Threader-owicki-gries: ERROR/TIMEOUT[1] 326.67sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 321.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe015 |
SatAbs: ![]() 1.11sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.88sec (x2.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.67sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.72sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.61sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 2.62sec (x2.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 203.11sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.50sec (x2.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.25sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.64sec (x2.37) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 213.75sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 2.60sec (x2.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.64sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.68sec (x2.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 198.99sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.86sec (x2.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.71sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 125.46sec (x113.02) Satabs-prefix-first: ERROR/TIMEOUT[130] 903.90sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 234.59sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.06sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 125.76sec (x113.29) Satabs-prefix-first: ERROR/TIMEOUT[130] 904.26sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 231.96sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.18sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.21sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 125.49sec (x113.05) Satabs-prefix-first: ERROR/TIMEOUT[130] 903.97sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 235.41sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.38sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 5.67sec (x5.10) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.66sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.64sec (x3.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.43sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.91sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.86sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 122.25sec (x110.13) Satabs-prefix-first: ERROR/TIMEOUT[130] 914.60sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 245.21sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.61sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.54sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe016 |
SatAbs: ![]() 1.90sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 190.01sec Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 2.66sec (x1.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.10sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.75sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 13.35sec (x7.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 212.86sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 13.30sec (x7.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 211.97sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 13.25sec (x6.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 212.71sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 13.08sec (x6.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 212.25sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 13.34sec (x7.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 211.68sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 13.26sec (x6.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 212.62sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 409.92sec (x215.74) Satabs-prefix-first: ERROR/TIMEOUT[130] 917.87sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.48sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.60sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 40.67sec (x21.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.57sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 80.89sec (x42.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 262.16sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.39sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 7.39sec (x3.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.58sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 43.24sec (x22.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.57sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 92.69sec (x48.78) Satabs-prefix-first: ERROR/TIMEOUT[130] 921.64sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 259.69sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.42sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe017 |
SatAbs: ![]() 0.96sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 2.50sec (x2.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 289.82sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.16sec (x2.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 173.78sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.26sec (x2.35) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 174.61sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.18sec (x2.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 174.09sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 11.51sec (x11.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 222.67sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.01sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 11.92sec (x12.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 225.02sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.34sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 11.82sec (x12.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 222.37sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.08sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.12sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 86.46sec (x90.06) Satabs-prefix-first: ERROR/TIMEOUT[130] 914.86sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 266.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.71sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.90sec (x11.35) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 223.22sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.03sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 11.29sec (x11.76) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 222.05sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.15sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 5.93sec (x6.17) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 319.84sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.60sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.18sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 12.51sec (x13.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 231.65sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.39sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 11.25sec (x11.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 221.52sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.24sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe018 |
SatAbs: ![]() 0.65sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 17.39sec (x26.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 229.37sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.06sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.09sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.42sec (x3.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 188.47sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.36sec (x3.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 188.61sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.24sec (x3.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 188.23sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 2.37sec (x3.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 187.87sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.38sec (x3.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 190.19sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.39sec (x3.67) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 188.45sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 64.69sec (x99.52) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.56sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 18.80sec (x28.92) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 285.69sec Threader-owicki-gries: ERROR/TIMEOUT[1] 285.69sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 285.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 28.83sec (x44.35) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 198.39sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 286.03sec Threader-owicki-gries: ERROR/TIMEOUT[1] 281.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 282.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 73.71sec (x113.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.75sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.72sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 19.84sec (x30.52) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 287.43sec Threader-owicki-gries: ERROR/TIMEOUT[1] 289.93sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 283.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 25.22sec (x38.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.09sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 282.44sec Threader-owicki-gries: ERROR/TIMEOUT[1] 281.97sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 284.38sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe019 |
SatAbs: ![]() 2.41sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 187.12sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 9.20sec (x3.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.27sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.35sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 10.71sec (x4.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.20sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 11.32sec (x4.69) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 224.88sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 10.74sec (x4.45) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 225.28sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 11.02sec (x4.57) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 224.55sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 11.04sec (x4.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 225.99sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 10.78sec (x4.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 226.31sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 458.35sec (x190.18) Satabs-prefix-first: ERROR/TIMEOUT[130] 940.79sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.05sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.19sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 57.53sec (x23.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.57sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.08sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 103.95sec (x43.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 221.82sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 331.47sec Threader-owicki-gries: ERROR/TIMEOUT[1] 331.83sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 331.90sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 568.75sec (x235.99) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.45sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 83.43sec (x34.61) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 64.69sec (x26.84) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 233.64sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 333.68sec Threader-owicki-gries: ERROR/TIMEOUT[1] 331.02sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 332.90sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe020 |
SatAbs: ![]() 1.23sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 3.96sec (x3.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 267.04sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.37sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.98sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.08sec |
Cycles
SatAbs: ![]() 2.56sec (x2.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 181.04sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.32sec (x1.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 185.05sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.39sec (x1.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 180.70sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 2.36sec (x1.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 180.42sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.48sec (x2.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 180.73sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.30sec (x1.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 181.58sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 26.19sec (x21.29) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.09sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 280.39sec Threader-owicki-gries: ERROR/TIMEOUT[1] 280.01sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 280.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 25.85sec (x21.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 196.83sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 279.59sec Threader-owicki-gries: ERROR/TIMEOUT[1] 283.79sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 279.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 25.51sec (x20.73) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.07sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 281.86sec Threader-owicki-gries: ERROR/TIMEOUT[1] 280.30sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 281.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 155.61sec (x126.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 287.80sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.89sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.76sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 26.02sec (x21.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 206.68sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 279.56sec Threader-owicki-gries: ERROR/TIMEOUT[1] 281.93sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 280.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 25.15sec (x20.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.70sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 280.89sec Threader-owicki-gries: ERROR/TIMEOUT[1] 280.91sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 281.76sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe021 |
SatAbs: ![]() 1.74sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 2.07sec (x1.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 288.99sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.75sec (x1.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 183.51sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.90sec (x1.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 184.40sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 1.97sec (x1.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 182.99sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 38.25sec (x21.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 261.58sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.22sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.13sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.95sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 4.50sec (x2.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 204.07sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 158.25sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.61sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 12.21sec (x7.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 224.13sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.30sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.12sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.55sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 85.20sec (x48.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 277.21sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.75sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.04sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.64sec (x2.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 203.84sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 161.29sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.01sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 157.84sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.60sec (x2.64) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 204.94sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 157.38sec Threader-owicki-gries: ERROR/TIMEOUT[1] 157.66sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 4.63sec (x2.66) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 303.37sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.66sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.72sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.52sec (x2.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.22sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 158.43sec Threader-owicki-gries: ERROR/TIMEOUT[1] 157.77sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 159.56sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 11.88sec (x6.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 240.03sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.25sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.17sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe022 |
SatAbs: ![]() 0.72sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 9.67sec (x13.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.09sec Threader-owicki-gries: ERROR/TIMEOUT[130] 895.85sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.72sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.60sec (x.83) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.58sec (x.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.62sec (x.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 2.27sec (x3.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 153.20sec Threader-owicki-gries: ERROR/TIMEOUT[1] 154.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 153.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.05sec (x2.84) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 153.49sec Threader-owicki-gries: ERROR/TIMEOUT[1] 152.95sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 152.94sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.11sec (x2.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 155.20sec Threader-owicki-gries: ERROR/TIMEOUT[1] 153.94sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 152.96sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 15.66sec (x21.75) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.80sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.83sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.28sec (x3.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 153.46sec Threader-owicki-gries: ERROR/TIMEOUT[1] 153.61sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 154.78sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.12sec (x2.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 153.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 153.24sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 153.30sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 18.31sec (x25.43) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.18sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.88sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.12sec (x2.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 153.04sec Threader-owicki-gries: ERROR/TIMEOUT[1] 153.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 153.77sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.07sec (x2.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 152.88sec Threader-owicki-gries: ERROR/TIMEOUT[1] 153.38sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 152.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe023 |
SatAbs: ![]() 0.72sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.08sec |
Cycles
SatAbs: ![]() 2.48sec (x3.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 302.03sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.15sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 2.46sec (x3.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 204.93sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.20sec (x3.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.75sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.27sec (x3.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 207.46sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 913.45sec (x1268.68) Satabs-prefix-first: ERROR/TIMEOUT[130] 908.69sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 263.23sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 913.89sec (x1269.29) Satabs-prefix-first: ERROR/TIMEOUT[130] 908.54sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 261.83sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.36sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.97sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 913.78sec (x1269.13) Satabs-prefix-first: ERROR/TIMEOUT[130] 908.48sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 264.87sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 967.22sec (x1343.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 292.83sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.25sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 911.38sec (x1265.80) Satabs-prefix-first: ERROR/TIMEOUT[130] 906.55sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 252.41sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 911.61sec (x1266.12) Satabs-prefix-first: ERROR/TIMEOUT[130] 905.93sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 253.52sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.64sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.33sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 5.43sec (x7.54) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 310.42sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.48sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.47sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 911.72sec (x1266.27) Satabs-prefix-first: ERROR/TIMEOUT[130] 907.28sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 254.41sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.23sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.23sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 911.73sec (x1266.29) Satabs-prefix-first: ERROR/TIMEOUT[130] 906.87sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 252.24sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.54sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe024 |
SatAbs: ![]() 1.92sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 38.55sec (x20.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 272.76sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.24sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.84sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.26sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 3.91sec (x2.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 188.08sec Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 3.94sec (x2.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 188.44sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 3.92sec (x2.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 189.99sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 5.10sec (x2.65) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 196.46sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 161.79sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 4.76sec (x2.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.21sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 159.51sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.51sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 160.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 5.45sec (x2.83) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 198.65sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 161.29sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.32sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 159.50sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 36.49sec (x19.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 228.42sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.23sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.28sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.32sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.79sec (x2.49) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.09sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 159.51sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.87sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 159.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.90sec (x2.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.85sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 159.69sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.41sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 159.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 70.98sec (x36.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 238.24sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.21sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.86sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.85sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.40sec (x2.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 195.77sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 158.29sec Threader-owicki-gries: ERROR/TIMEOUT[1] 160.48sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 159.91sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.40sec (x2.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 198.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 158.74sec Threader-owicki-gries: ERROR/TIMEOUT[1] 159.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 160.21sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe025 |
SatAbs: ![]() 2.07sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.46sec (x1.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.58sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.46sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 2.95sec (x1.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.69sec Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.90sec (x1.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.12sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.79sec (x1.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 191.61sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 2.94sec (x1.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 191.33sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.90sec (x1.40) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 196.25sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.01sec (x1.45) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.39sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 72.83sec (x35.18) Satabs-prefix-first: ERROR/TIMEOUT[130] 903.98sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 238.89sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.32sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.53sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.20sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 72.64sec (x35.09) Satabs-prefix-first: ERROR/TIMEOUT[130] 905.17sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 233.10sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.17sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.31sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 74.46sec (x35.97) Satabs-prefix-first: ERROR/TIMEOUT[130] 904.88sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 233.15sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.25sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.22sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 2.74sec (x1.32) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.40sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.42sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.25sec (x1.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.31sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.27sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.34sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.38sec (x1.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe026 |
SatAbs: ![]() 1.77sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 2.25sec (x1.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 272.79sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.11sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.29sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.42sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.10sec (x1.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 186.94sec Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.06sec (x1.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 186.55sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.28sec (x1.28) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 185.25sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 5.73sec (x3.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 157.45sec Threader-owicki-gries: ERROR/TIMEOUT[1] 155.28sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 156.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 5.67sec (x3.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 157.77sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.28sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 155.86sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 5.64sec (x3.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 156.65sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.28sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 159.67sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 101.41sec (x57.29) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 265.25sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.16sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.49sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.37sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.33sec (x3.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 155.55sec Threader-owicki-gries: ERROR/TIMEOUT[1] 157.04sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 156.90sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.41sec (x3.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 156.62sec Threader-owicki-gries: ERROR/TIMEOUT[1] 157.26sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 157.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 6.47sec (x3.65) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 296.68sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.73sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.64sec (x3.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 157.73sec Threader-owicki-gries: ERROR/TIMEOUT[1] 155.39sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 157.64sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 5.35sec (x3.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 156.76sec Threader-owicki-gries: ERROR/TIMEOUT[1] 157.26sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 156.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe027 |
SatAbs: ![]() 2.55sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 191.73sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 143.87sec (x56.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 275.75sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.96sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.05sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 9.73sec (x3.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.61sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 9.69sec (x3.80) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.93sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.05sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 9.49sec (x3.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 211.85sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.05sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 9.45sec (x3.70) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 214.96sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 9.74sec (x3.81) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 213.68sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 9.65sec (x3.78) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 211.75sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 274.70sec (x107.72) Satabs-prefix-first: ERROR/TIMEOUT[130] 917.83sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.79sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 64.56sec (x25.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 337.73sec Threader-owicki-gries: ERROR/TIMEOUT[1] 336.12sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 336.66sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 65.15sec (x25.54) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 336.20sec Threader-owicki-gries: ERROR/TIMEOUT[1] 338.37sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 337.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 140.17sec (x54.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.14sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.67sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.80sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 56.21sec (x22.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 336.42sec Threader-owicki-gries: ERROR/TIMEOUT[1] 337.21sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 337.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 80.48sec (x31.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 230.10sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 334.51sec Threader-owicki-gries: ERROR/TIMEOUT[1] 336.86sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 334.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe028 |
SatAbs: ![]() 1.91sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 41.62sec (x21.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 254.69sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.62sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.95sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.02sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 2.47sec (x1.29) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.75sec Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.41sec (x1.26) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.45sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.43sec (x1.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 191.46sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 2.26sec (x1.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.19sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.37sec (x1.24) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.72sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.93sec (x1.53) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 193.47sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 34.12sec (x17.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 185.71sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 283.81sec Threader-owicki-gries: ERROR/TIMEOUT[1] 284.63sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 283.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 30.04sec (x15.72) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 187.25sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 284.24sec Threader-owicki-gries: ERROR/TIMEOUT[1] 284.70sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 283.46sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 31.55sec (x16.51) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 184.64sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 285.02sec Threader-owicki-gries: ERROR/TIMEOUT[1] 284.50sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 283.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 19.92sec (x10.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.14sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 284.25sec Threader-owicki-gries: ERROR/TIMEOUT[1] 283.17sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 282.89sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 19.80sec (x10.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 209.60sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 282.96sec Threader-owicki-gries: ERROR/TIMEOUT[1] 283.96sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 285.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 19.34sec (x10.12) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 204.68sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 285.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 284.26sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 283.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe029 |
SatAbs: ![]() 0.47sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 1.58sec (x3.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.64sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.66sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.68sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.56sec (x1.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.41sec (x.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 0.56sec (x1.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 3.36sec (x7.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.66sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.65sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.77sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 4.19sec (x8.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.14sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.27sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.45sec (x7.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.16sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 3.55sec (x7.55) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.57sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.74sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.80sec (x8.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.15sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.10sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.50sec (x7.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.21sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.16sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 1.92sec (x4.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.48sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.19sec (x8.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.41sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.99sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.96sec (x8.42) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.34sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.26sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.81sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe030 |
SatAbs: ![]() 0.87sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ![]() |
Cycles
SatAbs: ![]() 2.69sec (x3.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.54sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.54sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.47sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.01sec (x2.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 193.45sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.04sec (x2.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 190.70sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
Cycles
SatAbs: ![]() 2.06sec (x2.36) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ![]() |
![]() |
Cycles
SatAbs: ![]() 24.75sec (x28.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 298.78sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.57sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.83sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 10.59sec (x12.17) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 211.66sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.43sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 8.94sec (x10.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 209.75sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.47sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 26.86sec (x30.87) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 303.72sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.80sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.71sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 11.72sec (x13.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 210.64sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.39sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.80sec (x12.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 209.10sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.01sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.99sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.44sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 3.66sec (x4.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.79sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.78sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 10.60sec (x12.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 212.43sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.34sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.12sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 8.69sec (x9.98) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 208.98sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.13sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.01sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.22sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe031 |
SatAbs: ![]() 2.06sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 10.19sec (x4.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.71sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.73sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 2.45sec (x1.18) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 196.74sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.40sec (x1.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.07sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.47sec (x1.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 196.83sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 10.99sec (x5.33) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 252.57sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.41sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.54sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 5.03sec (x2.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 246.27sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 158.40sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.14sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 157.13sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 8.88sec (x4.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 215.97sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.44sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.42sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 11.34sec (x5.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 255.12sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.37sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.30sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.60sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.68sec (x2.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 247.21sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 156.49sec Threader-owicki-gries: ERROR/TIMEOUT[1] 155.94sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 156.60sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 8.39sec (x4.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 214.14sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.20sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.20sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 8.31sec (x4.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.68sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.73sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 4.98sec (x2.41) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 244.15sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 156.97sec Threader-owicki-gries: ERROR/TIMEOUT[1] 157.51sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 155.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 8.84sec (x4.29) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 215.42sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.53sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.51sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe032 |
SatAbs: ![]() 1.42sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 20.09sec (x14.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.66sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.67sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.38sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 3.11sec (x2.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.42sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.95sec (x2.07) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 204.31sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 3.14sec (x2.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 205.72sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 65.36sec (x46.02) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 244.34sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.40sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.14sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 64.17sec (x45.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 242.92sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.02sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.25sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 66.49sec (x46.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 246.90sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.46sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.35sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.16sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 66.45sec (x46.79) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 243.04sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.54sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.44sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 65.16sec (x45.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 242.09sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.28sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.17sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.43sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 65.51sec (x46.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 246.89sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.05sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.37sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.28sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 32.80sec (x23.09) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.66sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.60sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 64.86sec (x45.67) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 246.84sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.03sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.49sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 66.55sec (x46.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 242.44sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.45sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.02sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.23sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe033 |
SatAbs: ![]() 0.46sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 1.36sec (x2.95) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.33sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.62sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.51sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 0.58sec (x1.26) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 0.48sec (x1.04) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 0.49sec (x1.06) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 2.17sec (x4.71) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 146.36sec Threader-owicki-gries: ERROR/TIMEOUT[1] 147.71sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 145.96sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 1.95sec (x4.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 145.65sec Threader-owicki-gries: ERROR/TIMEOUT[1] 146.88sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 146.80sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.00sec (x4.34) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 144.93sec Threader-owicki-gries: ERROR/TIMEOUT[1] 147.30sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 147.03sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 1.92sec (x4.17) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 146.30sec Threader-owicki-gries: ERROR/TIMEOUT[1] 146.23sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 146.04sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 1.88sec (x4.08) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 146.14sec Threader-owicki-gries: ERROR/TIMEOUT[1] 146.44sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 146.17sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 1.91sec (x4.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 146.91sec Threader-owicki-gries: ERROR/TIMEOUT[1] 145.97sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 146.40sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 20.18sec (x43.86) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.51sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.70sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.25sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.27sec (x4.93) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 147.66sec Threader-owicki-gries: ERROR/TIMEOUT[1] 146.22sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 146.74sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.06sec (x4.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 145.45sec Threader-owicki-gries: ERROR/TIMEOUT[1] 146.93sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 146.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe034 |
SatAbs: ![]() 0.85sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 10.90sec (x12.82) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 284.97sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.50sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.37sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.31sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 1.87sec (x2.20) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 207.45sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.10sec |
Cycles
SatAbs: ![]() 2.13sec (x2.50) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 232.59sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.11sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.08sec |
Cycles
SatAbs: ![]() 1.96sec (x2.30) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 221.29sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.11sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.08sec |
![]() |
Cycles
SatAbs: ![]() 3.38sec (x3.97) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 214.63sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 169.80sec Threader-owicki-gries: ERROR/TIMEOUT[1] 173.34sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 169.10sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.09sec (x3.63) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 191.61sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 159.97sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.98sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 160.41sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.07sec (x3.61) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 195.70sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 160.87sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.38sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 3.01sec (x3.54) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.39sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 157.32sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.52sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.24sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.93sec (x3.44) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.95sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 157.97sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.36sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.57sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.88sec (x3.38) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.82sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 157.79sec Threader-owicki-gries: ERROR/TIMEOUT[1] 157.51sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.18sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 80.38sec (x94.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 266.86sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.81sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.69sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.34sec (x3.92) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 194.49sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 158.53sec Threader-owicki-gries: ERROR/TIMEOUT[1] 156.66sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.45sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.06sec (x3.60) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 192.41sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 158.49sec Threader-owicki-gries: ERROR/TIMEOUT[1] 158.98sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 158.62sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe035 |
SatAbs: ![]() 2.09sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 6.11sec (x2.92) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 290.76sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.55sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.61sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.11sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.08sec |
Cycles
SatAbs: ![]() 3.65sec (x1.74) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 227.27sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 3.71sec (x1.77) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 211.83sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.08sec |
Cycles
SatAbs: ![]() 3.27sec (x1.56) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 208.52sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 3.08sec (x1.47) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.53sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.32sec (x1.58) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.62sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 3.39sec (x1.62) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 200.74sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 3.33sec (x1.59) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 200.76sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.09sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.09sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.09sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.22sec (x1.54) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.35sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 3.52sec (x1.68) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.11sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ERROR/TIMEOUT[130] 911.50sec (x436.12) Satabs-prefix-first: ERROR/TIMEOUT[130] 902.33sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 277.94sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.64sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.52sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 910.47sec (x435.63) Satabs-prefix-first: ERROR/TIMEOUT[100] 823.17sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 270.09sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.63sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.77sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.53sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ERROR/TIMEOUT[130] 911.36sec (x436.05) Satabs-prefix-first: ERROR/TIMEOUT[100] 809.37sec CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 273.43sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 897.19sec Threader-owicki-gries: ERROR/TIMEOUT[130] 897.19sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.48sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe036 |
SatAbs: ![]() 0.59sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 17.67sec (x29.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.84sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.82sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 896.99sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.09sec |
Cycles
SatAbs: ![]() 0.56sec (x.94) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 0.54sec (x.91) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 0.59sec (x1.00) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 0.68sec (x1.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.57sec (x.96) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 0.62sec (x1.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 0.62sec (x1.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.62sec (x1.05) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.61sec (x1.03) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 0.52sec (x.88) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.60sec (x1.01) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 0.66sec (x1.11) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.07sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
x86/safe037 |
SatAbs: ![]() 1.95sec Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ![]() Checkfence: 0.00sec ESBMC: ![]() Threader-monolithic: ![]() Threader-owicki-gries: ![]() Threader-rely-guarantee: ![]() Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: sc): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 49.37sec (x25.31) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 289.54sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[130] 896.85sec Threader-owicki-gries: ERROR/TIMEOUT[130] 896.92sec Threader-rely-guarantee: ERROR/TIMEOUT[130] 897.29sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
Cycles
SatAbs: ![]() 2.48sec (x1.27) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.89sec Checkfence: 0.01sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.27sec (x1.16) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 196.45sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.06sec |
Cycles
SatAbs: ![]() 2.33sec (x1.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.76sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT MMChecker (MM: csharp): ERROR/TIMEOUT[1] 0.07sec |
![]() |
Cycles
SatAbs: ![]() 2.40sec (x1.23) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.36sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.45sec (x1.25) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 197.85sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
Cycles
SatAbs: ![]() 2.21sec (x1.13) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 200.05sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.06sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT Blender: ![]() |
![]() |
Cycles
SatAbs: ![]() 2.37sec (x1.21) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 200.56sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.23sec (x1.14) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.44sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.07sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.51sec (x1.28) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 201.66sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |
Cycles
SatAbs: ![]() 2.64sec (x1.35) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 199.90sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.06sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.07sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.26sec (x1.15) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 198.11sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.05sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.08sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.06sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
Cycles
SatAbs: ![]() 2.33sec (x1.19) Satabs-prefix-first: ![]() CBMC-WMM: ![]() CBMC-SC: ![]() CImpact: ERROR/TIMEOUT[8] 204.53sec ESBMC: ![]() Threader-monolithic: ERROR/TIMEOUT[1] 0.08sec Threader-owicki-gries: ERROR/TIMEOUT[1] 0.04sec Threader-rely-guarantee: ERROR/TIMEOUT[1] 0.08sec Poirot-Integer: ERROR/TIMEOUT Poirot-BitVector: ERROR/TIMEOUT |
![]() |