Do not use relevance during non-linear check model (#4938)

This led to a model soundness issue in rare cases where a relevant literal was dropped due to an entailment check by an irrelevant literal.

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