From 8936ca3ab2a1b9e3612e08a73542f7a288ee1df8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 15 Jun 2013 21:00:39 -0500
Subject: [PATCH] Fix in SMT2 parser for parametric datatypes

---
 src/parser/smt2/Smt2.g | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5abaa0163..373f5b3a4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -801,7 +801,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
                              MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
         v.insert(v.end(), f.begin(), f.end());
-        f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+        expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
-- 
2.30.2