summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ematching/trigger.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ematching/trigger.cpp')
-rw-r--r--src/theory/quantifiers/ematching/trigger.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index ac43d3bc9..8d9cfd3a3 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -143,7 +143,7 @@ uint64_t Trigger::addInstantiations()
bool Trigger::sendInstantiation(InstMatch& m)
{
- return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
+ return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals);
}
bool Trigger::mkTriggerTerms(Node q,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback