From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 24 Aug 2020 19:29:40 +0000 (-0500)
Subject: Do not use relevance during non-linear check model (#4938)
X-Git-Tag: cvc5-1.0.0~2960
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=df2150c721b811a588e5f731b6bc11b236ee3a7e;p=cvc5.git

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 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