diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-11-27 17:52:36 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-27 17:52:36 -0300 |
| commit | 46eeb6a507c31b4ac65b0ef70c32898667097377 (patch) | |
| tree | 06b34813dd1bc3dcc25479bf4c72ef3252655b77 /src/theory/quantifiers_engine.cpp | |
| parent | bd2793a68e021ab58ab07db0cac67cf3d6806ead (diff) | |
Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8337ba0b0..8730e3a97 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -407,14 +407,15 @@ void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa) // set rewrite engine as owner setOwner(q, d_private->d_rr_engine.get(), 2); } - if (qa.d_sygus) + if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull())) { if (d_private->d_synth_e.get() == nullptr) { Trace("quant-warn") << "WARNING : synth engine is null, and we have : " << q << std::endl; } - // set synth engine as owner + // set synth engine as owner since this is either a conjecture or a function + // definition to be used by sygus setOwner(q, d_private->d_synth_e.get(), 2); } } |