Counter-examples testing

[saxbophone]

As a form of regression testing, a CMake target which attempts to build test code fragments which should give a compilation error

In CI, we should check that all said targets result in a compilation error if building them is attempted —if any of them build successfully, then this is a build error.

By necessity, we should probably exclude this target from the main build process, and allow building it only if it's requested specifically.