diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 456f44019..d4926311d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -166,6 +166,13 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, ->toStreamSygus(ss, m_eu); Trace("cegis") << ss.str() << std::endl; } + if (m_eu.isNull()) + { + // A condition enumerator was excluded by symmetry breaking, fail. + // TODO (#2498): either move conditions to getTermList or handle + // partial models in this module. + return false; + } unif_values[index][e].push_back(m_eu); } // inter-enumerator symmetry breaking for return values |