From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 28 Feb 2018 03:06:58 +0000 (-0800)
Subject: Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)
X-Git-Tag: cvc5-1.0.0~5265
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=db3d2f7ae12e107f771c5683636febe3e27e8716;p=cvc5.git

Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)
---

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());