This browser is not able to show SVG: try Firefox, Chrome, Safari, or Opera instead.
goto-harness generates a proof harness for a function under test. It constructs functions that set up an appropriate environment before calling function. This is most useful when trying to analyze an isolated unit of a program.