Comment author: @gasche

Clearly the most beautiful bug this month -- for now.

Comment author: @garrigue

Using ocaml 4.06.1, the search seems to go on forever.
What version did you use?

Comment author: @Octachron

I tested on 4.07.0, where it only takes few seconds to fail on the second refutation clause.

Comment author: @garrigue

For the second clause, it indeed produces a counter example.
My question was for the first clause. How long does it take to be accepted without warning?
For me on MacOS, it just goes on forever, so the bug does not appear.

Comment author: @garrigue

Sorry. Indeed on 4.07.0, and on the 4.07 branch the first clause succeeds pretty fast too.
However on 4.06.0 it goes on forever, whereas the allowed number of existentials is supposed to be lower.
Mystery in the search.

Comment author: @Octachron

On 4.06.1, it takes me ~ 10 minutes to find a counter-example for the first refutable clause. I have another example with a 3×4 board where it only takes ~ 30 seconds to find a counter-example with 4.06.1 (whereas 4.07 still fail to find it). Should I upload it?

Comment author: @garrigue

For there record:

there_are_no_wazir_tours (Right::Right::Up::Up::Left::Down::Left::Up::Left::Down::Down::Down:: Right::Right::Right::[]);;
Exception: Match_failure ("//toplevel//", 1, 59).

Turning it into a segfault should be easy (using the result type).

Comment author: @garrigue

There is now a GPR fixing that.
Please review :)

#1951

Fixed by #1997.
Unfortunately, the search takes so long that we cannot add this to the test suite.