Minor fixes for rec-fun (#1616)

1 files changed, 39 insertions, 11 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 5586c04fb..bc298fa9c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -517,14 +517,36 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
     Assert( !h.isNull() );
     // if it is a function definition, rewrite the body independently
     Node fbody = QuantAttributes::getFunDefBody( q );
-    Assert( !body.isNull() );
     Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
-    Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, false );
-    Assert( new_vars.size()==h.getNumChildren() );
-    return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) );
-  }else{
-    return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, options::elimExtArithQuant() );
-  }
+    if (!fbody.isNull())
+    {
+      Node r = computeProcessTerms2(fbody,
+                                    true,
+                                    true,
+                                    curr_cond,
+                                    0,
+                                    cache,
+                                    icache,
+                                    new_vars,
+                                    new_conds,
+                                    false);
+      Assert(new_vars.size() == h.getNumChildren());
+      return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r));
+    }
+    // It can happen that we can't infer the shape of the function definition,
+    // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to
+    // forall xy. false.
+  }
+  return computeProcessTerms2(body,
+                              true,
+                              true,
+                              curr_cond,
+                              0,
+                              cache,
+                              icache,
+                              new_vars,
+                              new_conds,
+                              options::elimExtArithQuant());
 }
 
 Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
@@ -1917,7 +1939,16 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs );
     return nn.negate();
   }else if( n.getKind()==kind::FORALL ){
-    if( polarity ){
+    if (n.getNumChildren() == 3)
+    {
+      // Do not pre-skolemize quantified formulas with three children.
+      // This includes non-standard quantified formulas
+      // like recursive function definitions, or sygus conjectures, and
+      // quantified formulas with triggers.
+      return n;
+    }
+    else if (polarity)
+    {
       if( options::preSkolemQuant() && options::preSkolemQuantNested() ){
         vector< Node > children;
         children.push_back( n[0] );
@@ -1932,9 +1963,6 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
         }
         //process body
         children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) );
-        if( n.getNumChildren()==3 ){
-          children.push_back( n[2] );
-        }
         //return processed quantifier
         return NodeManager::currentNM()->mkNode( kind::FORALL, children );
       }