summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-02-27 19:06:58 -0800
committerGitHub <noreply@github.com>2018-02-27 19:06:58 -0800
commitdb3d2f7ae12e107f771c5683636febe3e27e8716 (patch)
treed21f39ec8e38776c16439859213f9dd74cca2a24
parent7f33294261869ab8f0caa8660222576a4ff7bcdc (diff)
Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)
-rw-r--r--src/parser/smt2/smt2.cpp3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 77b50af4c..d55b9f54b 100644
--- 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());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback