Perform theory widening eagerly (#4044)

Fixes #3971 and fixes #3991. In incremental mode, the logic can change from one
(check-sat) call to another. In the reported issue, we start with QF_NIA
but then switch to QF_UFNIA because there is a div term (which has a UF in
its expanded form). Dealing with this issue is challenging in general. As a
result, we have decided not to allow theory widening in
Theory::expandDefinitions() anymore but instead to do it eagerly in
SmtEngine::setDefaults().

26 files changed, 239 insertions, 95 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index fd98064e3..d1eed0748 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -509,23 +509,25 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     }
   }
 
+  /////////////////////////////////////////////////////////////////////////////
+  // Theory widening
+  //
+  // Some theories imply the use of other theories to handle certain operators,
+  // e.g. UF to handle partial functions.
+  /////////////////////////////////////////////////////////////////////////////
+  bool needsUf = false;
   // strings require LIA, UF; widen the logic
   if (logic.isTheoryEnabled(THEORY_STRINGS))
   {
     LogicInfo log(logic.getUnlockedCopy());
     // Strings requires arith for length constraints, and also UF
-    if (!logic.isTheoryEnabled(THEORY_UF))
-    {
-      Trace("smt") << "because strings are enabled, also enabling UF"
-                   << std::endl;
-      log.enableTheory(THEORY_UF);
-    }
+    needsUf = true;
     if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()
         || !logic.areIntegersUsed())
     {
-      Trace("smt") << "because strings are enabled, also enabling linear "
-                      "integer arithmetic"
-                   << std::endl;
+      Notice()
+          << "Enabling linear integer arithmetic because strings are enabled"
+          << std::endl;
       log.enableTheory(THEORY_ARITH);
       log.enableIntegers();
       log.arithOnlyLinear();
@@ -533,21 +535,34 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     logic = log;
     logic.lock();
   }
-  if (logic.isTheoryEnabled(THEORY_ARRAYS)
+  if (needsUf
+      // Arrays, datatypes and sets permit Boolean terms and thus require UF
+      || logic.isTheoryEnabled(THEORY_ARRAYS)
       || logic.isTheoryEnabled(THEORY_DATATYPES)
-      || logic.isTheoryEnabled(THEORY_SETS))
+      || logic.isTheoryEnabled(THEORY_SETS)
+      // Non-linear arithmetic requires UF to deal with division/mod because
+      // their expansion introduces UFs for the division/mod-by-zero case.
+      || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())
+      // If division/mod-by-zero is not treated as a constant value in BV, we
+      // need UF.
+      || (logic.isTheoryEnabled(THEORY_BV)
+          && !options::bitvectorDivByZeroConst())
+      // FP requires UF since there are multiple operators that are partially
+      // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more
+      // details).
+      || logic.isTheoryEnabled(THEORY_FP))
   {
     if (!logic.isTheoryEnabled(THEORY_UF))
     {
       LogicInfo log(logic.getUnlockedCopy());
-      Trace("smt") << "because a theory that permits Boolean terms is enabled, "
-                      "also enabling UF"
-                   << std::endl;
+      Notice() << "Enabling UF because " << logic << " requires it."
+               << std::endl;
       log.enableTheory(THEORY_UF);
       logic = log;
       logic.lock();
     }
   }
+  /////////////////////////////////////////////////////////////////////////////
 
   // by default, symmetry breaker is on only for non-incremental QF_UF
   if (!options::ufSymmetryBreaker.wasSetByUser())
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3ac719eed..dee3365fb 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1588,8 +1588,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
         theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
 
         Assert(t != NULL);
-        LogicRequest req(d_smt);
-        node = t->expandDefinition(req, n);
+        node = t->expandDefinition(n);
       }
 
       // the partial functions can fall through, in which case we still
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e4aeca980..cdb6c77f3 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -63,8 +63,9 @@ void TheoryArith::preRegisterTerm(TNode n){
   d_internal->preRegisterTerm(n);
 }
 
-Node TheoryArith::expandDefinition(LogicRequest &logicRequest, Node node) {
-  return d_internal->expandDefinition(logicRequest, node);
+Node TheoryArith::expandDefinition(Node node)
+{
+  return d_internal->expandDefinition(node);
 }
 
 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index a16f1ed5e..f15db32a1 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -58,7 +58,7 @@ public:
    */
   void preRegisterTerm(TNode n) override;
 
-  Node expandDefinition(LogicRequest& logicRequest, Node node) override;
+  Node expandDefinition(Node node) override;
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index bed59baf5..374de8562 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -5061,8 +5061,8 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
   return d_rowTracking[ridx];
 }
 
