Do beta-reduction in expandDefinitions (#2286)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ab14904ff17a5cbf92d9f25da6800b9b48c890a2..bcb5c58b4d76174fad70073a645076c7cdc10baa 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2814,13 +2814,29 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
       }
 
       // otherwise expand it
-      bool doExpand = k == kind::APPLY;
-      if( !doExpand ){
-        // options that assign substitutions to APPLY_UF
-        if (options::macrosQuant() || options::sygusInference())
+      bool doExpand = false;
+      if (k == kind::APPLY)
+      {
+        doExpand = true;
+      }
+      else if (k == kind::APPLY_UF)
+      {
+        // Always do beta-reduction here. The reason is that there may be
+        // operators such as INTS_MODULUS in the body of the lambda that would
+        // otherwise be introduced by beta-reduction via the rewriter, but are
+        // not expanded here since the traversal in this function does not
+        // traverse the operators of nodes. Hence, we beta-reduce here to
+        // ensure terms in the body of the lambda are expanded during this
+        // call.
+        if (n.getOperator().getKind() == kind::LAMBDA)
+        {
+          doExpand = true;
+        }
+        else if (options::macrosQuant() || options::sygusInference())
         {
-          //expand if we have inferred an operator corresponds to a defined function
-          doExpand = k==kind::APPLY_UF && d_smt.isDefinedFunction( n.getOperator().toExpr() );
+          // The above options assign substitutions to APPLY_UF, thus we check
+          // here and expand if this operator corresponds to a defined function.
+          doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr());
         }
       }
       if (doExpand) {