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
When I was working with some AUFBV formulas from Klee last semester, yices2 to was normally about 10x faster than Z3.
1 reply 0 retweets 2 likes -
Replying to @ElectronicKiwi @oe1cxw
Thanks. I should try yices. Tried boolector some years ago but license limits me to older version of boolector.
2 replies 0 retweets 1 like -
Replying to @alastair_d_reid @oe1cxw
you need quantifiers though, right? I think yices2 only supports QF.
1 reply 0 retweets 1 like
Replying to @ElectronicKiwi @alastair_d_reid
Yices has support for exist-forall problems. Boolector can do no quantifiers at all afaik.
2:39 PM - 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.