summaryrefslogtreecommitdiff
path: root/src/theory/rep_set.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r--src/theory/rep_set.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index f44b269cf..d0eee1886 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -69,7 +69,7 @@ const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const
namespace {
-bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
+bool containsStoreAll(Node n, std::unordered_set<Node>& cache)
{
if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
cache.insert(n);
@@ -91,7 +91,7 @@ bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
void RepSet::add( TypeNode tn, Node n ){
//for now, do not add array constants FIXME
if( tn.isArray() ){
- std::unordered_set<Node, NodeHashFunction> cache;
+ std::unordered_set<Node> cache;
if( containsStoreAll( n, cache ) ){
return;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback