From 6369830eec077ef112e6cc806cd910c7209eb2db Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 30 Nov 2012 20:21:39 +0000
Subject: [PATCH] parametric datatypes fix related to non-ascribed type
 constructors introduced by decision procedure

---
 src/theory/datatypes/theory_datatypes.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6273eb2c2..7c8f4014e 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -828,6 +828,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
       n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
       Assert( n_ic.getType()==n.getType() );
     }
+    n_ic = Rewriter::rewrite( n_ic );
     //d_inst_map[n][index] = n_ic;
     return n_ic;
   //}
-- 
2.30.2