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.

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index fb5b6eec876dd57a22feaa25571a1cee9d3f1a3f..8535396e7cef02604b4f0e4b8700faa14564f9d1 100644 (file)
--- 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