Use lemma property enum for OutputChannel::lemma (#4755)

There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.

This makes them into a enum.

2 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 7f0e93997..5a50bc99a 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1394,7 +1394,7 @@ void CegInstantiator::presolve( Node q ) {
       lem = NodeManager::currentNM()->mkNode( OR, g, lem );
       Trace("cegqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
       Assert(!expr::hasFreeVar(lem));
-      d_qe->getOutputChannel().lemma( lem, false, true );
+      d_qe->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
     }
   }
 }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b3ea69dbc..84f4bb83b 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -723,7 +723,7 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
       nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
       Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
       Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
-      d_quantEngine->getOutputChannel().lemma(lem, false, true);
+      d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
     }
     return false;
   }else{