-
-Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) {
+Node TheoryArithPrivate::expandDefinition(Node node)
+{
   NodeManager* nm = NodeManager::currentNM();
 
   // eliminate here since the rewritten form of these may introduce division
@@ -5082,8 +5082,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
-        Node divByZeroNum =
-            getArithSkolemApp(logicRequest, num, ArithSkolemId::DIV_BY_ZERO);
+        Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret);
       }
@@ -5098,8 +5097,8 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
-        Node intDivByZeroNum = getArithSkolemApp(
-            logicRequest, num, ArithSkolemId::INT_DIV_BY_ZERO);
+        Node intDivByZeroNum =
+            getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret);
       }
@@ -5114,8 +5113,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
-        Node modZeroNum =
-            getArithSkolemApp(logicRequest, num, ArithSkolemId::MOD_BY_ZERO);
+        Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret);
       }
@@ -5147,8 +5145,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
         Node lem;
         if (k == kind::SQRT)
         {
-          Node skolemApp =
-              getArithSkolemApp(logicRequest, node[0], ArithSkolemId::SQRT);
+          Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
           Node uf = skolemApp.eqNode(var);
           Node nonNeg = nm->mkNode(
               kind::AND, nm->mkNode(kind::MULT, var, var).eqNode(node[0]), uf);
@@ -5219,8 +5216,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
   Unreachable();
 }
 
-Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest,
-                                        ArithSkolemId asi)
+Node TheoryArithPrivate::getArithSkolem(ArithSkolemId asi)
 {
   std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
   if (it == d_arith_skolem.end())
@@ -5268,7 +5264,6 @@ Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest,
                             nm->mkFunctionType(tn, tn),
                             desc,
                             NodeManager::SKOLEM_EXACT_NAME);
-      logicRequest.widenLogic(THEORY_UF);
     }
     d_arith_skolem[asi] = skolem;
     return skolem;
@@ -5276,11 +5271,9 @@ Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest,
   return it->second;
 }
 
