diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-17 11:15:08 -0500 |
|---|---|---|
| committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-08-17 11:15:08 -0500 |
| commit | 8931c69d4dd1afe689cda92f6a9628898f980f30 (patch) | |
| tree | 24d91e8d57c8f18f5075d0a108cd2646fbe461d3 | |
| parent | 29ae7d5ec0a73b90529e2200d948e6f4051099f1 (diff) | |
Fix arithmetic division by zero in sygus repair constant module (#2329)
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 7 |
1 files 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<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; |