Fix sygus quantifier elimination preprocess for multiple functions (#5130)

The option --sygus-qe-preproc performs quantifier elimination to coerce certain synthesis conjectures to be single invocation. This technique was broken when multiple synthesis functions were present. This fixes the issue and adds a regression where --sygus-qe-preproc enables a benchmark to be quickly solved.

1 files changed, 7 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 95f1acb25..5358a0aff 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -184,13 +184,19 @@ void SynthEngine::assignConjecture(Node q)
       for (unsigned i = 0, size = all_vars.size(); i < size; i++)
       {
         Node v = all_vars[i];
-        if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
+        if (std::find(funcs0.begin(), funcs0.end(), v) != funcs0.end())
+        {
+          Trace("cegqi-qep") << "- fun var: " << v << std::endl;
+        }
+        else if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
         {
           qe_vars.push_back(v);
+          Trace("cegqi-qep") << "- qe var: " << v << std::endl;
         }
         else
         {
           nqe_vars.push_back(v);
+          Trace("cegqi-qep") << "- non qe var: " << v << std::endl;
         }
       }
       std::vector<Node> orig;