diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-01 14:55:19 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-01 14:55:19 -0600 |
commit | c48548ea68b6241bee2cb9393ef2710c5803fb06 (patch) | |
tree | 044b335f3ea83baef89207c49c0cd5da227ecaa8 /src/theory/quantifiers/fmf | |
parent | eac7249ef4e35ad8c37f36098c228965f71a319b (diff) |
Eliminate PREPROCESS lemma property (#5827)
This is now possible since we always preprocess lemmas.
Note that the LemmaProperty on inferences may be redundant throughout the non-linear solver now.
Diffstat (limited to 'src/theory/quantifiers/fmf')
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 0f17bb04a..9144bca2a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -725,7 +725,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, LemmaProperty::PREPROCESS); + d_quantEngine->getOutputChannel().lemma(lem); } return false; }else{ |