diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-23 12:01:02 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-23 12:01:02 -0500 |
commit | 52a7602c529108c6e56868c427ac691fe472ff7c (patch) | |
tree | 0c7974347145d6a9057246443023eb5c060d5c3f /src/theory | |
parent | 17d0499e11cc40e795a1a13ffa7b24f585372d9e (diff) |
Fix warning in sygus PBE (#2190)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 1a8721530..56d2cf2b5 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -430,11 +430,13 @@ bool CegConjecturePbe::constructCandidates(const std::vector<Node>& enums, // set by options::sygusPbeMultiFairDiff(). If d is zero, then our // enumeration is such that all terms of T1 or T2 of size n are considered // before any term of size n+1. + int diffAllow = options::sygusPbeMultiFairDiff(); std::vector<unsigned> enum_consider; for (unsigned i = 0, esize = enums.size(); i < esize; i++) { - if (!options::sygusPbeMultiFair() - || szs[i] - min_term_size <= options::sygusPbeMultiFairDiff()) + Assert(szs[i] >= min_term_size); + int diff = szs[i] - min_term_size; + if (!options::sygusPbeMultiFair() || diff <= diffAllow) { enum_consider.push_back( i ); } |