Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930)

This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.

This addresses CVC4/cvc4-projects#113.

Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:

QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.

Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.

20 files changed, 183 insertions, 86 deletions

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 23ced4d8f..ab33f123c 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -534,6 +534,24 @@ header = "options/arith_options.h"
   help       = "whether to increment the precision for irrational function constraints"
 
 [[option]]
+  name       = "nlRlvMode"
+  category   = "regular"
+  long       = "nl-rlv=MODE"
+  type       = "NlRlvMode"
+  default    = "NONE"
+  help       = "choose mode for using relevance of assertoins in non-linear arithmetic"
+  help_mode  = "Modes for using relevance of assertoins in non-linear arithmetic."
+[[option.mode.NONE]]
+  name = "none"
+  help = "Do not use relevance."
+[[option.mode.INTERLEAVE]]
+  name = "interleave"
+  help = "Alternate rounds using relevance."
+[[option.mode.ALWAYS]]
+  name = "always"
+  help = "Always use relevance."
+  
+[[option]]
   name       = "brabTest"
   category   = "regular"
   long       = "arith-brab"
diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml
index 84c994c3f..6ec9d8854 100644
--- a/src/options/theory_options.toml
+++ b/src/options/theory_options.toml
@@ -34,3 +34,11 @@ header = "options/theory_options.h"
   default    = "true"
   read_only  = true
   help       = "condense values for functions in models rather than explicitly representing them"
+
+[[option]]
+  name       = "relevanceFilter"
+  category   = "regular"
+  long       = "relevance-filter"
+  type       = "bool"
+  default    = "false"
+  help       = "enable analysis of relevance of asserted literals with respect to the input formula"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 5376d7418..7d2427015 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1307,6 +1307,22 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
+  if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+      && options::nlRlvMode() != options::NlRlvMode::NONE)
+  {
+    if (!options::relevanceFilter())
+    {
+      if (options::relevanceFilter.wasSetByUser())
+      {
+        Warning() << "SmtEngine: turning on relevance filtering to support "
+                     "--nl-ext-rlv="
+                  << options::nlRlvMode() << std::endl;
+      }
+      // must use relevance filtering techniques
+      options::relevanceFilter.set(true);
+    }
+  }
+
   // For now, these array theory optimizations do not support model-building
   if (options::produceModels() || options::produceAssignments()
       || options::checkModels())
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index daa36f972..cc10d6659 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/node_algorithm.h"
 #include "options/arith_options.h"
+#include "options/theory_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/rewriter.h"
@@ -279,11 +280,6 @@ bool NlModel::checkModel(const std::vector<Node>& assertions,
   std::vector<Node> check_assertions;
   for (const Node& a : assertions)
   {
-    // don't have to check tautological literals
-    if (d_tautology.find(a) != d_tautology.end())
-    {
-      continue;
-    }
     if (d_check_model_solved.find(a) == d_check_model_solved.end())
     {
       Node av = a;
@@ -455,52 +451,6 @@ void NlModel::setUsedApproximate() { d_used_approx = true; }
 
 bool NlModel::usedApproximate() const { return d_used_approx; }
 
-void NlModel::addTautology(Node n)
-{
-  // ensure rewritten
-  n = Rewriter::rewrite(n);
-  std::unordered_set<TNode, TNodeHashFunction> visited;
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(n);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    if (visited.find(cur) == visited.end())
-    {
-      visited.insert(cur);
-      if (cur.getKind() == AND)
-      {
-        // children of AND are also implied
-        for (const Node& cn : cur)
-        {
-          visit.push_back(cn);
-        }
-      }
-      else
-      {
-        // is this an arithmetic literal?
-        Node atom = cur.getKind() == NOT ? cur[0] : cur;
-        if ((atom.getKind() == EQUAL && atom[0].getType().isReal())
-            || atom.getKind() == LEQ)
-        {
-          // Add to tautological literals if it does not contain
-          // non-linear multiplication. We cannot consider literals
-          // with non-linear multiplication to be tautological since this
-          // model object is responsible for checking whether they hold.
-          // (TODO, cvc4-projects #113: revisit this).
-          if (!expr::hasSubtermKind(NONLINEAR_MULT, atom))
-          {
-            Trace("nl-taut") << "Tautological literal: " << atom << std::endl;
-            d_tautology.insert(cur);
-          }
-        }
-      }
-    }
-  } while (!visit.empty());
-}
-
 bool NlModel::solveEqualitySimple(Node eq,
                                   unsigned d,
                                   std::vector<NlLemma>& lemmas)
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index 1e6f6c8f3..dcbd9cce7 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -166,22 +166,6 @@ class NlModel
   void setUsedApproximate();
   /** Did we use an approximation during this check? */
   bool usedApproximate() const;
-  /**
-   * This states that formula n is a tautology (satisfied in all models).
-   * We call this on internally generated lemmas. This method computes a
-   * set of literals that are implied by n, that are hence tautological
-   * as well, such as:
-   *   l_pi <= real.pi <= u_pi (pi approximations)
-   *   sin(x) = -1*sin(-x)
-   * where these literals are internally generated for the purposes
-   * of guiding the models of the linear solver.
-   *
-   * TODO (cvc4-projects #113: would be helpful if we could do this even
-   * more aggressively by ignoring all internally generated literals.
-   *
-   * Tautological literals do not need be checked during checkModel.
-   */
-  void addTautology(Node n);
   //------------------------------ end recording model substitutions and bounds
 
   /**
@@ -334,8 +318,6 @@ class NlModel
   std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved;
   /** did we use an approximation on this call to last-call effort? */
   bool d_used_approx;
-  /** the set of all tautological literals */
-  std::unordered_set<Node, NodeHashFunction> d_tautology;
 }; /* class NlModel */
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 9dbb95d93..fb5b6eec8 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -38,6 +38,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_containing(containing),
       d_ee(ee),
       d_needsLastCall(false),
+      d_checkCounter(0),
       d_extTheory(&containing),
       d_model(containing.getSatContext()),
       d_trSlv(d_model),
@@ -182,8 +183,6 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
       d_lemmas.insert(lem);
     }
     d_stats.d_inferences << nlem.d_id;
