diff options
| author | anwu1219 <haozewu@stanford.edu> | 2018-09-25 10:58:08 -0700 |
|---|---|---|
| committer | anwu1219 <haozewu@stanford.edu> | 2018-09-25 10:58:08 -0700 |
| commit | 5590206f1f6f1bff5a68fee071fc236c86af53e1 (patch) | |
| tree | bb7faa96099fa8b55b1b1143e884fa0bf0d64329 /src/theory/quantifiers/sygus/cegis_unif.cpp | |
| parent | fa85f7665365c4eeaaa0d84284718239f1d059c4 (diff) | |
| parent | f4ce78488ae41b4effc140edfc35cbba79d2dcd4 (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4
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 |