Unit tests need clean up

[delcypher]

This was motivated by #1159 . Prior to this I had never looked very closely at Z3's unit tests. Doing so has revealed several problems that need addressing.

• The tests seem rely on SASSERT(). That's a no-op in non debug builds, right? That doesn't seem like a great idea because that means we don't know if the checks actually pass on a release build.
• src/test/hashtable.cpp seems to redefine SASSERT() and that implementation isn't particularly good because it doesn't halt execution with a non zero exit code which means we'll easily miss any failures here.
• Several of the tests have #ifdef _WINDOWS (e.g. src/test/api.cpp) guarding them with no obvious reason why. This means lots of things won't get tested on TravisCI because that uses Linux.

While I'm here I've also observed that we seem to be using a "homegrown" unit testing framework. I would suggest that part of the solution here is to use a well tested and widely used unit testing framework rather than rolling our own.

Example C++ unit testing frameworks include

• GoogleTest I've used this one. It's also used by LLVM.
• Boost.test
• Catch

My preference would be GoogleTest but that's only because it's the only C++ unit test framework I've used before. Other suggestions are welcome.

[NikolajBjorner]

some of this is actionable, but I am not sure how valuable each of these is. I am replacing SASSERT by ENSURE to ensure checks are exercised within all modes.
If you want to get rid of windows guards you are welcome to add a pull request, but this is super low priority from what I am concerned, the spew of issues that are added every day outpaces the cycles I have to address such things. For test frameworks, they are probably good, but unless there is a tangible reason for using them, I would spend all cycles elsewhere.

[wintersteiger]

I agree with @NikolajBjorner; it's not worth the effort. Those test cases are used infrequently and in early stages of some new features, but then they never change or throw any errors. It's been years since I saw it throw an actual error. I think the real functional (and performance) tests are pretty much all in SMT2 files these days.

We don't have many good tests that exercise the various APIs though (see z3test/regressions/* for * in {c++, cs, python} + a huge bag of largely unsorted files on my desktop...). Getting a solution that makes it easy to turn GitHub issues into API test cases would be super useful!

[delcypher]

For test frameworks, they are probably good, but unless there is a tangible reason for using them, I would spend all cycles elsewhere.
I agree with @NikolajBjorner; it's not worth the effort. Those test cases are used infrequently and in early stages of some new features, but then they never change or throw any errors. It's been years since I saw it throw an actual error. I think the real functional (and performance) tests are pretty much all in SMT2 files these days.

Okay. Fair points. My thoughts regarding using a unit test framework was to make it much easier to write unit tests. Given that neither of you seem that keen on the unit tests I won't waste time porting the existing ones to a new framework.

I'll keep this issue open though as I'd like port the existing tests to non-windows platforms if I get the time at some point.