summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_split.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/quant_split.cpp')
-rw-r--r--src/theory/quantifiers/quant_split.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 55fa2a1e5..e6cee778b 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -167,7 +167,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
{
std::vector<Node> vars;
- TypeNode dtjtn = dt[j].getSpecializedConstructorType(tn);
+ TypeNode dtjtn = dt[j].getInstantiatedConstructorType(tn);
Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1);
for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback