Slides for my talk are now available here: https://alastairreid.github.io/papers/oopsla2017-whoguardstheguards-slides.pdf …https://twitter.com/alastair_d_reid/status/923434747753242625 …
-
-
Replying to @alastair_d_reid
I'm always amazed to read that Z3 works fine for your stuff. For the things I am doing it's far to slow, I can only use Yices and Boolector.
3 replies 0 retweets 3 likes -
Replying to @oe1cxw @alastair_d_reid
Could be an issue with the way you encode your problems (non-optimal for Z3)? You might want to have a chat with the Z3 devs about this.
1 reply 0 retweets 0 likes -
Replying to @TerminateThread @alastair_d_reid
Maybe, but smtcomp results for Z3 don't look good either for the logics I am using (QF_AUFBV and subsets of that).
2 replies 0 retweets 0 likes
I can share benchmarks if anyone is interested. So far I've only reported Z3 issues for stuff where Z3 is even slower than usual.
4:33 AM - 27 Oct 2017
0 replies
0 retweets
0 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.