From 8931c69d4dd1afe689cda92f6a9628898f980f30 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Aug 2018 11:15:08 -0500 Subject: [PATCH] Fix arithmetic division by zero in sygus repair constant module (#2329) --- src/theory/quantifiers/sygus/sygus_repair_const.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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::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; -- 2.30.2