Skip to content

Enable Test-Harness Export by Default

Thomas Lemberger requested to merge enable-test-harness-export-by-default into trunk

Enable the test-harness export by default. Avoid confusing log messages about it, and document how to use the test harnesses with a small tutorial.

This MR adds a new example program to doc/examples that uses __assert_fail and __VERIFIER_nondet_int.

Fixes #332 (closed) .

Merge request reports