From 28d0b471fff550582364bb72906cdc0efcde817e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 27 Jun 2025 19:48:51 -0700 Subject: [PATCH] following the review comments --- src/math/lp/nla_order_lemmas.cpp | 1 - src/math/lp/nla_types.h | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 252bbecd3..81714f697 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -10,7 +10,6 @@ #include "math/lp/nla_core.h" #include "math/lp/nla_common.h" #include "math/lp/factorization_factory_imp.h" -#include "util/trail.h" namespace nla { diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h index c300d72c1..401e4eb62 100644 --- a/src/math/lp/nla_types.h +++ b/src/math/lp/nla_types.h @@ -66,8 +66,8 @@ namespace nla { class core; // // lemmas are created in a scope. - // when the destructor of new_lemma is invoked - // all constraints are assumed added to the lemma + // when the destructor of lemma_builder is invoked + // all constraints are assumed already added to the current_lemma // correctness of the lemma can be checked at this point. // class lemma_builder {