Exit when counter-example is found

Open serras opened this issue 3 years ago • 2 comments

In a perfect world we would like to finish the search for a counter-example in Pirouette once one is found. However, due to the intricate coupling between the IO part and the breadth-first search, more work is being done that it should be right now.

May 25 '22 14:05 serras

Given we now have a pure SMT interface, I'd be curious to know if we get to stop on the first counter-example now.

Jun 17 '22 08:06 VictorCMiraldo

With #115 this should be the case: the Data.Foldable.find should stop once the first one is found.

Jun 24 '22 08:06 serras