From df2150c721b811a588e5f731b6bc11b236ee3a7e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Aug 2020 14:29:40 -0500 Subject: [PATCH] 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. --- src/theory/arith/nl/nonlinear_extension.cpp | 16 +++++----------- 1 file 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& assertions, // get the presubstitution Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; - std::vector 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 passertions = assertions; if (options::nlExt()) { // preprocess the assertions with the trancendental solver -- 2.30.2