From 52a7602c529108c6e56868c427ac691fe472ff7c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Jul 2018 12:01:02 -0500 Subject: [PATCH] Fix warning in sygus PBE (#2190) --- src/theory/quantifiers/sygus/sygus_pbe.cpp | 6 ++++-- 1 file 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& 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 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 ); } -- 2.30.2