summaryrefslogtreecommitdiff
path: root/src/parser/smt/Smt.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt/Smt.g')
-rw-r--r--src/parser/smt/Smt.g5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 160bd321f..25c2fbc89 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -198,10 +198,11 @@ annotatedFormula[CVC4::Expr& expr]
(LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED]
| FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] )
annotatedFormula[expr] RPAREN_TOK
- { PARSER_STATE->defineVar(name,expr); }
+ { PARSER_STATE->pushScope();
+ PARSER_STATE->defineVar(name,expr); }
annotatedFormula[expr]
RPAREN_TOK
- { PARSER_STATE->undefineVar(name); }
+ { PARSER_STATE->popScope(); }
| /* a variable */
( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback