diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index ad45fb9b7..2e7f0cc02 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -78,7 +78,8 @@ bool Cegis::processInitialize(Node n, // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj) // for each i,j. We do not do this and revert to the default behavior of // this module instead. - bool isVarAgnostic = options::sygusEnumVarAgnostic() && csize == 1; + bool isActiveGen = + options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1; // initialize an enumerator for each candidate for (unsigned i = 0; i < csize; i++) { @@ -101,9 +102,9 @@ bool Cegis::processInitialize(Node n, d_tds->registerEnumerator(candidates[i], candidates[i], d_parent, - isVarAgnostic, + isActiveGen, do_repair_const, - isVarAgnostic); + isActiveGen); } return true; } |