diff options
Diffstat (limited to 'src/expr/bound_var_manager.h')
| -rw-r--r-- | src/expr/bound_var_manager.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index 3330decff..b619a36e2 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -98,7 +98,7 @@ class BoundVarManager /** Whether we keep cache values */ bool d_keepCacheVals; /** The set of cache values we have used */ - std::unordered_set<Node, NodeHashFunction> d_cacheVals; + std::unordered_set<Node> d_cacheVals; }; } // namespace cvc5 |