Skip to content

Commit 2107223

Browse files
Add witness output to goto-checker interfaces
1 parent 1968915 commit 2107223

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/goto-checker/goto_checker.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,11 @@ class goto_checkert
5959
/// This builds and returns the counterexample
6060
virtual goto_tracet build_error_trace() const = 0;
6161

62+
/// This outputs an error witness
63+
virtual void output_error_witness(const goto_tracet &) = 0;
64+
/// This outputs an proof
65+
virtual void output_proof() = 0;
66+
6267
protected:
6368
goto_checkert(const optionst &, ui_message_handlert &);
6469

0 commit comments

Comments
 (0)