diff options
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
| -rw-r--r-- | src/theory/quantifiers/instantiate.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 42bff316a..9b410dd08 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -100,8 +100,8 @@ class InstLemmaList */ class Instantiate : public QuantifiersUtil { - using NodeInstListMap = context:: - CDHashMap<Node, std::shared_ptr<InstLemmaList>, NodeHashFunction>; + using NodeInstListMap = + context::CDHashMap<Node, std::shared_ptr<InstLemmaList>>; public: Instantiate(QuantifiersState& qs, @@ -352,7 +352,7 @@ class Instantiate : public QuantifiersUtil * The list of quantified formulas for which the domain of d_c_inst_match_trie * is valid. */ - context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom; + context::CDHashSet<Node> d_c_inst_match_trie_dom; /** * A CDProof storing instantiation steps. */ |