From 8b189c3f51d2272ecbda57e367d2bd1af34fb94d Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 5 Aug 2014 17:23:41 +0200
Subject: [PATCH] Minor fix : do not drop instantiation patterns when merging
 quantifiers.

---
 src/theory/quantifiers/quantifiers_rewriter.cpp | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 4c01e927d..1a20693f9 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -159,7 +159,13 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
     }
     Node body = in[1];
     bool doRewrite = false;
+    std::vector< Node > ipl;
     while( body.getNumChildren()>=2 && body.getKind()==in.getKind() ){
+      if( body.getNumChildren()==3 ){
+        for( unsigned i=0; i<body[2].getNumChildren(); i++ ){
+          ipl.push_back( body[2][i] );
+        }
+      }
       for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
         args.push_back( body[0][i] );
       }
@@ -171,7 +177,12 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
       children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
       children.push_back( body );
       if( in.getNumChildren()==3 ){
-        children.push_back( in[2] );
+        for( unsigned i=0; i<in[2].getNumChildren(); i++ ){
+          ipl.push_back( in[2][i] );
+        }
+      }
+      if( !ipl.empty() ){
+        children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, ipl ) );
       }
       Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
       if( in!=n ){
-- 
2.30.2