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
Also, I don't really know how to understand SMTCOMP results outside of a crude 'league table'. I am using the solvers in incremental mode and do know what my theory is - QF_BV with a very light usage of UF in a earlier, less CPU-hogging phase of my code.
In the end you always have to try the solvers yourself on your specific problem.. So outputting SMTLIB2 code is the way to go IMO. When your algorithm does 1000s of fast small queries then going through SMTLIB2 can be a huge overhead, but for a few hard queries it's best imo.
Well, I've taken the stupid route, I guess, but after a uninspiring day of filling in a Really Big Pile of Pure Virtual Functions (yes, today I truly am the boolector_saddo) I'll be able to find out. My problem with the few hard queries approach is that my overheads are ...
very much a combination of "hey, the top 200 problems you gave me were kinda hard" and "whoa, really, 800,000 different CEGIS runs, are you fucking kidding me?". So a solver that absolutely slays on the hard stuff would be nice but I also need to be sure the easy stuff is fast.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
