diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-17 17:52:40 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-17 17:52:40 -0600 |
| commit | c30f459b03572907b06f839535ac4694c0c37b0d (patch) | |
| tree | 4112cd96e30928f4b57787eabe98a0aaa178540e /src/smt/smt_engine.h | |
| parent | 8d89e06c34a0a22e006a74d48d4cc8843b293f73 (diff) | |
| parent | f411ca8ce97f488fd0db0a79abe8b4e61521ae69 (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 9655297b3..0781ac1c0 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -249,6 +249,11 @@ class CVC4_PUBLIC SmtEngine { smt::SmtEnginePrivate* d_private; /** + * Check that a generated Proof (via getProof()) checks. + */ + void checkProof(); + + /** * Check that a generated Model (via getModel()) actually satisfies * all user assertions. */ |