diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-01-08 13:38:24 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-08 13:38:24 -0300 |
| commit | 2958e98eff88ce14aefcdeee3c6ec579fcc2bb1d (patch) | |
| tree | af304364b3fdd8f98663b4dcfb2d2632719f0ee2 /src/api | |
| parent | 63d27f031f8942607d869080d0e2cfb6078d40b1 (diff) | |
[proof-new] Implementing getProof in the API and SMT engine (#5751)
A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 49974d30d..621e3c1c0 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2473,7 +2473,7 @@ Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const << "Cannot get specialized constructor type for non-datatype type " << retSort; CVC4_API_SOLVER_TRY_CATCH_BEGIN; - + NodeManager* nm = d_solver->getNodeManager(); Node ret = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, |