diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-19 12:16:42 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-19 12:16:42 -0600 |
| commit | d278cfe019534f8765a9979c3181ae1f8fbc8470 (patch) | |
| tree | c40e959f08829f1c483d0c0ad745332364e2848a /src/theory/quantifiers/ematching/ho_trigger.cpp | |
| parent | 7430455bc71b6641f121edb3ec0cf1706bf40235 (diff) | |
Simplify interface to instantiate (#5926)
Does not support InstMatch interfaces anymore, which are spurious.
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 { |