You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
So far my experience is Yices >> Z3 as far as QF_BV is concerned, although my Z3 prototype used a lot of stuff I didn't really need (integers and arrays). I'll give Z3 a shot in the new framework, but I really built it to use Boolector, which sounds like the bee's knees.
In my experience Yices >> Z3 and Boolector >> Z3. Yices vs Boolector is a bit more difficult. I'd say Boolector has the better SAT engine but Yices has better theories. For most pure QF_BV my expectation would be that Boolector performs slightly better.
Regarding API, did you have a look at PySMT? It's a unified python API for various SMT solvers, including Z3, Yices, and Boolector.https://github.com/pysmt/pysmt
I looked at that, but I need C++. I'm doing a lot of heavyweight processing of the instruction graphs before they hit the SMT solver, and (a) Python is slow and (b) igraph makes me want to gouge my eyes out. Although BGL is like working with someone's semi-dormant thesis on ...
Crossing my fingers for more than slightly... Maybe SMTCOMP19 isn't the Final Word on things but it looks a good deal like Boolector did considerably better on QF_BV - and the most competitive Yices results seem to have had a bit of tweaking in terms of what SAT was used.
Are you running incremental queries or single-shot? My expectation is that for single shot QF_BV queries Boolector > Yices and for incremental problems its maybe about even, depending on the details of the SMT problem.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
