summaryrefslogtreecommitdiff
path: root/src/theory/theory_model.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r--src/theory/theory_model.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index ab66e8fe7..951a62cae 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -398,7 +398,7 @@ class TheoryModel
/** are we using model cores? */
bool d_using_model_core;
/** symbols that are in the model core */
- std::unordered_set<Node, NodeHashFunction> d_model_core;
+ std::unordered_set<Node> d_model_core;
/** Get model value function.
*
* This function is a helper function for getValue.
@@ -414,7 +414,7 @@ class TheoryModel
virtual void addTermInternal(TNode n);
private:
/** cache for getModelValue */
- mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
+ mutable std::unordered_map<Node, Node> d_modelCache;
//---------------------------- separation logic
/** the value of the heap */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback