+CDSChecker can also check boolean assertions in your test programs. Just
+include <model-assert.h> and use the MODEL_ASSERT() macro in your test program.
+CDSChecker will report a bug in any possible execution in which the argument to
+MODEL_ASSERT() evaluates to false (that is, 0).
+