projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
7f33294
)
Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)
author
Aina Niemetz
<aina.niemetz@gmail.com>
Wed, 28 Feb 2018 03:06:58 +0000
(19:06 -0800)
committer
GitHub
<noreply@github.com>
Wed, 28 Feb 2018 03:06:58 +0000
(19:06 -0800)
src/parser/smt2/smt2.cpp
patch
|
blob
|
history
diff --git
a/src/parser/smt2/smt2.cpp
b/src/parser/smt2/smt2.cpp
index 77b50af4c5de2a403664a96fc60ad1f9487b8605..d55b9f54b5e25283a49947e6c5d62b4dc274df84 100644
(file)
--- a/
src/parser/smt2/smt2.cpp
+++ b/
src/parser/smt2/smt2.cpp
@@
-397,15
+397,12
@@
void Smt2::pushDefineFunRecScope(
{
pushScope(bindingLevel);
- std::vector<Expr> f_app;
- f_app.push_back(func);
// bound variables are those that are explicitly named in the preamble
// of the define-fun(s)-rec command, we define them here
for (const std::pair<std::string, CVC4::Type>& svn : sortedVarNames)
{
Expr v = mkBoundVar(svn.first, svn.second);
bvs.push_back(v);
- f_app.push_back(v);
}
bvs.insert(bvs.end(), flattenVars.begin(), flattenVars.end());