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.g8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index d44f7abcb..429adee0a 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -470,8 +470,8 @@ functionDeclaration[CVC4::Command*& smt_command]
} else {
t = EXPR_MANAGER->mkFunctionType(sorts);
}
- PARSER_STATE->mkVar(name, t);
- smt_command = new DeclareFunctionCommand(name, t);
+ Expr func = PARSER_STATE->mkVar(name, t);
+ smt_command = new DeclareFunctionCommand(name, func, t);
}
;
@@ -490,8 +490,8 @@ predicateDeclaration[CVC4::Command*& smt_command]
} else {
t = EXPR_MANAGER->mkPredicateType(p_sorts);
}
- PARSER_STATE->mkVar(name, t);
- smt_command = new DeclareFunctionCommand(name, t);
+ Expr func = PARSER_STATE->mkVar(name, t);
+ smt_command = new DeclareFunctionCommand(name, func, t);
}
;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback