diff options
Diffstat (limited to 'src/theory/arith/nl/iand_solver.cpp')
| -rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index ff51f7bb5..78ffb3c09 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -99,7 +99,7 @@ void IAndSolver::checkInitialRefine() Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE" << std::endl; - d_im.addPendingArithLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE); + d_im.addPendingLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE); } } } @@ -152,7 +152,7 @@ void IAndSolver::checkFullRefine() << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl; // note that lemma can contain div/mod, and will be preprocessed in the // prop engine - d_im.addPendingArithLemma( + d_im.addPendingLemma( lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true); } else if (options::iandMode() == options::IandMode::BITWISE) @@ -162,7 +162,7 @@ void IAndSolver::checkFullRefine() << "IAndSolver::Lemma: " << lem << " ; BITWISE_REFINE" << std::endl; // note that lemma can contain div/mod, and will be preprocessed in the // prop engine - d_im.addPendingArithLemma( + d_im.addPendingLemma( lem, InferenceId::ARITH_NL_IAND_BITWISE_REFINE, nullptr, true); } else @@ -172,11 +172,11 @@ void IAndSolver::checkFullRefine() Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; // value lemmas should not contain div/mod so we don't need to tag it with PREPROCESS - d_im.addPendingArithLemma(lem, - InferenceId::ARITH_NL_IAND_VALUE_REFINE, - nullptr, - true, - LemmaProperty::NONE); + d_im.addPendingLemma(lem, + InferenceId::ARITH_NL_IAND_VALUE_REFINE, + nullptr, + true, + LemmaProperty::NONE); } } } |