From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 30 Nov 2012 20:21:39 +0000 (+0000)
Subject: parametric datatypes fix related to non-ascribed type constructors introduced by... 
X-Git-Tag: cvc5-1.0.0~7516
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6369830eec077ef112e6cc806cd910c7209eb2db;p=cvc5.git

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

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;
   //}