Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)
authorAina Niemetz <aina.niemetz@gmail.com>
Wed, 28 Feb 2018 03:06:58 +0000 (19:06 -0800)
committerGitHub <noreply@github.com>
Wed, 28 Feb 2018 03:06:58 +0000 (19:06 -0800)
src/parser/smt2/smt2.cpp

index 77b50af4c5de2a403664a96fc60ad1f9487b8605..d55b9f54b5e25283a49947e6c5d62b4dc274df84 100644 (file)
@@ -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());