From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 16 Jun 2013 02:00:39 +0000 (-0500)
Subject: Fix in SMT2 parser for parametric datatypes
X-Git-Tag: cvc5-1.0.0~7287^2~98
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8936ca3ab2a1b9e3612e08a73542f7a288ee1df8;p=cvc5.git

Fix in SMT2 parser for parametric datatypes
---

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.");