diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 14:04:35 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 14:28:24 -0400 |
commit | 16215e6e021c0fb24a6237126e17c89485dfc012 (patch) | |
tree | 484f927a27af4d26c616d5982e0b0ce2497eaad7 /src/parser | |
parent | 118e998b926870e817cd57c49b91fdb27948e828 (diff) |
Some model and printing fixes for defined functions in input.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1ee288aa4..a390cf452 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -267,7 +267,7 @@ command returns [CVC4::Command* cmd = NULL] sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } } term[expr, expr2] @@ -479,7 +479,7 @@ extendedCommand[CVC4::Command*& cmd] sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } } term[e,e2] |