-Node TheoryArithPrivate::getArithSkolemApp(LogicRequest& logicRequest,
-                                           Node n,
-                                           ArithSkolemId asi)
+Node TheoryArithPrivate::getArithSkolemApp(Node n, ArithSkolemId asi)
 {
-  Node skolem = getArithSkolem(logicRequest, asi);
+  Node skolem = getArithSkolem(asi);
   if (!options::arithNoPartialFun())
   {
     skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index a4469f3b5..b5debe76d 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -432,7 +432,7 @@ public:
    * Does non-context dependent setup for a node connected to a theory.
    */
   void preRegisterTerm(TNode n);
-  Node expandDefinition(LogicRequest &logicRequest, Node node);
+  Node expandDefinition(Node node);
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
@@ -860,10 +860,9 @@ private:
   /** get arithmetic skolem
    *
    * Returns the Skolem in the above map for the given id, creating it if it
-   * does not already exist. If a Skolem function is created, the logic is
-   * widened to include UF.
+   * does not already exist.
    */
-  Node getArithSkolem(LogicRequest& logicRequest, ArithSkolemId asi);
+  Node getArithSkolem(ArithSkolemId asi);
   /** get arithmetic skolem application
    *
    * By default, this returns the term f( n ), where f is the Skolem function
@@ -872,7 +871,7 @@ private:
    * If the option arithNoPartialFun is enabled, this returns f, where f is
    * the Skolem constant for the identifier asi.
    */
-  Node getArithSkolemApp(LogicRequest& logicRequest, Node n, ArithSkolemId asi);
+  Node getArithSkolemApp(Node n, ArithSkolemId asi);
 
   /**
    *  Maps for Skolems for to-integer, real/integer div-by-k, and inverse
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 94fc1e34c..32791415e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -194,7 +194,8 @@ void TheoryBV::finishInit()
   tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
 }
 
-Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
+Node TheoryBV::expandDefinition(Node node)
+{
   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 
   switch (node.getKind()) {
@@ -221,7 +222,6 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
     Node divByZero = getBVDivByZero(node.getKind(), width);
     Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
     node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
-    logicRequest.widenLogic(THEORY_UF);
     return node;
   }
     break;
@@ -234,7 +234,6 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
   Unreachable();
 }
 
-
 void TheoryBV::preRegisterTerm(TNode node) {
   d_calledPreregister = true;
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index bc54a09e7..7f88d8388 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -79,7 +79,7 @@ public:
 
   void finishInit() override;
 
-  Node expandDefinition(LogicRequest& logicRequest, Node node) override;
+  Node expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode n) override;
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index b3244fe91..9c8e9e2fa 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -558,7 +558,8 @@ void TheoryDatatypes::finishInit() {
   }
 }
 
-Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
+Node TheoryDatatypes::expandDefinition(Node n)
+{
   NodeManager* nm = NodeManager::currentNM();
   switch (n.getKind())
   {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index cc54241d0..c6ffb8907 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -302,7 +302,7 @@ private:
   bool needsCheckLastEffort() override;
   void preRegisterTerm(TNode n) override;
   void finishInit() override;
-  Node expandDefinition(LogicRequest& logicRequest, Node n) override;
+  Node expandDefinition(Node n) override;
   Node ppRewrite(TNode n) override;
   void presolve() override;
   void addSharedTerm(TNode t) override;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index b028184cd..68f3ad35a 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -318,17 +318,6 @@ Node TheoryFp::toRealUF(Node node) {
   return nm->mkNode(kind::APPLY_UF, fun, node[0]);
 }
 
-void TheoryFp::enableUF(LogicRequest &lr)
-{
-  if (!this->d_expansionRequested) {
-    // Needed for conversions to/from real and min/max
-    lr.widenLogic(THEORY_UF);
-    // THEORY_BV has to be enabled when the logic is set
-    this->d_expansionRequested = true;
-  }
-  return;
-}
-
 Node TheoryFp::abstractRealToFloat(Node node)
 {
   Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
@@ -393,7 +382,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
   return uf;
 }
 
-Node TheoryFp::expandDefinition(LogicRequest &lr, Node node)
+Node TheoryFp::expandDefinition(Node node)
 {
   Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
                                << std::endl;
@@ -404,17 +393,14 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node)
     res = removeToFPGeneric::removeToFPGeneric(node);
 
   } else if (node.getKind() == kind::FLOATINGPOINT_MIN) {
-    enableUF(lr);
     res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MIN_TOTAL,
                                            node[0], node[1], minUF(node));
 
   } else if (node.getKind() == kind::FLOATINGPOINT_MAX) {
-    enableUF(lr);
     res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MAX_TOTAL,
                                            node[0], node[1], maxUF(node));
 
   } else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) {
-    enableUF(lr);
     FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
     FloatingPointToUBVTotal newInfo(info);
 
@@ -424,7 +410,6 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node)
             toUBVUF(node));
 
   } else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) {
-    enableUF(lr);
     FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
     FloatingPointToSBVTotal newInfo(info);
 
@@ -434,7 +419,6 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node)
             toSBVUF(node));
 
   } else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL) {
-    enableUF(lr);
     res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
                                            node[0], toRealUF(node));
 
@@ -442,13 +426,6 @@ Node TheoryFp::expandDefinition(LogicRequest &lr, Node node)
     // Do nothing
   }
 
-  // We will need to enable UF to abstract these in ppRewrite
-  if (res.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL
-      || res.getKind() == kind::FLOATINGPOINT_TO_FP_REAL)
-  {
-    enableUF(lr);
-  }
-
   if (res != node) {
     Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
                                  << " rewritten to " << res << std::endl;
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index ae4a2a1cb..de629b000 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -41,7 +41,7 @@ class TheoryFp : public Theory {
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
-  Node expandDefinition(LogicRequest& lr, Node node) override;
+  Node expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode node) override;
   void addSharedTerm(TNode node) override;
@@ -105,9 +105,6 @@ class TheoryFp : public Theory {
   context::CDO<bool> d_conflict;
   context::CDO<Node> d_conflictNode;
 
-  /** Uninterpretted functions for partially defined functions. **/
-  void enableUF(LogicRequest& lr);
-
   typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>
       ComparisonUFMap;
 
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index f4b265d98..8430987f2 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -95,7 +95,8 @@ void TheorySets::preRegisterTerm(TNode node) {
   d_internal->preRegisterTerm(node);
 }
 
-Node TheorySets::expandDefinition(LogicRequest &logicRequest, Node n) {
+Node TheorySets::expandDefinition(Node n)
+{
   Kind nk = n.getKind();
   if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
       || nk == COMPREHENSION)
@@ -118,7 +119,7 @@ Node TheorySets::expandDefinition(LogicRequest &logicRequest, Node n) {
       throw LogicException(ss.str());
     }
   }
-  return d_internal->expandDefinition(logicRequest, n);
+  return d_internal->expandDefinition(n);
 }
 
 Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 5fc1a61a3..1bb515cc6 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -55,7 +55,7 @@ class TheorySets : public Theory
   Node getModelValue(TNode) override;
   std::string identify() const override { return "THEORY_SETS"; }
   void preRegisterTerm(TNode node) override;
-  Node expandDefinition(LogicRequest& logicRequest, Node n) override;
+  Node expandDefinition(Node n) override;
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
   void presolve() override;
   void propagate(Effort) override;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index b949be76c..e3db6887b 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1485,7 +1485,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
   }
 }
 
