diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-11 15:36:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-11 13:36:38 -0700 |
| commit | 1339e2a3b884d34a9c27eb45bb6847a493fe0365 (patch) | |
| tree | eee01493ebe789c8c1b09e5f977273c360a52bc7 /src/theory/quantifiers/quant_util.cpp | |
| parent | 1c859fd0f43fa2081bdb247423e81d9174a5f474 (diff) | |
Remove instantiation model true option (#4861)
This was an option that rejected instantiations that are true according to the current
model's equality engine.
This option was never helpful and will be burdensome to maintain with new updates
to equality engine infrastructure.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index a8eda10bb..cb1207912 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -32,7 +32,7 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const { - return d_quantEngine->getActiveEqualityEngine(); + return d_quantEngine->getMasterEqualityEngine(); } bool QuantifiersModule::areEqual(TNode n1, TNode n2) const |