summaryrefslogtreecommitdiff
path: root/src/proof/method_id.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/method_id.cpp')
-rw-r--r--src/proof/method_id.cpp5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp
index c5e8458cd..9567590a8 100644
--- a/src/proof/method_id.cpp
+++ b/src/proof/method_id.cpp
@@ -18,6 +18,8 @@
#include "proof/proof_checker.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
const char* toString(MethodId id)
@@ -49,7 +51,8 @@ std::ostream& operator<<(std::ostream& out, MethodId id)
Node mkMethodId(MethodId id)
{
- return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
+ return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ Rational(static_cast<uint32_t>(id)));
}
bool getMethodId(TNode n, MethodId& i)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback