summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/single_inv_partition.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/single_inv_partition.h')
-rw-r--r--src/theory/quantifiers/single_inv_partition.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h
index 0a4af3185..cdc56d1f0 100644
--- a/src/theory/quantifiers/single_inv_partition.h
+++ b/src/theory/quantifiers/single_inv_partition.h
@@ -201,7 +201,7 @@ class SingleInvocationPartition
std::vector<Node> d_si_vars;
/** every free variable of conjuncts[2] */
- std::vector<Node> d_all_vars;
+ std::unordered_set<Node, NodeHashFunction> d_all_vars;
/** map from functions to first-order variables that anti-skolemized them */
std::map<Node, Node> d_func_fo_var;
/** map from first-order variables to the function it anti-skolemized */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback