diff options
Diffstat (limited to 'src/theory/quantifiers/ematching/ho_trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 4c606a273..875c74aa4 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -368,7 +368,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) else { // do not run higher-order matching - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals); } } @@ -381,7 +381,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index) if (var_index == d_ho_var_list.size()) { // we now have an instantiation to try - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals); } else { |