summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_pools.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_pools.cpp')
-rw-r--r--src/theory/quantifiers/term_pools.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp
index 43eec9499..aa0fbd06d 100644
--- a/src/theory/quantifiers/term_pools.cpp
+++ b/src/theory/quantifiers/term_pools.cpp
@@ -81,6 +81,7 @@ void TermPools::registerPool(Node p, const std::vector<Node>& initValue)
d.initialize();
for (const Node& i : initValue)
{
+ Assert(i.getType().isComparableTo(p.getType().getSetElementType()));
d.add(i);
}
}
@@ -156,4 +157,4 @@ void TermPools::processInternal(Node q,
} // namespace quantifiers
} // namespace theory
-} // namespace CVC4
+} // namespace cvc5
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback