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 …
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.
-
-
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.
-
Maybe, but smtcomp results for Z3 don't look good either for the logics I am using (QF_AUFBV and subsets of that).
- Show replies
New conversation -
-
-
Boolector has a "non commercial only" license.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
When I was working with some AUFBV formulas from Klee last semester, yices2 to was normally about 10x faster than Z3.
-
Thanks. I should try yices. Tried boolector some years ago but license limits me to older version of boolector.
- Show replies
New conversation -
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.