diff options
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index fb5b6eec8..8535396e7 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -427,17 +427,11 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions, // get the presubstitution Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; - std::vector<Node> passertions; - if (options::nlRlvMode() != options::NlRlvMode::NONE) - { - // only keep the relevant assertions (those required for showing input - // is satisfied) - computeRelevantAssertions(assertions, passertions); - } - else - { - passertions = assertions; - } + // Notice that we do not consider relevance here, since assertions were + // already filtered based on relevance. It is incorrect to filter based on + // relevance here, since we may have discarded literals that are relevant + // that are entailed based on the techniques in getAssertions. + std::vector<Node> passertions = assertions; if (options::nlExt()) { // preprocess the assertions with the trancendental solver |