summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-03-21 14:04:35 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-03-21 14:28:24 -0400
commit16215e6e021c0fb24a6237126e17c89485dfc012 (patch)
tree484f927a27af4d26c616d5982e0b0ce2497eaad7 /src/parser/smt2/Smt2.g
parent118e998b926870e817cd57c49b91fdb27948e828 (diff)
Some model and printing fixes for defined functions in input.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g4
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]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback