parametric datatypes fix related to non-ascribed type constructors introduced by...

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6273eb2c26a52bf051c2bd46faf1c2b72549c66a..7c8f4014e0d35fb1d0f5282d428ef8a8776a498d 100644 (file)
--- 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;
   //}