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 514f42fb1b76832e16a4f7a212bfe0d6e445c9a9..75d595a39b546f49403f1454c375f868aef6670f 100644 (file)
--- 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;