From 46eeb6a507c31b4ac65b0ef70c32898667097377 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 27 Nov 2019 17:52:36 -0300 Subject: Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502) --- src/theory/quantifiers_engine.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers_engine.cpp') 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); } } -- cgit v1.2.3