-Node TheorySetsPrivate::expandDefinition(LogicRequest& logicRequest, Node n)
+Node TheorySetsPrivate::expandDefinition(Node n)
 {
   Debug("sets-proc") << "expandDefinition : " << n << std::endl;
   return n;
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index ab9071793..84cea99a1 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -209,7 +209,7 @@ class TheorySetsPrivate {
    * Another option to fix this is to make TheoryModel::getValue more general
    * so that it makes theory-specific calls to evaluate interpreted symbols.
    */
-  Node expandDefinition(LogicRequest &logicRequest, Node n);
+  Node expandDefinition(Node n);
 
   Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index da8c3583d..609822fe1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -640,7 +640,8 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   }
 }
 
-Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
+Node TheoryStrings::expandDefinition(Node node)
+{
   Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
 
   if (node.getKind() == STRING_FROM_CODE)
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 84e0a0a00..453e4eca9 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -293,7 +293,7 @@ private:
   /** preregister term */
   void preRegisterTerm(TNode n) override;
   /** Expand definition */
-  Node expandDefinition(LogicRequest& logicRequest, Node n) override;
+  Node expandDefinition(Node n) override;
   /** Check at effort e */
   void check(Effort e) override;
   /** needs check last effort */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index a6751e1ec..c777f164f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -424,22 +424,21 @@ public:
   virtual void finishInit() { }
 
   /**
-   * Some theories have kinds that are effectively definitions and
-   * should be expanded before they are handled.  Definitions allow
-   * a much wider range of actions than the normal forms given by the
-   * rewriter; they can enable other theories and create new terms.
-   * However no assumptions can be made about subterms having been
-   * expanded or rewritten.  Where possible rewrite rules should be
-   * used, definitions should only be used when rewrites are not
-   * possible, for example in handling under-specified operations
-   * using partially defined functions.
+   * Some theories have kinds that are effectively definitions and should be
+   * expanded before they are handled.  Definitions allow a much wider range of
+   * actions than the normal forms given by the rewriter. However no
+   * assumptions can be made about subterms having been expanded or rewritten.
+   * Where possible rewrite rules should be used, definitions should only be
+   * used when rewrites are not possible, for example in handling
+   * under-specified operations using partially defined functions.
    *
    * Some theories like sets use expandDefinition as a "context
    * independent preRegisterTerm".  This is required for cases where
    * a theory wants to be notified about a term before preprocessing
    * and simplification but doesn't necessarily want to rewrite it.
    */
-  virtual Node expandDefinition(LogicRequest &logicRequest, Node node) {
+  virtual Node expandDefinition(Node node)
+  {
     // by default, do nothing
     return node;
   }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 809ef5139..9c631ca60 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -587,7 +587,7 @@ class TheoryEngine {
    * @param assertion the normalized assertion being sent
    * @param originalAssertion the actual assertion that was sent
    * @param toTheoryId the theory that is on the receiving end
-   * @param fromTheoryId the theory that sent the assertino
+   * @param fromTheoryId the theory that sent the assertion
    * @return true if a new assertion, false if theory already got it
    */
   bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index 260bec418..2a061b017 100644
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -20,6 +20,7 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId)
     case THEORY_FP: out << "THEORY_FP"; break;
     case THEORY_ARRAYS: out << "THEORY_ARRAYS"; break;
     case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break;
+    case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break;
     case THEORY_SEP: out << "THEORY_SEP"; break;
     case THEORY_SETS: out << "THEORY_SETS"; break;
     case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3b42fa6a1..1098d42ce 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -201,7 +201,8 @@ unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) {
   return node.getKind()==kind::APPLY_UF ? 0 : 1;
 }
 
-Node TheoryUF::expandDefinition(LogicRequest &logicRequest, Node node) {
+Node TheoryUF::expandDefinition(Node node)
+{
   Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : "
                       << node << std::endl;
   if( node.getKind()==kind::HO_APPLY ){
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 50b7a65cb..8627eb3f0 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -195,7 +195,7 @@ private:
   void finishInit() override;
 
   void check(Effort) override;
-  Node expandDefinition(LogicRequest& logicRequest, Node node) override;
+  Node expandDefinition(Node node) override;
   void preRegisterTerm(TNode term) override;
   Node explain(TNode n) override;
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1f3d4f623..649178f91 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -582,6 +582,8 @@ set(regress_0_tests
   regress0/nl/issue3719.smt2
   regress0/nl/issue3729-cm-solved-tf.smt2
   regress0/nl/issue3959.smt2
+  regress0/nl/issue3971.smt2
+  regress0/nl/issue3991.smt2
   regress0/nl/issue4007-rint-uf.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
diff --git a/test/regress/regress0/nl/issue3971.smt2 b/test/regress/regress0/nl/issue3971.smt2
new file mode 100644
index 000000000..93d370659
--- /dev/null
+++ b/test/regress/regress0/nl/issue3971.smt2
@@ -0,0 +1,145 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const i4 Int)
+(declare-const i5 Int)
+(declare-const i6 Int)
+(declare-const i7 Int)
+(declare-const i8 Int)
+(declare-const i9 Int)
+(declare-const i12 Int)
+(declare-const i13 Int)
+(declare-const i14 Int)
+(declare-const v4 Bool)
+(assert (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))))
+(declare-const v5 Bool)
+(assert v1)
+(declare-const i15 Int)
+(declare-const v6 Bool)
+(assert (distinct v5 (<= i8 i15)))
+(declare-const i16 Int)
+(assert v0)
+(declare-const i17 Int)
+(assert (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)))
+(declare-const i18 Int)
+(declare-const v7 Bool)
+(assert (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6))
+(declare-const v8 Bool)
+(declare-const v9 Bool)
+(assert (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)))
+(assert (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))
+(assert (=> v4 (<= i13 i6)))
+(declare-const v10 Bool)
+(declare-const v11 Bool)
+(assert v9)
+(check-sat)
+(assert (> (abs i7) i4))
+(assert v2)
+(declare-const v12 Bool)
+(assert (distinct v5 (<= i8 i15)))
+(declare-const i19 Int)
+(assert (xor (not (< (div i4 i8) 79)) (> (- 888) i15) (distinct i6 i12) (distinct i6 i12) (= (or v1 v3 v2) v1) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) v10))
+(check-sat)
+(declare-const v13 Bool)
+(push 1)
+(assert (< i9 i8))
+(assert (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8))
+(push 1)
+(push 1)
+(declare-const v14 Bool)
+(assert v7)
+(assert v10)
+(declare-const v15 Bool)
+(declare-const v16 Bool)
+(declare-const i20 Int)
+(assert (or v1 v3 v2))
+(declare-const i21 Int)
+(declare-const v17 Bool)
+(assert (=> (> i6 (abs 79)) (or (= (- i8) 36) v6 v1)))
+(declare-const v18 Bool)
+(assert (distinct i6 i12))
+(declare-const v19 Bool)
+(assert (< i9 i8))
+(declare-const v20 Bool)
+(assert (= v16 (>= i19 (abs i14)) (= (or (= (- i8) 36) v6 v1) (distinct i6 i12) (> 546 i8) (> 546 i8) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) (> i6 (abs 79)) v11 (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) (<= i13 i6)))
+(declare-const v21 Bool)
+(declare-const v22 Bool)
+(assert (> 79 34))
+(declare-const i22 Int)
+(assert v9)
+(declare-const i23 Int)
+(declare-const v23 Bool)
+(declare-const v24 Bool)
+(declare-const i24 Int)
+(pop 1)
+(declare-const i25 Int)
+(assert (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))))
+(declare-const v25 Bool)
+(pop 1)
+(declare-const v26 Bool)
+(declare-const i26 Int)
+(declare-const i27 Int)
+(assert (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1))
+(push 1)
+(assert (and (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8) (>= i14 i19) (> (abs i7) i4)))
+(declare-const v27 Bool)
+(declare-const v28 Bool)
+(declare-const v29 Bool)
+(declare-const i28 Int)
+(assert (distinct v5 (<= i8 i15)))
+(assert (xor (> (- 888) i15) v3 (< i9 i8) (=> v4 (<= i13 i6)) (>= 162 43) (and (>= 162 43) (distinct 623 752) (= i15 960)) (and (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= v2 (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (<= i13 i6) v12 v11 v10 (distinct v5 (<= i8 i15)) v5 v8) (>= i14 i19) (> (abs i7) i4))))
+(assert (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)))
+(declare-const v30 Bool)
+(assert (or (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) v6 (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (>= 162 43) v30 (< (div i4 i8) 79) v2 (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6)))
+(assert (= (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) v28 v28))
+(declare-const v31 Bool)
+(assert (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1))
+(declare-const v32 Bool)
+(pop 1)
+(declare-const i29 Int)
+(assert (xor v2 v2 v3 v0 v0 v2 v3 v1 v2))
+(declare-const v33 Bool)
+(assert v9)
+(push 1)
+(declare-const v34 Bool)
+(assert (or (>= 162 43) (>= i14 i19) (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (< (div i4 i8) 79) (< i6 (div i4 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (or (not (< (div i4 i8) 79)) (> (abs i7) i4) (= (or (= (- i8) 36) v6 v1) (distinct i6 i12) (> 546 i8) (> 546 i8) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6)) (> i6 (abs 79)) v11 (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) (xor (or v1 v3 v2) (<= i13 i6) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v1 (<= i13 i6) (= (or v1 v3 v2) v1) v0 (= (or v1 v3 v2) v1) v2 v0 v2 (or v1 v3 v2) (=> v4 (<= i13 i6))) (= (- i8) 36) v4 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6))) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (< i9 i8) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1)) v5))
+(declare-const i30 Int)
+(declare-const v35 Bool)
+(push 1)
+(assert (and (>= 162 43) (distinct 623 752) (= i15 960)))
+(declare-const v36 Bool)
+(assert (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))))
+(push 1)
+(declare-const v37 Bool)
+(declare-const v38 Bool)
+(assert (distinct (= v3 v4 (<= i13 i6) v0 v10 v6) (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (> 546 i8) (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (= (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v2 (=> (= v3 v4 (<= i13 i6) v0 v10 v6) v1) (>= 34 36) (and v3 (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) v3 v0 v2 v4 (= (or v1 v3 v2) v1) (= (or v1 v3 v2) v1))) (< i6 (div i4 i8)) (or (or (= (- i8) 36) v6 v1) v10 v5 v10 (= (<= i8 i15) v0 (distinct i6 i12) (= (or v1 v3 v2) v1) v6 v1 (= (- i8) 36) v6) v8 (< i9 i8)) (< (div i4 i8) 79)))
+(assert (and (= v3 v4 (<= i13 i6) v0 v10 v6) (>= (abs 969) (* i6 162 i4 i4))))
+(assert v0)
+(assert (<= 12 i4))
+(check-sat)
+(assert (distinct (>= (abs 969) (* i6 162 i4 i4)) (xor (=> (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (=> v4 (<= i13 i6))) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (< (div i4 i8) 79) v11 (xor (xor (or v1 v3 v2) v3 (= (or v1 v3 v2) v1) (= (- i8) 36) (=> v4 (<= i13 i6)) v3 v2 (=> v4 (<= i13 i6)) v4 (or v1 v3 v2)) (xor v2 v2 v3 v0 v0 v2 v3 v1 v2) (= (- i8) 36) v6) v4 (> 546 i8) (> i6 (abs 79)))))
+(assert (=> (or (= (- i8) 36) v6 v1) (distinct v5 (<= i8 i15))))
+(declare-const v39 Bool)
+(push 1)
+(declare-const v40 Bool)
+(declare-const v41 Bool)
+(declare-const v42 Bool)
+(check-sat)
+(assert (or (= (- i8) 36) v6 v1))
+(assert (=> (=> v4 (<= i13 i6)) (< i6 (div i4 i8))))
+(pop 1)
+(declare-const v43 Bool)
+(pop 1)
+(assert (or v1 v3 v2))
+(push 1)
+(assert (not (> (abs i7) i4)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/issue3991.smt2 b/test/regress/regress0/nl/issue3991.smt2
new file mode 100644
index 000000000..c006b2885
--- /dev/null
+++ b/test/regress/regress0/nl/issue3991.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --incremental --check-unsat-cores
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-const i7 Int)
+(check-sat)
+(declare-const v18 Bool)
+(assert (and (= i7 93) (or (> 19 i7) v18) v18))
+(check-sat)
+(assert (> 19 i7))
+(assert (> (div i7 0) 0))
+(check-sat)