From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Jul 2018 17:01:02 +0000 (-0500)
Subject: Fix warning in sygus PBE (#2190)
X-Git-Tag: cvc5-1.0.0~4878
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52a7602c529108c6e56868c427ac691fe472ff7c;p=cvc5.git

Fix warning in sygus PBE (#2190)
---

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 );
       }