diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-08-04 12:28:12 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-04 10:28:12 -0500 |
| commit | 5f89c684f95f16bdb5953fc543a36115093f1982 (patch) | |
| tree | b483a793b10e3cc147b4629a0eda3933140ca4f2 /src/smt | |
| parent | 81544bb6de5b21db7ed5e41d56277105bbea103d (diff) | |
[proof] Add getProof to API and use it in GetProofCommand (#6974)
Also adds a call to get proof in a unit test.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/command.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 36bc17096..342931912 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1993,7 +1993,7 @@ void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - d_result = solver->getSmtEngine()->getProof(); + d_result = solver->getProof(); d_commandStatus = CommandSuccess::instance(); } catch (api::CVC5ApiRecoverableException& e) |