diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-29 19:52:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-30 00:52:48 +0000 |
| commit | 7e5fe049ad88405a90fd5a43caa872d646d4b8e2 (patch) | |
| tree | 2fe225b29e2721c8d5237f0628e2a393a001bc99 /src/theory/quantifiers/quantifiers_modules.cpp | |
| parent | ef31c2518c194029a913fe2872e2040d2f5e4294 (diff) | |
Miscellaneous elimination of dependencies on quantifiers engine (#6238)
This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_modules.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_modules.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 0c8c9399b..a45029074 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -111,7 +111,7 @@ void QuantifiersModules::initialize(QuantifiersEngine* qe, // full saturation : instantiate from relevant domain, then arbitrary terms if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { - d_rel_dom.reset(new RelevantDomain(qe, qr)); + d_rel_dom.reset(new RelevantDomain(qs, qr, tr)); d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, tr, d_rel_dom.get())); modules.push_back(d_fs.get()); } |