diff options
| -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; |