diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-27 19:06:58 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-27 19:06:58 -0800 |
commit | db3d2f7ae12e107f771c5683636febe3e27e8716 (patch) | |
tree | d21f39ec8e38776c16439859213f9dd74cca2a24 /src/parser | |
parent | 7f33294261869ab8f0caa8660222576a4ff7bcdc (diff) |
Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 3 |
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()); |