Hangs whilst proving

[zeskeertwee]

Hi!
It would probably be a nice (and quite simple to implement) to run the proof on a seperate thread (maybe even in parallel for the different proofs!) so that the UI does not hang.
I would love to implement this if you agree it would be useful!

[alegnani]

Hi and thank you for your issue!
At the moment I don't have much time so I can't really work on this.
The feature would definitely be useful and I would greatly appreciate a pull request. :)

[zeskeertwee]

I've implemented it on my fork, but i couldn't manage to compile it, as it complains about a missing z3.h, and when i point it to the correct place for it it complains about a missing stdbool.h. I'm fairly sure it should work, but i haven't been able to test it.

[alegnani]

Sorry for getting back so late to you and thank you for the contribution.

Not sure why it should not work on your machine; you might be missing something from the c tool-chain. You can try compiling the whole project with the build_z3 feature flag which builds z3 locally. Beware that this takes quite a considerable amount of time.

I tried compiling your code but there appear to be quite a lot errors due to multiple borrows etc. I will look into it in the next couple of days.