increase timeout for Z3 for one hard-to-prove obligation

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities

Other

1.29k stars 200 forks source link

increase timeout for Z3 for one hard-to-prove obligation #73

Closed damiendoligez closed 1 year ago

damiendoligez commented 1 year ago

Fixes one part of #67 : the failure on Bakery.tla.

muenchnerkindl commented 1 year ago

Sure, go ahead. I find it just a little strange because on my machine this obligation is checked very quickly (using tlapm-1.5.0):

@!!BEGIN @!!type:obligation @!!id:2 @!!loc:398:5:398:7 @!!status:proved @!!prover:z3 @!!meth:time-limit: 5; time-used: 0.5 (10%) @!!already:false @!!END