Skip to content
This repository has been archived by the owner on Oct 5, 2023. It is now read-only.

Exit when counter-example is found #97

Open
serras opened this issue May 25, 2022 · 2 comments
Open

Exit when counter-example is found #97

serras opened this issue May 25, 2022 · 2 comments

Comments

@serras
Copy link
Contributor

serras commented May 25, 2022

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.
@VictorCMiraldo VictorCMiraldo mentioned this issue May 29, 2022
Merged
@VictorCMiraldo
Copy link
Contributor

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.

@serras
Copy link
Contributor Author

serras commented Jun 24, 2022

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

@VictorCMiraldo VictorCMiraldo changed the title In dev: exit when counter-example is found Exit when counter-example is found Jun 29, 2022
@VictorCMiraldo VictorCMiraldo mentioned this issue Jun 30, 2022
Closed
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@serras @VictorCMiraldo