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 fd6eedc5a..3b6c3cbe4 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.push_back(lem); + lems.emplace_back(lem, Inference::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.push_back(lem); + lems.emplace_back(lem, Inference::IAND_VALUE_REFINE); } } } |