From f50d6702ad0ffc5a10308abc2a43f86a9b623a8c Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Wed, 10 Mar 2010 03:58:23 +0000
Subject: Lexical scoping for let-bound variables (Bug #53)

---
 src/parser/smt/smt_parser.g | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/parser/smt')

diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index c12aa5f7a..d1ac50651 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -154,6 +154,7 @@ annotatedFormula returns [CVC4::Expr formula]
     LPAREN LET LPAREN name=variable[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN
     { defineVar(name,expr1); }
     formula=annotatedFormula
+    { undefineVar(name); }
     RPAREN
 
   | /* An flet binding */
@@ -161,6 +162,7 @@ annotatedFormula returns [CVC4::Expr formula]
     LPAREN FLET LPAREN name=function_var[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN
     { defineVar(name,expr1); }
     formula=annotatedFormula
+    { undefineVar(name); }
     RPAREN
     
   | /* A non-built-in function application */
-- 
cgit v1.2.3