From 5b04e6f0b29be4f376ab1f306529bf8a22111bd5 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 14 Dec 2011 22:44:58 +0000
Subject: minor fixes to printing and parsing of CVC-language defined functions
 and lambdas; resolves bug 294

---
 src/parser/cvc/Cvc.g | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/parser/cvc/Cvc.g')

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2d659cfe3..9f0c2cddb 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -897,6 +897,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
           }
         }
       } else {
+        // f is not null-- meaning this is a definition not a declaration
         if(!topLevel) {
           // must be top-level; doesn't make sense to write something
           // like e.g. FORALL(x:INT = 4): [...]
@@ -908,8 +909,9 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
             i != i_end;
             ++i) {
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
+          Expr func = EXPR_MANAGER->mkVar(*i, f.getType());
           PARSER_STATE->defineFunction(*i, f);
-          Command* decl = new DefineFunctionCommand(*i, Expr(), f);
+          Command* decl = new DefineFunctionCommand(*i, func, f);
           seq->addCommand(decl);
         }
       }
-- 
cgit v1.2.3