diff options
Diffstat (limited to 'src/expr/bound_var_manager.cpp')
| -rw-r--r-- | src/expr/bound_var_manager.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp index 820c82d22..53c87fb97 100644 --- a/src/expr/bound_var_manager.cpp +++ b/src/expr/bound_var_manager.cpp @@ -18,6 +18,8 @@ #include "expr/node_manager_attributes.h" #include "util/rational.h" +using namespace cvc5::kind; + namespace cvc5 { BoundVarManager::BoundVarManager() : d_keepCacheVals(false) {} @@ -51,7 +53,7 @@ Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2, size_t i) Node BoundVarManager::getCacheValue(size_t i) { - return NodeManager::currentNM()->mkConst(Rational(i)); + return NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(i)); } Node BoundVarManager::getCacheValue(TNode cv, size_t i) |