-    // also indicate this is a tautology
-    d_model.addTautology(lem);
   }
 }
 
@@ -192,6 +191,22 @@ void NonlinearExtension::processSideEffect(const NlLemma& se)
   d_trSlv.processSideEffect(se);
 }
 
+void NonlinearExtension::computeRelevantAssertions(
+    const std::vector<Node>& assertions, std::vector<Node>& keep)
+{
+  Trace("nl-ext-rlv") << "Compute relevant assertions..." << std::endl;
+  Valuation v = d_containing.getValuation();
+  for (const Node& a : assertions)
+  {
+    if (v.isRelevant(a))
+    {
+      keep.push_back(a);
+    }
+  }
+  Trace("nl-ext-rlv") << "...keep " << keep.size() << "/" << assertions.size()
+                      << " assertions" << std::endl;
+}
+
 unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
 {
   Trace("nl-ext-lemma-debug")
@@ -251,6 +266,16 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
 void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
 {
   Trace("nl-ext") << "Getting assertions..." << std::endl;
+  bool useRelevance = false;
+  if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE)
+  {
+    useRelevance = (d_checkCounter % 2);
+  }
+  else if (options::nlRlvMode() == options::NlRlvMode::ALWAYS)
+  {
+    useRelevance = true;
+  }
+  Valuation v = d_containing.getValuation();
   NodeManager* nm = NodeManager::currentNM();
   // get the assertions
   std::map<Node, Rational> init_bounds[2];
@@ -264,6 +289,11 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
     nassertions++;
     const Assertion& assertion = *it;
     Node lit = assertion.d_assertion;
+    if (useRelevance && !v.isRelevant(lit))
+    {
+      // not relevant, skip
+      continue;
+    }
     init_assertions.insert(lit);
     // check for concrete bounds
     bool pol = lit.getKind() != NOT;
@@ -390,7 +420,6 @@ std::vector<Node> NonlinearExtension::checkModelEval(
 }
 
 bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
-                                    const std::vector<Node>& false_asserts,
                                     std::vector<NlLemma>& lemmas,
                                     std::vector<Node>& gs)
 {
@@ -398,7 +427,17 @@ 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 = assertions;
+  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;
+  }
   if (options::nlExt())
   {
     // preprocess the assertions with the trancendental solver
@@ -681,6 +720,7 @@ void NonlinearExtension::check(Theory::Effort e)
 bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
 {
   ++(d_stats.d_mbrRuns);
+  d_checkCounter++;
 
   // get the assertions
   std::vector<Node> assertions;
@@ -786,7 +826,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
       // error bounds on the Taylor approximation of transcendental functions.
       std::vector<NlLemma> lemmas;
       std::vector<Node> gs;
-      if (checkModel(assertions, false_asserts, lemmas, gs))
+      if (checkModel(assertions, lemmas, gs))
       {
         complete_status = 1;
       }
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 6fb8dbbfa..ee58a9e2e 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -254,11 +254,12 @@ class NonlinearExtension
    * ensureLiteral respectively.
    */
   bool checkModel(const std::vector<Node>& assertions,
-                  const std::vector<Node>& false_asserts,
                   std::vector<NlLemma>& lemmas,
                   std::vector<Node>& gs);
   //---------------------------end check model
-
+  /** compute relevant assertions */
+  void computeRelevantAssertions(const std::vector<Node>& assertions,
+                                 std::vector<Node>& keep);
   /**
    * Potentially adds lemmas to the set out and clears lemmas. Returns
    * the number of lemmas added to out. We do not add lemmas that have already
@@ -293,6 +294,11 @@ class NonlinearExtension
   NlStats d_stats;
   // needs last call effort
   bool d_needsLastCall;
+  /**
+   * The number of times we have the called main check method
+   * (modelBasedRefinement). This counter is used for interleaving strategies.
+   */
+  unsigned d_checkCounter;
   /** Extended theory, responsible for context-dependent simplification. */
   ExtTheory d_extTheory;
   /** The non-linear model object
diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp
index 9fe973569..c918438ee 100644
--- a/src/theory/output_channel.cpp
+++ b/src/theory/output_channel.cpp
@@ -49,6 +49,10 @@ bool isLemmaPropertySendAtoms(LemmaProperty p)
 {
   return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE;
 }
+bool isLemmaPropertyNeedsJustify(LemmaProperty p)
+{
+  return (p & LemmaProperty::NEEDS_JUSTIFY) != LemmaProperty::NONE;
+}
 
 std::ostream& operator<<(std::ostream& out, LemmaProperty p)
 {
@@ -71,6 +75,10 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p)
     {
       out << " SEND_ATOMS";
     }
+    if (isLemmaPropertyNeedsJustify(p))
+    {
+      out << " NEEDS_JUSTIFY";
+    }
     out << " }";
   }
   return out;
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index d65d4fc53..0fd610c58 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -42,7 +42,9 @@ enum class LemmaProperty : uint32_t
   // whether the lemma needs preprocessing
   PREPROCESS = 2,
   // whether the processing of the lemma should send atoms to the caller
-  SEND_ATOMS = 4
+  SEND_ATOMS = 4,
+  // whether the lemma is part of the justification for answering "sat"
+  NEEDS_JUSTIFY = 8
 };
 /** Define operator lhs | rhs */
 LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs);
@@ -58,6 +60,8 @@ bool isLemmaPropertyRemovable(LemmaProperty p);
 bool isLemmaPropertyPreprocess(LemmaProperty p);
 /** is the send atoms bit set on p? */
 bool isLemmaPropertySendAtoms(LemmaProperty p);
+/** is the needs justify bit set on p? */
+bool isLemmaPropertyNeedsJustify(LemmaProperty p);
 
 /**
  * Writes an lemma property name to a stream.
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9fdf7e7aa..9dc483f93 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -962,7 +962,8 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
         Trace("quantifiers-sk-debug")
             << "Skolemize lemma : " << slem << std::endl;
       }
-      getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
+      getOutputChannel().lemma(
+          lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY);
     }
     return;
   }
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index a8ebd921a..dce038fbf 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -374,8 +374,12 @@ void InferenceManager::doPendingLemmas()
         d_termReg.registerTermAtomic(n, sks.first);
       }
     }
-
-    d_out.lemma(lem);
+    LemmaProperty p = LemmaProperty::NONE;
+    if (ii.d_id == Inference::REDUCTION)
+    {
+      p |= LemmaProperty::NEEDS_JUSTIFY;
+    }
+    d_out.lemma(lem, p);
   }
   // process the pending require phase calls
   for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7431b26e4..f0966a96d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -47,6 +47,7 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/relevance_manager.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_model.h"
@@ -152,6 +153,12 @@ void TheoryEngine::finishInit() {
         d_userContext, "DefaultModel", options::assignFunctionValues());
     d_aloc_curr_model = true;
   }
+  // create the relevance filter if any option requires it
+  if (options::relevanceFilter())
+  {
+    d_relManager.reset(
+        new RelevanceManager(d_userContext, theory::Valuation(this)));
+  }
 
   //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
   if( d_curr_model_builder==NULL ){
@@ -201,6 +208,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_eeDistributed(nullptr),
       d_quantEngine(nullptr),
       d_decManager(new DecisionManager(userContext)),
+      d_relManager(nullptr),
       d_curr_model(nullptr),
       d_aloc_curr_model(false),
       d_curr_model_builder(nullptr),
@@ -456,6 +464,12 @@ void TheoryEngine::check(Theory::Effort effort) {
     // If in full effort, we have a fake new assertion just to jumpstart the checking
     if (Theory::fullEffort(effort)) {
       d_factsAsserted = true;
+      // Reset round for the relevance manager, which notice only sets a flag
+      // to indicate that its information must be recomputed.
+      if (d_relManager != nullptr)
+      {
+        d_relManager->resetRound();
+      }
     }
 
     // Check until done
@@ -938,6 +952,16 @@ void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
   CVC4_FOR_EACH_THEORY;
 }
 
+bool TheoryEngine::isRelevant(Node lit) const
+{
+  if (d_relManager != nullptr)
+  {
+    return d_relManager->isRelevant(lit);
+  }
+  // otherwise must assume its relevant
+  return true;
+}
+
 void TheoryEngine::shutdown() {
   // Set this first; if a Theory shutdown() throws an exception,
   // at least the destruction of the TheoryEngine won't confound
@@ -998,6 +1022,10 @@ void TheoryEngine::notifyPreprocessedAssertions(
       theoryOf(theoryId)->ppNotifyAssertions(assertions);
     }
   }
+  if (d_relManager != nullptr)
+  {
+    d_relManager->notifyPreprocessedAssertions(assertions);
+  }
 }
 
 bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
@@ -1659,6 +1687,14 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
     lemmas.push_back(newLemmas[i].getNode());
   }
 
+  // If specified, we must add this lemma to the set of those that need to be
+  // justified, where note we pass all auxiliary lemmas in lemmas, since these
+  // by extension must be justified as well.
+  if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
+  {
+    d_relManager->notifyPreprocessedAssertions(lemmas.ref());
+  }
+
   // assert lemmas to prop engine
   for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
   {
@@ -1999,6 +2035,11 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
           it != it_end;
           ++it) {
         Node assertion = (*it).d_assertion;
+        if (!isRelevant(assertion))
+        {
+          // not relevant, skip
+          continue;
+        }
         Node val = getModel()->getValue(assertion);
         if (val != d_true)
         {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 91984daca..549f4078e 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -35,7 +35,6 @@
 #include "prop/prop_engine.h"
 #include "smt/command.h"
 #include "theory/atom_requests.h"
-#include "theory/decision_manager.h"
 #include "theory/engine_output_channel.h"
 #include "theory/interrupted.h"
 #include "theory/rewriter.h"
@@ -92,6 +91,9 @@ namespace theory {
   class TheoryEngineModelBuilder;
   class EqEngineManagerDistributed;
 
+  class DecisionManager;
+  class RelevanceManager;
+
   namespace eq {
     class EqualityEngine;
   }/* CVC4::theory::eq namespace */
@@ -165,6 +167,8 @@ class TheoryEngine {
    * The decision manager
    */
   std::unique_ptr<theory::DecisionManager> d_decManager;
+  /** The relevance manager */
+  std::unique_ptr<theory::RelevanceManager> d_relManager;
 
   /**
    * Default model object
@@ -498,6 +502,12 @@ public:
   inline bool needCheck() const {
     return d_outputChannelUsed || d_lemmasAdded;
   }
+  /**
+   * Is the literal lit (possibly) critical for satisfying the input formula in
+   * the current context? This call is applicable only during collectModelInfo
+   * or during LAST_CALL effort.
+   */
+  bool isRelevant(Node lit) const;
 
   /**
    * This is called at shutdown time by the SmtEngine, just before
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 1a2b9220a..9375a4868 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -172,5 +172,7 @@ bool Valuation::needCheck() const{
   return d_engine->needCheck();
 }
 
+bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); }
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index d8d57d2e5..35d990715 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -156,7 +156,13 @@ public:
 
   /** need check ? */
   bool needCheck() const;
-  
+
+  /**
+   * Is the literal lit (possibly) critical for satisfying the input formula in
+   * the current context? This call is applicable only during collectModelInfo
+   * or during LAST_CALL effort.
+   */
+  bool isRelevant(Node lit) const;
 };/* class Valuation */
 
 }/* CVC4::theory namespace */
diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
index d01d7b7d2..eaefbe651 100644
--- a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
+++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
@@ -1,2 +1,3 @@
+% COMMAND-LINE: --nl-rlv=none
 % EXPECT: entailed
 QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ;
diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2
index 0fc0f55f9..6c66d2e4c 100644
--- a/test/regress/regress1/nl/issue3647.smt2
+++ b/test/regress/regress1/nl/issue3647.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models --produce-models --decision=internal
+; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/sin1-deq-sat.smt2 b/test/regress/regress1/nl/sin1-deq-sat.smt2
index d9e12c7b4..4fb0732a3 100644
--- a/test/regress/regress1/nl/sin1-deq-sat.smt2
+++ b/test/regress/regress1/nl/sin1-deq-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
+; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2
index d2a21fa60..9c1d9cef6 100644
--- a/test/regress/regress1/nl/sin1-sat.smt2
+++ b/test/regress/regress1/nl/sin1-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
+; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)
diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2
index e7b7547c4..2fc1a6115 100644
--- a/test/regress/regress1/sygus/issue3648.smt2
+++ b/test/regress/regress1/sygus/issue3648.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models
+; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always
 (set-logic ALL)
 (declare-fun a () Real)
 (assert (> a 0.000001))