From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Aug 2018 16:15:08 +0000 (-0500)
Subject:  Fix arithmetic division by zero in sygus repair constant module (#2329)
X-Git-Tag: cvc5-1.0.0~4765
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8931c69d4dd1afe689cda92f6a9628898f980f30;p=cvc5.git

 Fix arithmetic division by zero in sygus repair constant module (#2329)
---

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 514f42fb1..75d595a39 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -576,7 +576,10 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
     {
       visited.insert(cur);
       Kind ck = cur.getKind();
-      if (restrictLA && (ck == NONLINEAR_MULT || ck == DIVISION))
+      bool isArithDivKind = (ck == DIVISION_TOTAL || ck == INTS_DIVISION_TOTAL
+                             || ck == INTS_MODULUS_TOTAL);
+      Assert(ck != DIVISION && ck != INTS_DIVISION && ck != INTS_MODULUS);
+      if (restrictLA && (ck == NONLINEAR_MULT || isArithDivKind))
       {
         for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
         {
@@ -584,7 +587,7 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
           std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
           if (itf != d_fo_to_sk.end())
           {
-            if (ck == NONLINEAR_MULT || (ck == DIVISION && j == 1))
+            if (ck == NONLINEAR_MULT || (isArithDivKind && j == 1))
             {
               exvar = itf->second;
               return true;