diff options
Diffstat (limited to 'src/theory/arith/nl/iand_solver.cpp')
-rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 3b6c3cbe4..08c85cafe 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -101,7 +101,7 @@ std::vector<NlLemma> IAndSolver::checkInitialRefine() Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE" << std::endl; - lems.emplace_back(lem, Inference::IAND_INIT_REFINE); + lems.emplace_back(lem, InferenceId::NL_IAND_INIT_REFINE); } } return lems; @@ -163,7 +163,7 @@ std::vector<NlLemma> IAndSolver::checkFullRefine() Node lem = valueBasedLemma(i); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; - lems.emplace_back(lem, Inference::IAND_VALUE_REFINE); + lems.emplace_back(lem, InferenceId::NL_IAND_VALUE_REFINE); } } } |