diff --git a/install.sh b/install.sh
index 299186752..90ee9b78a 100755
--- a/install.sh
+++ b/install.sh
@@ -14,10 +14,10 @@ CBMC=`pwd`
 git checkout $CBMC_VERSION
 if grep '^MINISAT2' src/config.inc > /dev/null
 then
-  make -C src minisat2-download > /dev/null
+  make -C src minisat2-download > /dev/null -j4
 elif grep '^GLUCOSE' src/config.inc
 then
-  make -C src glucose-download
+  make -C src glucose-download -j4
 else
   echo "SAT solver not supported"
   exit 1
@@ -26,7 +26,7 @@ if [ "$COMPILER" != "" ]
 then
   make -C src CXX=$COMPILER
 else
-  make -C src
+  make -C src -j4
 fi
 
 cd ../src
@@ -36,7 +36,7 @@ if [ "$COMPILER" != "" ]
 then
   make CXX=$COMPILER
 else
-  make
+  make -j4
 fi
 cd ..
 echo "The executable is src/2ls/2ls"
diff --git a/regression/interprocedural/contextsensitive2/main.c b/regression/interprocedural/contextsensitive2/main.c
index 70fd27c8b..4a2ef0219 100644
--- a/regression/interprocedural/contextsensitive2/main.c
+++ b/regression/interprocedural/contextsensitive2/main.c
@@ -20,7 +20,6 @@ void main()
   int x = 1;
   int y = do1(x);
   assert(y==1);
-  x = -x;
-  int z = do2(x);
+  int z = do2(-x);
   assert(-1<=z && z<=1);
 }
diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp
index a9e8a3f76..9c69d5c79 100644
--- a/src/2ls/2ls_parse_options.cpp
+++ b/src/2ls/2ls_parse_options.cpp
@@ -53,6 +53,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include "summary_checker_bmc.h"
 #include "summary_checker_kind.h"
 #include "summary_checker_nonterm.h"
+#include "summary_checker_rect.h"
 #include "show.h"
 #include "horn_encoding.h"
 
@@ -316,6 +317,13 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
     if(!cmdline.isset("unwind"))
       options.set_option("unwind", std::numeric_limits<unsigned>::max());
   }
+    //............................................
+  // handle recursive functions
+  if(cmdline.isset("has-recursion"))
+  {
+    options.set_option("has-recursion", true);
+  }
+  //.............................................
 
   // check for spuriousness of assertion failures
   if(cmdline.isset("no-spurious-check"))
@@ -493,9 +501,9 @@ int twols_parse_optionst::doit()
   }
 
 #if IGNORE_RECURSION
-  if(recursion_detected)
+  if(recursion_detected && !cmdline.isset("has-recursion"))
   {
-    status() << "Recursion not supported" << eom;
+    status() << "Recursion not supportedwithout --has-recursion option" << eom;
     report_unknown();
     return 5;
   }
@@ -582,8 +590,15 @@ int twols_parse_optionst::doit()
     std::unique_ptr<summary_checker_baset> checker;
     if(!options.get_bool_option("k-induction") &&
        !options.get_bool_option("incremental-bmc"))
-      checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_ait(options, heap_analysis));
+    {
+      if(options.get_bool_option("has-recursion"))
+        checker=std::unique_ptr<summary_checker_baset>(
+          new summary_checker_rect(options, heap_analysis));
+      else
+        checker=std::unique_ptr<summary_checker_baset>(
+          new summary_checker_ait(options, heap_analysis));
+
+    }
     if(options.get_bool_option("k-induction") &&
        !options.get_bool_option("incremental-bmc"))
       checker=std::unique_ptr<summary_checker_baset>(
@@ -1765,6 +1780,7 @@ void twols_parse_optionst::help()
     " --termination                compute ranking functions to prove termination\n" // NOLINT(*)
     " --k-induction                use k-induction\n"
     " --incremental-bmc            use incremental-bmc\n"
+    " --has-recursion              enable recursive function support"
     " --preconditions              compute preconditions\n"
     " --sufficient                 sufficient preconditions (default: necessary)\n" // NOLINT(*)
     " --havoc                      havoc loops and function calls\n"
diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h
index 2199b95d3..2bdf1dc75 100644
--- a/src/2ls/2ls_parse_options.h
+++ b/src/2ls/2ls_parse_options.h
@@ -65,7 +65,7 @@ class optionst;
   "(graphml-witness):(json-cex):" \
   "(no-spurious-check)(stop-on-fail)" \
   "(competition-mode)(slice)(no-propagation)(independent-properties)" \
-  "(no-unwinding-assertions)"
+  "(no-unwinding-assertions)(has-recursion)"
   // the last line is for CBMC-regression testing only
 
 class twols_parse_optionst:
diff --git a/src/2ls/Makefile b/src/2ls/Makefile
index 5b9362169..c817b5e84 100644
--- a/src/2ls/Makefile
+++ b/src/2ls/Makefile
@@ -6,6 +6,7 @@ SRC = 2ls_main.cpp 2ls_parse_options.cpp \
       2ls_languages.cpp \
       show.cpp summary_checker_base.cpp \
       summary_checker_ai.cpp summary_checker_bmc.cpp \
+      summary_checker_rect.cpp \
       summary_checker_kind.cpp summary_checker_nonterm.cpp \
       cover_goals_ext.cpp horn_encoding.cpp \
       preprocessing_util.cpp \
diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp
index 63aa43f15..548dfbedf 100644
--- a/src/2ls/summary_checker_base.cpp
+++ b/src/2ls/summary_checker_base.cpp
@@ -7,6 +7,7 @@ Author: Peter Schrammel
 \*******************************************************************/
 
 #include <iostream>
+#include <fstream>
 
 #include <util/options.h>
 #include <util/i2string.h>
@@ -80,6 +81,7 @@ void summary_checker_baset::SSA_functions(
 
   // properties
   initialize_property_map(goto_model.goto_functions);
+  //CustomSSAOperation(SSA,ns,"");//execute ic3
 }
 
 /*******************************************************************\
diff --git a/src/2ls/summary_checker_base.h b/src/2ls/summary_checker_base.h
index 0d65062ce..6475517be 100644
--- a/src/2ls/summary_checker_base.h
+++ b/src/2ls/summary_checker_base.h
@@ -84,7 +84,7 @@ class summary_checker_baset:public property_checkert
     const namespacet &ns,
     const ssa_heap_analysist &heap_analysis);
 
-  void summarize(
+  virtual void summarize(
     const goto_modelt &,
     bool forward=true,
     bool termination=false);
diff --git a/src/2ls/summary_checker_rect.cpp b/src/2ls/summary_checker_rect.cpp
new file mode 100644
index 000000000..968bcf171
--- /dev/null
+++ b/src/2ls/summary_checker_rect.cpp
@@ -0,0 +1,134 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   summary_checker_rect.cpp
+ * Author: sarbojit
+ * 
+ * Created on 21 March, 2018, 7:13 PM
+ */
+
+#include <solver/summarizer_fw.h>
+#include <solver/summarizer_fw_term.h>
+#include <solver/summarizer_bw.h>
+#include <solver/summarizer_bw_term.h>
+#include <solver/summarizer_rec_fw.h>
+
+#include "summary_checker_rect.h"
+
+property_checkert::resultt summary_checker_rect::operator()(
+  const goto_modelt &goto_model)
+{
+  const namespacet ns(goto_model.symbol_table);
+
+  SSA_functions(goto_model, ns, heap_analysis);
+
+  ssa_unwinder.init(false, false);
+
+  unsigned unwind=options.get_unsigned_int_option("unwind");
+  if(unwind>0)
+  {
+    status() << "Unwinding" << messaget::eom;
+
+    ssa_unwinder.init_localunwinders();
+
+    ssa_unwinder.unwind_all(unwind);
+  }
+
+  // properties
+  initialize_property_map(goto_model.goto_functions);
+
+  property_checkert::resultt result=property_checkert::UNKNOWN;
+  bool finished=false;
+  while(!finished)
+  {
+    bool preconditions=options.get_bool_option("preconditions");
+    bool termination=options.get_bool_option("termination");
+    bool trivial_domain=options.get_bool_option("havoc");
+    if(!trivial_domain || termination)
+    {
+      // forward analysis
+      summarize(goto_model, true, termination);
+    }
+    if(!trivial_domain && preconditions)
+    {
+      status()<<"No backward analysis supported for recursive programs."<<eom;
+      exit(1);
+    }
+
+    if(preconditions)
+    {
+      report_statistics();
+      report_preconditions();
+      return property_checkert::UNKNOWN;
+    }
+
+    if(termination)
+    {
+      report_statistics();
+      return report_termination();
+    }
+
+#ifdef SHOW_CALLINGCONTEXTS
+    if(options.get_bool_option("show-calling-contexts"))
+      return property_checkert::UNKNOWN;
+#endif
+
+  if(result==property_checkert::UNKNOWN &&
+       options.get_bool_option("heap-values-refine") &&
+       options.get_bool_option("heap-interval"))
+    {
+      summary_db.clear();
+      options.set_option("heap-interval", false);
+      options.set_option("heap-zones", true);
+    }
+    else
+    {
+      finished=true;
+    }
+  }
+  //return result;
+  return UNKNOWN;
+}
+
+void summary_checker_rect::summarize(
+  const goto_modelt &goto_model,
+  bool forward,
+  bool termination)
+{
+  summarizer_baset *summarizer=NULL;
+#ifdef SHOW_CALLING_CONTEXTS
+  if(options.get_bool_option("show-calling-contexts"))
+    summarizer=new summarizer_fw_contextst(
+      options, summary_db, ssa_db, ssa_unwinder, ssa_inliner);
+  else // NOLINT(*)
+#endif
+  {
+    if(!termination)
+      summarizer=new summarizer_rec_fwt(
+        options, summary_db, ssa_db, ssa_unwinder, ssa_inliner);
+    else
+    {
+      status()<<"No termination check supported for recursive programs."<<eom;
+      exit(1);
+    }
+  }
+  assert(summarizer!=NULL);
+  summarizer->set_message_handler(get_message_handler());
+  if(!options.get_bool_option("context-sensitive") &&
+     options.get_bool_option("all-functions"))
+    summarizer->summarize();
+  else
+    summarizer->summarize(goto_model.goto_functions.entry_point());
+
+  // statistics
+  solver_instances+=summarizer->get_number_of_solver_instances();
+  solver_calls+=summarizer->get_number_of_solver_calls();
+  summaries_used+=summarizer->get_number_of_summaries_used();
+  termargs_computed+=summarizer->get_number_of_termargs_computed();
+
+  delete summarizer;
+}
diff --git a/src/2ls/summary_checker_rect.h b/src/2ls/summary_checker_rect.h
new file mode 100644
index 000000000..41e0a017b
--- /dev/null
+++ b/src/2ls/summary_checker_rect.h
@@ -0,0 +1,28 @@
+/* 
+ * File:   summary_checker_rect.h
+ * Author: sarbojit
+ *
+ * Created on 21 March, 2018, 7:13 PM
+ */
+
+#ifndef SUMMARY_CHECKER_RECT_H
+#define SUMMARY_CHECKER_RECT_H
+
+#include "summary_checker_ai.h"
+
+class summary_checker_rect:public summary_checker_ait
+{
+public:
+  explicit summary_checker_rect(optionst &_options,
+  const ssa_heap_analysist &heap_analysis):
+  summary_checker_ait(_options, heap_analysis)
+  {
+  }
+        
+  virtual resultt operator()(const goto_modelt &);
+protected:
+  void summarize(const goto_modelt &, bool, bool);
+};
+
+#endif /* SUMMARY_CHECKER_RECT_H */
+
diff --git a/src/config.inc.bak b/src/config.inc.bak
new file mode 100644
index 000000000..002688fa8
--- /dev/null
+++ b/src/config.inc.bak
@@ -0,0 +1,10 @@
+CBMC = ~/my-cbmc
+
+# Variables you may want to override
+#CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic
+
+#static compilation
+#LINKFLAGS += -static-libgcc -static-libstdc++
+
+#2LS switches
+TWOLS_FLAGS = 
diff --git a/src/domains/Makefile b/src/domains/Makefile
index e293aee2f..f25ec032b 100644
--- a/src/domains/Makefile
+++ b/src/domains/Makefile
@@ -9,6 +9,7 @@ SRC = tpolyhedra_domain.cpp equality_domain.cpp domain.cpp \
   strategy_solver_enumeration.cpp strategy_solver_binsearch.cpp \
   template_generator_base.cpp template_generator_summary.cpp \
   template_generator_callingcontext.cpp template_generator_ranking.cpp \
+  template_gen_rec_summary.cpp \
   strategy_solver_binsearch2.cpp strategy_solver_binsearch3.cpp \
   strategy_solver_predabs.cpp strategy_solver_heap.cpp \
   strategy_solver_heap_tpolyhedra.cpp \
diff --git a/src/domains/domain.h b/src/domains/domain.h
index 5f8fde816..646148442 100644
--- a/src/domains/domain.h
+++ b/src/domains/domain.h
@@ -24,11 +24,13 @@ class domaint
   domaint(
     unsigned _domain_number,
     replace_mapt &_renaming_map,
-    const namespacet &_ns):
+    const namespacet &_ns,
+    bool rec=false):
     domain_number(_domain_number),
     renaming_map(_renaming_map),
     ns(_ns)
   {
+    recursive=rec;
   }
 
   virtual ~domaint()
@@ -120,6 +122,8 @@ class domaint
   unsigned domain_number; // serves as id for variables names
   replace_mapt &renaming_map;
   const namespacet &ns;
+  
+  bool recursive;//sarbojit
 
   inline void rename(exprt &expr)
   {
diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp
index 72ad03b52..2ac046147 100644
--- a/src/domains/ssa_analyzer.cpp
+++ b/src/domains/ssa_analyzer.cpp
@@ -63,7 +63,9 @@ void ssa_analyzert::operator()(
   incremental_solvert &solver,
   local_SSAt &SSA,
   const exprt &precondition,
-  template_generator_baset &template_generator)
+  template_generator_baset &template_generator,
+  bool recursive,
+  const exprt &merge_expr)
 {
   if(SSA.goto_function.body.instructions.empty())
     return;
@@ -73,6 +75,8 @@ void ssa_analyzert::operator()(
 
   solver.new_context();
   solver << SSA.get_enabling_exprs();
+  
+  if(recursive) solver<<merge_expr;//add merge expressions to solver
 
   // add precondition (or conjunction of asssertion in backward analysis)
   solver << precondition;
@@ -174,6 +178,15 @@ void ssa_analyzert::operator()(
 
   // initialize inv
   domain->initialize(*result);
+  
+  // initialize input arguments and input global variables with calling context
+  if(recursive &&
+    template_generator.options.get_bool_option("context-sensitive"))
+  {
+    while(strategy_solver->iterate_for_ins(*result)) {}
+    status()<<"------------------------------------------------------------------\n"///////////////////////////
+     "-------------------------------------------------------------------\n"<<eom;///////////////////////////
+  }
 
   // iterate
   while(strategy_solver->iterate(*result)) {}
diff --git a/src/domains/ssa_analyzer.h b/src/domains/ssa_analyzer.h
index 5398e883d..3c6e69f22 100644
--- a/src/domains/ssa_analyzer.h
+++ b/src/domains/ssa_analyzer.h
@@ -22,7 +22,8 @@ class ssa_analyzert:public messaget
 public:
   typedef strategy_solver_baset::constraintst constraintst;
   typedef strategy_solver_baset::var_listt var_listt;
-
+  typedef std::vector<std::pair<exprt,std::vector<exprt>>> tmpl_rename_mapt;
+  
   ssa_analyzert():
     result(NULL),
     solver_instances(0),
@@ -40,7 +41,9 @@ class ssa_analyzert:public messaget
     incremental_solvert &solver,
     local_SSAt &SSA,
     const exprt &precondition,
-    template_generator_baset &template_generator);
+    template_generator_baset &template_generator,
+    bool recursive=false,
+    const exprt &merge_expr=true_exprt());
 
   void get_result(exprt &result, const domaint::var_sett &vars);
 
diff --git a/src/domains/strategy_solver_base.h b/src/domains/strategy_solver_base.h
index 7915b5ef9..29cd9823a 100644
--- a/src/domains/strategy_solver_base.h
+++ b/src/domains/strategy_solver_base.h
@@ -31,6 +31,7 @@ class strategy_solver_baset:public messaget
   {}
 
   virtual bool iterate(invariantt &inv) { assert(false); }
+  virtual bool iterate_for_ins(invariantt &inv) { assert(false); }
 
   inline unsigned get_number_of_solver_calls() { return solver_calls; }
   inline unsigned get_number_of_solver_instances() { return solver_instances; }
diff --git a/src/domains/strategy_solver_binsearch.cpp b/src/domains/strategy_solver_binsearch.cpp
index 398d66ddd..5c0b7db5c 100644
--- a/src/domains/strategy_solver_binsearch.cpp
+++ b/src/domains/strategy_solver_binsearch.cpp
@@ -36,10 +36,10 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv)
 
   exprt inv_expr=tpolyhedra_domain.to_pre_constraints(inv);
 
-#if 0
+//#if 0
   debug() << "improvement check: " << eom;
   debug() << "pre-inv: " << from_expr(ns, "", inv_expr) << eom;
-#endif
+//#endif
 
   solver << inv_expr;
 
@@ -49,33 +49,33 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv)
 
   strategy_cond_literals.resize(strategy_cond_exprs.size());
 
-#if 0
+//#if 0
   debug() << "post-inv: ";
-#endif
+//#endif
   for(std::size_t i=0; i<strategy_cond_exprs.size(); i++)
   {
-#if 0
+//#if 0
     debug() << (i>0 ? " || " : "") << from_expr(ns, "", strategy_cond_exprs[i]);
-#endif
+//#endif
     strategy_cond_literals[i]=solver.convert(strategy_cond_exprs[i]);
     // solver.set_frozen(strategy_cond_literals[i]);
     strategy_cond_exprs[i]=literal_exprt(strategy_cond_literals[i]);
   }
-#if 0
+//#if 0
   debug() << eom;
-#endif
+//#endif
 
   solver << disjunction(strategy_cond_exprs);
 
-#if 0
+//#if 0
   debug() << "solve(): ";
-#endif
+//#endif
 
   if(solver()==decision_proceduret::D_SATISFIABLE) // improvement check
   {
-#if 0
+//#if 0
     debug() << "SAT" << eom;
-#endif
+//#endif
 
 #if 0
     for(std::size_t i=0; i<solver.formula.size(); i++)
@@ -137,11 +137,11 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv)
 
     solver << post_inv_expr;
 
-#if 0
+//#if 0
     debug() << "symbolic value system: " << eom;
     debug() << "pre-inv: " << from_expr(ns, "", pre_inv_expr) << eom;
     debug() << "post-inv: " << from_expr(ns, "", post_inv_expr) << eom;
-#endif
+//s#endif
 
     while(tpolyhedra_domain.less_than(lower, upper))
     {
@@ -154,25 +154,25 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv)
       exprt c=
         tpolyhedra_domain.get_row_symb_value_constraint(row, middle, true);
 
-#if 0
+//#if 0
       debug() << "upper: " << from_expr(ns, "", upper) << eom;
       debug() << "middle: " << from_expr(ns, "", middle) << eom;
       debug() << "lower: " << from_expr(ns, "", lower) << eom;
-#endif
+//#endif
 
       solver.new_context(); // binary search iteration
 
-#if 0
+//#if 0
       debug() << "constraint: " << from_expr(ns, "", c) << eom;
-#endif
+//#endif
 
       solver << c;
 
       if(solver()==decision_proceduret::D_SATISFIABLE)
       {
-#if 0
+//#if 0
         debug() << "SAT" << eom;
-#endif
+//#endif
 
 #if 0
         for(std::size_t i=0; i<tpolyhedra_domain.template_size(); i++)
@@ -201,9 +201,9 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv)
       }
       else
       {
-#if 0
+//#if 0
         debug() << "UNSAT" << eom;
-#endif
+//#endif
 
 #if 0
         for(std::size_t i=0; i<solver.formula.size(); ++i)
@@ -231,9 +231,9 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv)
   }
   else
   {
-#if 0
+//#if 0
     debug() << "UNSAT" << eom;
-#endif
+//#endif
 
 #ifdef DEBUG_FORMULA
     for(std::size_t i=0; i<solver.formula.size(); ++i)
@@ -250,3 +250,230 @@ bool strategy_solver_binsearcht::iterate(invariantt &_inv)
 
   return improved;
 }
+
+bool strategy_solver_binsearcht::iterate_for_ins(invariantt &_inv)
+{
+  tpolyhedra_domaint::templ_valuet &inv=
+    static_cast<tpolyhedra_domaint::templ_valuet &>(_inv);
+
+  bool improved=false;
+
+  solver.new_context(); // for improvement check
+
+  exprt inv_expr=tpolyhedra_domain.to_pre_constraints(inv,true);
+
+//#if 0
+  debug() << "improvement check: " << eom;
+  debug() << "pre-inv: " << from_expr(ns, "", inv_expr) << eom;
+//#endif
+
+  solver << inv_expr;
+
+  exprt::operandst strategy_cond_exprs;
+  tpolyhedra_domain.make_not_post_constraints(
+    inv, strategy_cond_exprs, strategy_value_exprs,true);
+
+  strategy_cond_literals.resize(strategy_cond_exprs.size());
+
+//#if 0
+  debug() << "post-inv: ";
+//#endif
+
+  for(std::size_t i=0; i<strategy_cond_exprs.size(); i++)
+  {
+//#if 0
+    debug() << (i>0 ? " || " : "") << from_expr(ns, "", strategy_cond_exprs[i]);
+//#endif
+    strategy_cond_literals[i]=solver.convert(strategy_cond_exprs[i]);
+    // solver.set_frozen(strategy_cond_literals[i]);
+    strategy_cond_exprs[i]=literal_exprt(strategy_cond_literals[i]);
+  }
+//#if 0
+  debug() << eom;
+//#endif
+
+  solver << disjunction(strategy_cond_exprs);
+
+//#if 0
+  debug() << "solve(): ";
+//#endif
+
+  if(solver()==decision_proceduret::D_SATISFIABLE) // improvement check
+  {
+//#if 0
+    debug() << "SAT" << eom;
+//#endif
+
+#if 0
+    for(std::size_t i=0; i<solver.formula.size(); i++)
+    {
+      debug() << "literal: " << solver.formula[i]
+              << " " << solver.l_get(solver.formula[i]) << eom;
+    }
+
+    for(std::size_t i=0; i<tpolyhedra_domain.template_size(); i++)
+    {
+      exprt c=tpolyhedra_domain.get_row_post_constraint(i, inv[i]);
+      debug() << "cond: " << from_expr(ns, "", c) << " "
+              << from_expr(ns, "", solver.get(c)) << eom;
+      debug() << "expr: " << from_expr(ns, "", strategy_value_exprs[i]) << " "
+              << from_expr(
+                ns, "", simplify_const(solver.get(strategy_value_exprs[i])))
+              << eom;
+      debug() << "guards: "
+              << from_expr(ns, "", tpolyhedra_domain.templ[i].pre_guard) << " "
+              << from_expr(
+                ns, "", solver.get(tpolyhedra_domain.templ[i].pre_guard))
+              << eom;
+      debug() << "guards: "
+              << from_expr(ns, "", tpolyhedra_domain.templ[i].post_guard)
+              << " "
+              << from_expr(
+                ns, "", solver.get(tpolyhedra_domain.templ[i].post_guard))
+              << eom;
+    }
+#endif
+
+
+    std::size_t row=0;
+    for(; row<strategy_cond_literals.size(); row++)
+    {
+      if(solver.l_get(strategy_cond_literals[row]).is_true())
+        break;  // we've found a row to improve
+    }
+
+    debug() << "improving row: " << row << eom;
+    std::set<tpolyhedra_domaint::rowt> improve_rows;
+    improve_rows.insert(row);
+
+    tpolyhedra_domaint::row_valuet upper=
+      tpolyhedra_domain.get_max_row_value(row);
+    tpolyhedra_domaint::row_valuet lower=
+      simplify_const(solver.get(strategy_value_exprs[row]));
+
+    solver.pop_context();  // improvement check
+
+    solver.new_context(); // symbolic value system
+
+    exprt pre_inv_expr=
+      tpolyhedra_domain.to_symb_pre_constraints(inv, improve_rows, true);
+
+    solver << pre_inv_expr;
+
+    exprt post_inv_expr=tpolyhedra_domain.get_row_symb_post_constraint(row);
+
+    solver << post_inv_expr;
+
+//#if 0
+    debug() << "symbolic value system: " << eom;
+    debug() << "pre-inv: " << from_expr(ns, "", pre_inv_expr) << eom;
+    debug() << "post-inv: " << from_expr(ns, "", post_inv_expr) << eom;
+//s#endif
+
+    while(tpolyhedra_domain.less_than(lower, upper))
+    {
+      tpolyhedra_domaint::row_valuet middle=
+        tpolyhedra_domain.between(lower, upper);
+      if(!tpolyhedra_domain.less_than(lower, middle))
+        middle=upper;
+
+      // row_symb_value >= middle
+      exprt c=
+        tpolyhedra_domain.get_row_symb_value_constraint(row, middle, true);
+
+//#if 0
+      debug() << "upper: " << from_expr(ns, "", upper) << eom;
+      debug() << "middle: " << from_expr(ns, "", middle) << eom;
+      debug() << "lower: " << from_expr(ns, "", lower) << eom;
+//#endif
+
+      solver.new_context(); // binary search iteration
+
+//#if 0
+      debug() << "constraint: " << from_expr(ns, "", c) << eom;
+//#endif
+
+      solver << c;
+
+      if(solver()==decision_proceduret::D_SATISFIABLE)
+      {
+//#if 0
+        debug() << "SAT" << eom;
+//#endif
+
+#if 0
+        for(std::size_t i=0; i<tpolyhedra_domain.template_size(); i++)
+        {
+          debug() << from_expr(ns, "", tpolyhedra_domain.get_row_symb_value(i))
+                  << " " << from_expr(
+                    ns, "", solver.get(tpolyhedra_domain.get_row_symb_value(i)))
+                  << eom;
+        }
+#endif
+
+#if 0
+        for(const auto &rm : renaming_map)
+        {
+          debug() << "replace_map (1st): "
+                  << from_expr(ns, "", rm.first) << " "
+                  << from_expr(ns, "", solver.get(rm.first)) << eom;
+          debug() << "replace_map (2nd): "
+                  << from_expr(ns, "", rm.second) << " "
+                  << from_expr(ns, "", solver.get(rm.second)) << eom;
+        }
+#endif
+
+        lower=simplify_const(
+          solver.get(tpolyhedra_domain.get_row_symb_value(row)));
+      }
+      else
+      {
+//#if 0
+        debug() << "UNSAT" << eom;
+//#endif
+
+#if 0
+        for(std::size_t i=0; i<solver.formula.size(); ++i)
+        {
+          if(solver.solver->is_in_conflict(solver.formula[i]))
+            debug() << "is_in_conflict: " << solver.formula[i] << eom;
+          else
+            debug() << "not_in_conflict: " << solver.formula[i] << eom;
+        }
+#endif
+
+        if(!tpolyhedra_domain.less_than(middle, upper))
+          middle=lower;
+        upper=middle;
+      }
+      solver.pop_context(); // binary search iteration
+    }
+
+    debug() << "update value: " << from_expr(ns, "", lower) << eom;
+
+    solver.pop_context();  // symbolic value system
+
+    tpolyhedra_domain.set_row_value(row, lower, inv);
+    improved=true;
+  }
+  else
+  {
+//#if 0
+    debug() << "UNSAT" << eom;
+//#endif
+
+#ifdef DEBUG_FORMULA
+    for(std::size_t i=0; i<solver.formula.size(); ++i)
+    {
+      if(solver.solver->is_in_conflict(solver.formula[i]))
+        debug() << "is_in_conflict: " << solver.formula[i] << eom;
+      else
+        debug() << "not_in_conflict: " << solver.formula[i] << eom;
+    }
+#endif
+
+    solver.pop_context(); // improvement check
+  }
+
+  return improved;
+}
\ No newline at end of file
diff --git a/src/domains/strategy_solver_binsearch.h b/src/domains/strategy_solver_binsearch.h
index 8bcdf7f4b..e0783cfc2 100644
--- a/src/domains/strategy_solver_binsearch.h
+++ b/src/domains/strategy_solver_binsearch.h
@@ -25,7 +25,7 @@ class strategy_solver_binsearcht:public strategy_solver_baset
   }
 
   virtual bool iterate(invariantt &inv);
-
+  virtual bool iterate_for_ins(invariantt &inv);
 protected:
   tpolyhedra_domaint &tpolyhedra_domain;
 };
diff --git a/src/domains/template_gen_rec_summary.cpp b/src/domains/template_gen_rec_summary.cpp
new file mode 100644
index 000000000..e9233f6f5
--- /dev/null
+++ b/src/domains/template_gen_rec_summary.cpp
@@ -0,0 +1,235 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   template_gen_rec_summary.cpp
+ * Author: sarbojit
+ * 
+ * Created on 19 March, 2018, 10:19 PM
+ */
+
+#define SHOW_TEMPLATE
+#include "tpolyhedra_domain.h"
+
+#include "template_gen_rec_summary.h"
+
+void template_gen_rec_summaryt::operator()(const irep_idt &function_name,
+  unsigned _domain_number,
+  const local_SSAt &SSA,
+  exprt &merge_expr,
+  bool forward)
+{
+  domain_number=_domain_number;
+  handle_special_functions(SSA); // we have to call that to prevent trouble!
+
+  collect_variables_loop(SSA, forward);
+  merge_vars(function_name, SSA, merge_expr);
+  
+  // do not compute summary for entry-point
+  if(SSA.goto_function.body.instructions.front().function!=ID__start ||
+   options.get_bool_option("preconditions"))
+  {
+    collect_inout_vars(SSA, forward);
+  }
+  
+  if(options.get_bool_option("context-sensitive"))
+  {
+    instantiate_template_for_rec(SSA);
+  }
+  // either use standard templates or user-supplied ones
+  else if(!instantiate_custom_templates(SSA))
+    instantiate_standard_domains(SSA);
+
+#ifdef SHOW_TEMPLATE_VARIABLES
+  debug() << "Template variables: " << eom;
+  domaint::output_var_specs(debug(), var_specs, SSA.ns); debug() << eom;
+#endif
+#ifdef SHOW_TEMPLATE
+  debug() << "Template: " << eom;
+  domain_ptr->output_domain(debug(), SSA.ns);
+  debug()<<"Where:\n";
+  for(const exprt& op:merge_expr.operands())
+  {
+    debug()<<"     "<<from_expr(op)<<eom;
+  }
+  debug() << eom;
+#endif
+}
+
+void template_gen_rec_summaryt::merge_vars(const irep_idt &function_name,
+  const local_SSAt &SSA,
+  exprt& merge_expr)
+{
+  exprt::operandst expr_vec,guards_vec;
+  
+  for(const exprt& var:SSA.params)
+  {
+    std::string var_name=
+       id2string(to_symbol_expr(var).get_identifier());
+    irep_idt nondet_name(var_name+"#nondet");
+    in_vars_vec.push_back(symbol_exprt(dstring(var_name+"#comb"),var.type()));
+    expr_vec.push_back(symbol_exprt(nondet_name,var.type()));
+    
+  }
+  
+  for(const exprt& var:SSA.globals_in)
+  {
+    std::string var_name=
+       id2string(to_symbol_expr(var).get_identifier());
+    irep_idt nondet_name(var_name+"#nondet");
+    in_vars_vec.push_back(symbol_exprt(dstring(var_name+"#comb"),var.type()));
+    expr_vec.push_back(symbol_exprt(nondet_name,var.type()));
+    
+  }
+  
+  for(const exprt& var:SSA.globals_out)
+  {
+    std::string var_name=
+       id2string(to_symbol_expr(var).get_identifier());
+    var_name=var_name.substr(0,var_name.find_last_of("#"));
+    irep_idt nondet_name(var_name+"#nondet");
+    out_vars_vec.push_back(symbol_exprt(dstring(var_name+"#comb"),var.type()));
+    expr_vec.push_back(symbol_exprt(nondet_name,var.type()));
+    
+  }
+  
+  for(const local_SSAt::nodet &node:SSA.nodes)
+  {
+    for(const function_application_exprt &f_call:node.function_calls)
+    {
+      std::set<symbol_exprt> globals_in,globals_out;
+      exprt guard=SSA.guard_symbol(node.location);
+      std::vector<exprt>::iterator e_it=expr_vec.begin();
+      if(function_name==to_symbol_expr(f_call.function()).get_identifier()&&
+          f_call.function().id()==ID_symbol)
+      {
+        guards_vec.push_back(guard);
+        if(options.get_bool_option("context-sensitive"))
+        {
+          for(const exprt &arg:f_call.arguments())//merging arguments
+          {
+            exprt& expr=*e_it;
+            expr=if_exprt(guard,arg,expr);
+            e_it++;
+          }
+        }
+        SSA.get_globals(node.location,globals_in,true,false);
+        for(exprt g_in:globals_in)
+        {
+          exprt& expr=*e_it;
+          expr=if_exprt(guard,g_in,expr);
+          e_it++;
+        }
+        SSA.get_globals(node.location,globals_out,false);
+        for(exprt g_out:globals_out)
+        {
+          exprt& expr=*e_it;
+          expr=if_exprt(guard,g_out,expr);
+          e_it++;
+        }
+      }
+    }
+  }
+
+  std::vector<exprt> exp_vec;
+  guard_ins=symbol_exprt("guard#ins",bool_typet());
+  for(const exprt& var:SSA.params)
+  {
+    std::string var_name=
+       id2string(to_symbol_expr(var).get_identifier());
+    irep_idt name(var_name+"#rb"),name1(var_name+"#init");
+    symbol_exprt var_rb(name,var.type()),var_init(name1,var.type());
+    rb_vars.push_back(var_rb);
+    init_vars_map[var]=var_init;
+    exprt rhs=if_exprt(guard_ins,var_rb,var_init);
+    exp_vec.push_back(equal_exprt(var,rhs));
+  }
+  unsigned size=SSA.params.size()+SSA.globals_in.size(),n=size;
+  for(unsigned i=0;i<size;i++)
+  {
+    exp_vec.push_back(equal_exprt(in_vars_vec.at(i),expr_vec.at(i)));
+  }
+  size=SSA.globals_out.size();
+  for(unsigned i=0;i<size;i++)
+  {
+    exp_vec.push_back(equal_exprt(out_vars_vec.at(i),expr_vec.at(i+n)));
+  }
+  merge_expr=conjunction(exp_vec);
+  merge_guard=disjunction(guards_vec);
+}
+
+void template_gen_rec_summaryt::collect_inout_vars(
+  const local_SSAt &SSA,
+  bool forward)
+{
+  // add params and globals_in
+  exprt first_guard=
+    SSA.guard_symbol(SSA.goto_function.body.instructions.begin());
+  add_vars(
+    in_vars_vec,
+    merge_guard,
+    and_exprt(first_guard,guard_ins),
+    forward ? domaint::IN : domaint::OUT,
+    var_specs);
+
+  // add globals_out (includes return values)
+  exprt last_guard=
+    SSA.guard_symbol(--SSA.goto_function.body.instructions.end());
+  add_vars(
+    out_vars_vec,
+    merge_guard,
+    last_guard,
+    forward ? domaint::OUT : domaint::IN,
+    var_specs);
+  
+  std::vector<symbol_exprt>::const_iterator v_it=rb_vars.begin();
+  local_SSAt::var_sett::const_iterator out=SSA.globals_out.begin();
+  for(domaint::var_spect var_spec:var_specs)
+  {
+    if(var_spec.kind==domaint::OUT)
+    {
+      post_renaming_map[var_spec.var]=*out;
+      out++;
+    }
+    else
+    {
+      post_renaming_map[var_spec.var]=*v_it;
+      post_renaming_map[*v_it]=var_spec.var;      
+      v_it++;
+    }
+  }
+  for(domaint::var_spect var_spec:var_specs)
+  {
+    if(var_spec.kind==domaint::OUT) break;
+    var_spec.pre_guard=and_exprt(first_guard,guard_ins);
+    var_spec.post_guard=merge_guard;
+    var_spec.var=post_renaming_map[var_spec.var];
+    var_specs_no_out.push_back(var_spec);
+  }
+}
+
+void template_gen_rec_summaryt::instantiate_template_for_rec(local_SSAt SSA)
+{
+  replace_mapt &renaming_map=
+    std_invariants ? aux_renaming_map : post_renaming_map;
+  domain_ptr=
+      new tpolyhedra_domaint(domain_number, renaming_map, SSA.ns,true);
+  filter_template_domain();
+
+  //IN templates  
+  static_cast<tpolyhedra_domaint *>(domain_ptr)
+      ->add_interval_template(var_specs_no_out, SSA.ns,
+                              options.get_bool_option("context-sensitive"));
+  static_cast<tpolyhedra_domaint *>(domain_ptr)
+      ->add_sum_template(var_specs_no_out, SSA.ns, false);
+  static_cast<tpolyhedra_domaint *>(domain_ptr)
+      ->add_difference_template(var_specs_no_out, SSA.ns, false);
+  //OUT templates
+  static_cast<tpolyhedra_domaint *>(domain_ptr)
+      ->add_sum_template(var_specs, SSA.ns);
+  static_cast<tpolyhedra_domaint *>(domain_ptr)
+      ->add_difference_template(var_specs, SSA.ns);
+}
\ No newline at end of file
diff --git a/src/domains/template_gen_rec_summary.h b/src/domains/template_gen_rec_summary.h
new file mode 100644
index 000000000..3e845dcf7
--- /dev/null
+++ b/src/domains/template_gen_rec_summary.h
@@ -0,0 +1,48 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   template_gen_rec_summary.h
+ * Author: sarbojit
+ *
+ * Created on 19 March, 2018, 10:19 PM
+ */
+
+#ifndef TEMPLATE_GEN_REC_SUMMARY_H
+#define TEMPLATE_GEN_REC_SUMMARY_H
+
+#include "template_generator_summary.h"
+
+class template_gen_rec_summaryt:public template_generator_summaryt {
+public:
+  typedef std::vector<std::pair<exprt,std::vector<exprt>>> tmpl_rename_mapt;
+  explicit template_gen_rec_summaryt(
+   optionst &_options,
+   ssa_dbt &_ssa_db,
+   ssa_local_unwindert &_ssa_local_unwinder):
+   template_generator_summaryt(_options, _ssa_db, _ssa_local_unwinder)
+  {
+  }
+  virtual void operator()(const irep_idt &function_name,
+    unsigned _domain_number,
+    const local_SSAt &SSA,
+    exprt &merge_exprt,
+    bool forward=true);
+    
+  void merge_vars(const irep_idt &function_name,
+    const local_SSAt &SSA,
+    exprt& merge_expr);
+  void collect_inout_vars(const local_SSAt &SSA, bool forward);
+  void instantiate_template_for_rec(local_SSAt SSA);
+  replace_mapt init_vars_map;
+  domaint::var_specst var_specs_no_out;
+  private:
+    exprt merge_guard,guard_ins;
+    std::vector<symbol_exprt> in_vars_vec,out_vars_vec,rb_vars;
+};
+
+#endif /* TEMPLATE_GEN_REC_SUMMARY_H */
+
diff --git a/src/domains/template_generator_base.cpp b/src/domains/template_generator_base.cpp
index f9a56e7bd..628edeefe 100644
--- a/src/domains/template_generator_base.cpp
+++ b/src/domains/template_generator_base.cpp
@@ -150,7 +150,7 @@ void template_generator_baset::collect_variables_loop(
   bool forward)
 {
   // used for renaming map
-  var_listt pre_state_vars, post_state_vars;
+  //var_listt pre_state_vars, post_state_vars;
 
   // add loop variables
   for(local_SSAt::nodest::const_iterator n_it=SSA.nodes.begin();
diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp
index dbbecde6e..7c99a77a5 100644
--- a/src/domains/tpolyhedra_domain.cpp
+++ b/src/domains/tpolyhedra_domain.cpp
@@ -46,7 +46,7 @@ void tpolyhedra_domaint::initialize(valuet &value)
   v.resize(templ.size());
   for(std::size_t row=0; row<templ.size(); row++)
   {
-    if(templ[row].kind==IN)
+    if(templ[row].kind==IN&&!recursive)
       v[row]=true_exprt(); // marker for oo
     else
       v[row]=false_exprt(); // marker for -oo
@@ -225,7 +225,7 @@ Function: tpolyhedra_domaint::get_row_constraint
 
 \*******************************************************************/
 
-exprt tpolyhedra_domaint::get_row_constraint(
+exprt tpolyhedra_domaint::get_row_constraint(//enum
   const rowt &row,
   const row_valuet &row_value)
 {
@@ -254,20 +254,25 @@ Function: tpolyhedra_domaint::get_row_pre_constraint
 
 exprt tpolyhedra_domaint::get_row_pre_constraint(
   const rowt &row,
-  const row_valuet &row_value)
+  const row_valuet &row_value,
+  bool no_out)
 {
   assert(row<templ.size());
   const template_rowt &templ_row=templ[row];
   kindt k=templ_row.kind;
-  if(k==OUT || k==OUTL)
+  if((k==OUT || k==OUTL) && (!recursive || no_out))
     return true_exprt();
   if(is_row_value_neginf(row_value))
+  {
     return implies_exprt(templ_row.pre_guard, false_exprt());
+  }
   if(is_row_value_inf(row_value))
     return implies_exprt(templ_row.pre_guard, true_exprt());
-  return implies_exprt(
+  exprt c=implies_exprt(
     templ_row.pre_guard,
     binary_relation_exprt(templ_row.expr, ID_le, row_value));
+  //if((k==OUT || k==OUTL) && recursive) rename(c);
+  return c;
 }
 
 /*******************************************************************\
@@ -282,13 +287,13 @@ Function: tpolyhedra_domaint::get_row_pre_constraint
 
 \*******************************************************************/
 
-exprt tpolyhedra_domaint::get_row_pre_constraint(
+/*exprt tpolyhedra_domaint::get_row_pre_constraint(
   const rowt &row,
   const templ_valuet &value)
 {
   assert(value.size()==templ.size());
   return get_row_pre_constraint(row, value[row]);
-}
+}*/
 
 /*******************************************************************\
 
@@ -304,11 +309,13 @@ Function: tpolyhedra_domaint::get_row_post_constraint
 
 exprt tpolyhedra_domaint::get_row_post_constraint(
   const rowt &row,
-  const row_valuet &row_value)
+  const row_valuet &row_value,
+  bool no_out)
 {
   assert(row<templ.size());
   const template_rowt &templ_row=templ[row];
-  if(templ_row.kind==IN)
+  if((templ_row.kind==IN && !recursive) ||
+     ((templ_row.kind==OUT || templ_row.kind==OUTL) && no_out))
     return true_exprt();
 
 #if 0 // TEST for disjunctive domains
@@ -350,7 +357,7 @@ exprt tpolyhedra_domaint::get_row_post_constraint(
   exprt c=implies_exprt(
     templ_row.post_guard,
     binary_relation_exprt(templ_row.expr, ID_le, row_value));
-  if(templ_row.kind==LOOP)
+  if(templ_row.kind==LOOP || recursive)//sarbojit
     rename(c);
   return c;
 }
@@ -369,10 +376,11 @@ exprt tpolyhedra_domaint::get_row_post_constraint(
 
 exprt tpolyhedra_domaint::get_row_post_constraint(
   const rowt &row,
-  const templ_valuet &value)
+  const templ_valuet &value,
+  bool no_out)
 {
   assert(value.size()==templ.size());
-  return get_row_post_constraint(row, value[row]);
+  return get_row_post_constraint(row, value[row],no_out);
 }
 
 /*******************************************************************\
@@ -387,13 +395,14 @@ exprt tpolyhedra_domaint::get_row_post_constraint(
 
 \*******************************************************************/
 
-exprt tpolyhedra_domaint::to_pre_constraints(const templ_valuet &value)
+exprt tpolyhedra_domaint::to_pre_constraints(const templ_valuet &value,
+  bool no_out)//sarbojit
 {
   assert(value.size()==templ.size());
   exprt::operandst c;
   for(std::size_t row=0; row<templ.size(); ++row)
   {
-    c.push_back(get_row_pre_constraint(row, value[row]));
+    c.push_back(get_row_pre_constraint(row, value[row],no_out));//sarbojit
   }
   return conjunction(c);
 }
@@ -411,10 +420,11 @@ exprt tpolyhedra_domaint::to_pre_constraints(const templ_valuet &value)
 
 \*******************************************************************/
 
-void tpolyhedra_domaint::make_not_post_constraints(
+void tpolyhedra_domaint::make_not_post_constraints(//
   const templ_valuet &value,
   exprt::operandst &cond_exprs,
-  exprt::operandst &value_exprs)
+  exprt::operandst &value_exprs,
+  bool no_out)
 {
   assert(value.size()==templ.size());
   cond_exprs.resize(templ.size());
@@ -428,7 +438,7 @@ void tpolyhedra_domaint::make_not_post_constraints(
     cond_exprs[row]=
       and_exprt(
         templ[row].aux_expr,
-        not_exprt(get_row_post_constraint(row, value)));
+        not_exprt(get_row_post_constraint(row, value, no_out)));
   }
 }
 
@@ -444,7 +454,7 @@ void tpolyhedra_domaint::make_not_post_constraints(
 
 \*******************************************************************/
 
-symbol_exprt tpolyhedra_domaint::get_row_symb_value(const rowt &row)
+symbol_exprt tpolyhedra_domaint::get_row_symb_value(const rowt &row)//
 {
   assert(row<templ.size());
   return symbol_exprt(
@@ -470,11 +480,14 @@ exprt tpolyhedra_domaint::get_row_symb_pre_constraint(
 {
   assert(row<templ.size());
   const template_rowt &templ_row=templ[row];
-  if(templ_row.kind==OUT || templ_row.kind==OUTL)
+  if((templ_row.kind==OUT || templ_row.kind==OUTL) && !recursive)
     return true_exprt();
-  return implies_exprt(
+  exprt c=implies_exprt(
     templ_row.pre_guard,  // REMARK: and_expr==> loop15 regression
     binary_relation_exprt(templ_row.expr, ID_le, get_row_symb_value(row)));
+  //if((templ_row.kind==OUT || templ_row.kind==OUTL) && recursive)
+  //  rename(c);
+  return c;
 }
 
 /*******************************************************************\
@@ -489,16 +502,17 @@ exprt tpolyhedra_domaint::get_row_symb_pre_constraint(
 
 \*******************************************************************/
 
-exprt tpolyhedra_domaint::get_row_symb_post_constraint(const rowt &row)
+exprt tpolyhedra_domaint::get_row_symb_post_constraint(const rowt &row)//
 {
   assert(row<templ.size());
   const template_rowt &templ_row=templ[row];
-  if(templ_row.kind==IN)
+  if(templ_row.kind==IN && !recursive)
     return true_exprt();
   exprt c=and_exprt(
     templ_row.post_guard,
     binary_relation_exprt(templ_row.expr, ID_ge, get_row_symb_value(row)));
-  rename(c);
+  //if(templ_row.kind!=OUT && templ_row.kind!=OUTL && recursive)
+    rename(c);
   return and_exprt(templ_row.aux_expr, c);
 }
 
@@ -514,7 +528,7 @@ exprt tpolyhedra_domaint::get_row_symb_post_constraint(const rowt &row)
 
 \*******************************************************************/
 
-exprt tpolyhedra_domaint::to_symb_pre_constraints(const templ_valuet &value)
+/*exprt tpolyhedra_domaint::to_symb_pre_constraints(const templ_valuet &value)
 {
   assert(value.size()==templ.size());
   exprt::operandst c;
@@ -523,7 +537,7 @@ exprt tpolyhedra_domaint::to_symb_pre_constraints(const templ_valuet &value)
     c.push_back(get_row_symb_pre_constraint(row, value[row]));
   }
   return conjunction(c);
-}
+}*/
 
 /*******************************************************************\
 
@@ -539,7 +553,8 @@ exprt tpolyhedra_domaint::to_symb_pre_constraints(const templ_valuet &value)
 
 exprt tpolyhedra_domaint::to_symb_pre_constraints(
   const templ_valuet &value,
-  const std::set<rowt> &symb_rows)
+  const std::set<rowt> &symb_rows,
+  bool no_out)
 {
   assert(value.size()==templ.size());
   exprt::operandst c;
@@ -548,7 +563,7 @@ exprt tpolyhedra_domaint::to_symb_pre_constraints(
     if(symb_rows.find(row)!=symb_rows.end())
       c.push_back(get_row_symb_pre_constraint(row, value[row]));
     else
-      c.push_back(get_row_pre_constraint(row, value[row]));
+      c.push_back(get_row_pre_constraint(row, value[row], no_out));
   }
   return conjunction(c);
 }
@@ -565,7 +580,7 @@ exprt tpolyhedra_domaint::to_symb_pre_constraints(
 
 \*******************************************************************/
 
-exprt tpolyhedra_domaint::to_symb_post_constraints(
+/*exprt tpolyhedra_domaint::to_symb_post_constraints(
   const std::set<rowt> &symb_rows)
 {
   exprt::operandst c;
@@ -574,7 +589,7 @@ exprt tpolyhedra_domaint::to_symb_post_constraints(
     c.push_back(get_row_symb_post_constraint(row));
   }
   return conjunction(c);
-}
+}*/
 
 /*******************************************************************\
 
@@ -588,7 +603,7 @@ exprt tpolyhedra_domaint::to_symb_post_constraints(
 
 \*******************************************************************/
 
-exprt tpolyhedra_domaint::get_row_symb_value_constraint(
+exprt tpolyhedra_domaint::get_row_symb_value_constraint(//
   const rowt &row,
   const row_valuet &row_value,
   bool geq)
@@ -684,7 +699,7 @@ void tpolyhedra_domaint::project_on_vars(
             templ_row.pre_guard,
             binary_relation_exprt(templ_row.expr, ID_le, row_v)));
     }
-    else
+    else //if(templ_row.kind!=IN)//sarbojit
     {
       if(is_row_value_neginf(row_v))
         c.push_back(false_exprt());
@@ -848,25 +863,39 @@ void tpolyhedra_domaint::output_domain(
   for(std::size_t row=0; row<templ.size(); ++row)
   {
     const template_rowt &templ_row=templ[row];
-    switch(templ_row.kind)
+    //sarbojit---
+    if(recursive)
     {
-    case LOOP:
-      out << "(LOOP) [ " << from_expr(ns, "", templ_row.pre_guard) << " | ";
-      out << from_expr(ns, "", templ_row.post_guard) << " | ";
-      out << from_expr(ns, "", templ_row.aux_expr) << " ]===> "
-          << std::endl << "      ";
-      break;
-    case IN:
-      out << "(IN)   ";
-      out << from_expr(ns, "", templ_row.pre_guard) << "===> "
-          << std::endl << "      ";
-      break;
-    case OUT: case OUTL:
-      out << "(OUT)  ";
-      out << from_expr(ns, "", templ_row.post_guard) << "===> "
-          << std::endl << "      ";
-      break;
-    default: assert(false);
+      if(templ_row.kind==IN) out << "(IN";
+      if(templ_row.kind==OUT) out << "(OUT";
+      if(templ_row.kind==LOOP) out << "(LOOP";
+      out << ") [ " << from_expr(ns, "", templ_row.pre_guard) << " | ";
+      out << from_expr(ns, "", templ_row.post_guard) << " ]===> ";
+      out << std::endl << "      ";
+    }
+    //---sarbojit
+    else//sarbojit
+    {
+      switch(templ_row.kind)
+      {
+      case LOOP:
+        out << "(LOOP) [ " << from_expr(ns, "", templ_row.pre_guard) << " | ";
+        out << from_expr(ns, "", templ_row.post_guard) << " | ";
+        out << from_expr(ns, "", templ_row.aux_expr) << " ]===> "
+            << std::endl << "      ";
+        break;
+      case IN:
+        out << "(IN)   ";
+        out << from_expr(ns, "", templ_row.pre_guard) << "===> "
+            << std::endl << "      ";
+        break;
+      case OUT: case OUTL:
+        out << "(OUT)  ";
+        out << from_expr(ns, "", templ_row.post_guard) << "===> "
+            << std::endl << "      ";
+        break;
+      default: assert(false);
+      }
     }
     out << "( " <<
       from_expr(ns, "", templ_row.expr) << "<=CONST )" << std::endl;
@@ -1000,14 +1029,15 @@ tpolyhedra_domaint::template_rowt &tpolyhedra_domaint::add_template_row(
 
 void tpolyhedra_domaint::add_interval_template(
   const var_specst &var_specs,
-  const namespacet &ns)
+  const namespacet &ns,
+  bool rec_cntx_sensitive)
 {
   unsigned size=2*var_specs.size();
   templ.reserve(templ.size()+size);
 
   for(const auto v : var_specs)
-  {
-    if(v.kind==IN)
+  {//for context sensitive analysis of recursive function
+    if(v.kind==IN && !rec_cntx_sensitive)
       continue;
     if(v.var.type().id()==ID_pointer)
       continue;
@@ -1044,7 +1074,8 @@ void tpolyhedra_domaint::add_interval_template(
 
 void tpolyhedra_domaint::add_difference_template(
   const var_specst &var_specs,
-  const namespacet &ns)
+  const namespacet &ns,
+  bool no_in)
 {
   std::size_t size=var_specs.size()*(var_specs.size()-1);
   templ.reserve(templ.size()+size);
@@ -1059,7 +1090,7 @@ void tpolyhedra_domaint::add_difference_template(
     for(; v2!=var_specs.end(); ++v2)
     {
       kindt k=domaint::merge_kinds(v1->kind, v2->kind);
-      if(k==IN)
+      if(k==IN&&no_in)
         continue;
       if(k==LOOP && v1->pre_guard!=v2->pre_guard)
         continue; // TEST: we need better heuristics
@@ -1140,7 +1171,8 @@ Function: tpolyhedra_domaint::add_sum_template
 
 void tpolyhedra_domaint::add_sum_template(
   const var_specst &var_specs,
-  const namespacet &ns)
+  const namespacet &ns,
+  bool no_in)
 {
   unsigned size=var_specs.size()*(var_specs.size()-1);
   templ.reserve(templ.size()+size);
@@ -1152,7 +1184,7 @@ void tpolyhedra_domaint::add_sum_template(
     for(; v2!=var_specs.end(); ++v2)
     {
       kindt k=domaint::merge_kinds(v1->kind, v2->kind);
-      if(k==IN)
+      if(k==IN&&no_in)
         continue;
       if(k==LOOP && v1->pre_guard!=v2->pre_guard)
         continue; // TEST: we need better heuristics
@@ -1218,4 +1250,4 @@ void tpolyhedra_domaint::eliminate_sympaths(
                  ? true_exprt()
                  : static_cast<exprt>(not_exprt(disjunction(paths)));
   }
-}
+}
\ No newline at end of file
diff --git a/src/domains/tpolyhedra_domain.h b/src/domains/tpolyhedra_domain.h
index 42ca064c1..818dee437 100644
--- a/src/domains/tpolyhedra_domain.h
+++ b/src/domains/tpolyhedra_domain.h
@@ -43,8 +43,9 @@ class tpolyhedra_domaint:public domaint
   tpolyhedra_domaint(
     unsigned _domain_number,
     replace_mapt &_renaming_map,
-    const namespacet &_ns):
-    domaint(_domain_number, _renaming_map, _ns)
+    const namespacet &_ns,
+    bool rec=false):
+    domaint(_domain_number, _renaming_map, _ns, rec)
   {
   }
 
@@ -55,22 +56,27 @@ class tpolyhedra_domaint:public domaint
 
   // value -> constraints
   exprt get_row_constraint(const rowt &row, const row_valuet &row_value);
-  exprt get_row_pre_constraint(const rowt &row, const row_valuet &row_value);
-  exprt get_row_post_constraint(const rowt &row, const row_valuet &row_value);
+  exprt get_row_pre_constraint(const rowt &row, const row_valuet &row_value,
+    bool no_out=false);
+  exprt get_row_post_constraint(const rowt &row, const row_valuet &row_value,
+    bool no_out=false);
   exprt get_row_pre_constraint(const rowt &row, const templ_valuet &value);
-  exprt get_row_post_constraint(const rowt &row, const templ_valuet &value);
+  exprt get_row_post_constraint(const rowt &row, const templ_valuet &value,
+    bool no_out=false);
 
-  exprt to_pre_constraints(const templ_valuet &value);
+  exprt to_pre_constraints(const templ_valuet &value,bool no_out=false);
   void make_not_post_constraints(
     const templ_valuet &value,
     exprt::operandst &cond_exprs,
-    exprt::operandst &value_exprs);
+    exprt::operandst &value_exprs,
+    bool no_out=false);
 
   // value -> symbolic bound constraints (for optimization)
   exprt to_symb_pre_constraints(const templ_valuet &value);
   exprt to_symb_pre_constraints(
     const templ_valuet &value,
-    const std::set<rowt> &symb_rows);
+    const std::set<rowt> &symb_rows,
+    bool no_out=false);
   exprt to_symb_post_constraints(const std::set<rowt> &symb_rows);
   exprt get_row_symb_value_constraint(
     const rowt &row,
@@ -124,13 +130,16 @@ class tpolyhedra_domaint:public domaint
 
   void add_interval_template(
     const var_specst &var_specs,
-    const namespacet &ns);
+    const namespacet &ns,
+    bool rec_cntx_sensitive=false);
   void add_difference_template(
     const var_specst &var_specs,
-    const namespacet &ns);
+    const namespacet &ns,
+    bool no_in=true);
   void add_sum_template(
     const var_specst &var_specs,
-    const namespacet &ns);
+    const namespacet &ns,
+    bool no_in=true);
   void add_quadratic_template(
     const var_specst &var_specs,
     const namespacet &ns);
diff --git a/src/solver/Makefile b/src/solver/Makefile
index bd0fe97b7..ada270d7c 100644
--- a/src/solver/Makefile
+++ b/src/solver/Makefile
@@ -1,6 +1,7 @@
 SRC = summarizer_base.cpp  summarizer_bw.cpp	\
       summarizer_bw_term.cpp	summarizer_fw_contexts.cpp \
       summarizer_fw.cpp  summarizer_fw_term.cpp  \
+      summarizer_rec_fw.cpp \
       summary.cpp  summary_db.cpp
 
 include ../config.inc
diff --git a/src/solver/summarizer_fw.cpp b/src/solver/summarizer_fw.cpp
index 27f8dd1da..7d3370084 100644
--- a/src/solver/summarizer_fw.cpp
+++ b/src/solver/summarizer_fw.cpp
@@ -214,8 +214,9 @@ void summarizer_fwt::inline_summaries(
         f_it!=n_it->function_calls.end(); f_it++)
     {
       assert(f_it->function().id()==ID_symbol); // no function pointers
-      if(!check_call_reachable(
-           function_name, SSA, n_it, f_it, precondition, true))
+      if(to_symbol_expr(f_it->function()).get_identifier()==function_name ||
+          !check_call_reachable(
+            function_name, SSA, n_it, f_it, precondition, true))
       {
         continue;
       }
diff --git a/src/solver/summarizer_fw.h b/src/solver/summarizer_fw.h
index 6ee541620..a57f4636f 100644
--- a/src/solver/summarizer_fw.h
+++ b/src/solver/summarizer_fw.h
@@ -39,7 +39,7 @@ class summarizer_fwt:public summarizer_baset
     const exprt &precondition,
     bool context_sensitive);
 
-  void inline_summaries(
+  virtual void inline_summaries(
     const function_namet &function_name,
     local_SSAt &SSA,
     const exprt &precondition,
diff --git a/src/solver/summarizer_rec_fw.cpp b/src/solver/summarizer_rec_fw.cpp
new file mode 100755
index 000000000..4157908b8
--- /dev/null
+++ b/src/solver/summarizer_rec_fw.cpp
@@ -0,0 +1,204 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   summarizer_rec_fwt.cpp
+ * Author: sarbojit
+ * 
+ * Created on 13 March, 2018, 4:53 PM
+ */
+
+#include <domains/ssa_analyzer.h>
+#include <domains/template_gen_rec_summary.h>
+#include <algorithm>
+#include "summarizer_rec_fw.h"
+
+void summarizer_rec_fwt::compute_summary_rec(
+  const function_namet &function_name,
+  const exprt &precondition,
+  bool context_sensitive)
+{
+  local_SSAt &SSA=ssa_db.get(function_name);// TODO: make const
+    
+  bool recursive=false;
+  for(local_SSAt::nodet node:SSA.nodes)
+  {
+    for(function_application_exprt f_call:node.function_calls)
+      if(function_name==to_symbol_expr(f_call.function()).get_identifier() &&
+         f_call.function().id()==ID_symbol)//No function pointer
+        recursive=true;
+  }
+  if(recursive)//if this_function_is_recursive
+  {
+    status()<<"Function "<<function_name.c_str()<<" is recursive"<<eom;
+    //inline other non-recursive functions in the same SCC of the call graph
+    //this makes it self recursive
+  }
+    
+  // recursively compute summaries for non-recursive function calls
+  inline_summaries(function_name, SSA, precondition, context_sensitive);
+  
+  status() << "Analyzing function "  << function_name << eom;
+  #if 0
+  {
+    std::ostringstream out;
+    out << "Function body for " << function_name
+        << " to be analyzed: " << std::endl;
+    for(const auto &node : SSA.nodes)
+    {
+      if(!node.empty())
+      node.output(out, SSA.ns);
+    }
+    out << "(enable) " << from_expr(SSA.ns, "", SSA.get_enabling_exprs())
+        << "\n";
+    debug() << out.str() << eom;
+  }
+  #endif
+
+  // create summary
+  summaryt summary;
+  summary.params=SSA.params;
+  summary.globals_in=SSA.globals_in;
+  summary.globals_out=SSA.globals_out;
+  //if(recursive) summary.fw_precondition=true;
+  summary.fw_precondition=precondition;
+  
+  if(!options.get_bool_option("havoc"))
+  {
+    do_summary(function_name, SSA, summary,
+               true_exprt(),context_sensitive, recursive);
+  }
+
+  #if 0
+  if(!options.get_bool_option("competition-mode"))
+  {
+    std::ostringstream out;
+    out << std::endl << "Summary for function " << function_name << std::endl;
+    summary.output(out, SSA.ns);
+    status() << out.str() << eom;
+  }
+  #endif
+
+  // store summary in db
+  summary_db.put(function_name, summary);
+
+  if(!options.get_bool_option("competition-mode"))
+  {
+    std::ostringstream out;
+    out << std::endl << "Summary for function " << function_name << std::endl;
+    summary_db.get(function_name).output(out, SSA.ns);
+    status() << out.str() << eom;
+  }
+}
+
+void summarizer_rec_fwt::do_summary(
+  const function_namet &function_name,
+  local_SSAt &SSA,
+  summaryt &summary,
+  exprt cond,
+  bool context_sensitive,
+  bool recursive)
+{
+  status() << "Computing summary" << eom;
+  
+  // solver
+  incremental_solvert &solver=ssa_db.get_solver(function_name);
+  solver.set_message_handler(get_message_handler());
+  
+  // analyze
+  ssa_analyzert analyzer;
+  analyzer.set_message_handler(get_message_handler());
+  
+  if(recursive)
+  {
+    exprt merge_expr;
+    template_gen_rec_summaryt template_generator=template_gen_rec_summaryt(
+    options, ssa_db, ssa_unwinder.get(function_name));
+    template_generator.set_message_handler(get_message_handler());
+    template_generator(function_name, solver.next_domain_number(),
+     SSA, merge_expr, true);
+    
+    exprt precond(summary.fw_precondition);
+    if(context_sensitive)
+      replace_expr(template_generator.init_vars_map,precond);
+    
+    exprt::operandst conds;
+    conds.reserve(5);
+    conds.push_back(cond);
+    conds.push_back(precond);
+    conds.push_back(ssa_inliner.get_summaries(SSA));
+    cond=conjunction(conds);
+    
+    analyzer(solver, SSA, cond, template_generator, true, merge_expr);
+    analyzer.get_result(summary.fw_transformer, template_generator.inout_vars());
+    analyzer.get_result(summary.fw_invariant, template_generator.loop_vars());
+  }
+  else
+  {
+    template_generator_summaryt template_generator=template_generator_summaryt(
+    options, ssa_db, ssa_unwinder.get(function_name));
+    template_generator.set_message_handler(get_message_handler());
+    template_generator(solver.next_domain_number(),
+     SSA, true);
+    exprt::operandst conds;
+    conds.reserve(5);
+    conds.push_back(cond);
+    conds.push_back(summary.fw_precondition);
+    conds.push_back(ssa_inliner.get_summaries(SSA));
+  
+#ifdef REUSE_INVARIANTS
+  if(summary_db.exists(function_name)) // reuse existing invariants
+  {
+    const exprt &old_inv=summary_db.get(function_name).fw_invariant;
+    exprt inv=ssa_unwinder.get(function_name).rename_invariant(old_inv);
+    conds.push_back(inv);
+
+#if 0
+    std::ostringstream out;
+    out << "(original inv)" << from_expr(SSA.ns, "", old_inv) << "\n";
+    debug() << out.str() << eom;
+    out << "(renamed inv)" << from_expr(SSA.ns, "", inv) << "\n";
+    debug() << out.str() << eom;
+#endif
+  }
+#endif
+  
+    cond=conjunction(conds);
+
+    analyzer(solver, SSA, cond, template_generator);
+    analyzer.get_result(summary.fw_transformer, template_generator.inout_vars());
+    analyzer.get_result(summary.fw_invariant, template_generator.loop_vars());
+  }
+  
+#ifdef SHOW_WHOLE_RESULT
+  // to see all the custom template values
+  exprt whole_result;
+  analyzer.get_result(whole_result, template_generator.all_vars());
+  debug() << "whole result: " << from_expr(SSA.ns, "", whole_result) << eom;
+#endif
+  
+  if(options.get_bool_option("heap"))
+  {
+    analyzer.update_heap_out(summary.globals_out);
+    const exprt advancer_bindings=analyzer.input_heap_bindings();
+    if(!advancer_bindings.is_true())
+    {
+      summary.aux_precondition=advancer_bindings;
+    }
+  }
+
+
+  if(context_sensitive && !summary.fw_precondition.is_true())
+  {
+    summary.fw_transformer=
+      implies_exprt(summary.fw_precondition, summary.fw_transformer);
+    summary.fw_invariant=
+      implies_exprt(summary.fw_precondition, summary.fw_invariant);
+  }
+
+  solver_instances+=analyzer.get_number_of_solver_instances();
+  solver_calls+=analyzer.get_number_of_solver_calls();
+}
diff --git a/src/solver/summarizer_rec_fw.h b/src/solver/summarizer_rec_fw.h
new file mode 100755
index 000000000..df335de87
--- /dev/null
+++ b/src/solver/summarizer_rec_fw.h
@@ -0,0 +1,49 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   summarizer_rec_fwt.h
+ * Author: sarbojit
+ *
+ * Created on 13 March, 2018, 4:52 PM
+ */
+
+#ifndef SUMMARIZER_REC_FWT_H
+#define SUMMARIZER_REC_FWT_H
+
+#include <util/message.h>
+#include <util/options.h>
+#include <util/time_stopping.h>
+
+#include <ssa/ssa_inliner.h>
+#include <ssa/ssa_unwinder.h>
+#include <ssa/local_ssa.h>
+#include <ssa/ssa_db.h>
+
+#include "summarizer_fw.h"
+
+class summarizer_rec_fwt:public summarizer_fwt {
+public:
+    explicit summarizer_rec_fwt(optionst &_options,
+    summary_dbt &_summary_db,
+    ssa_dbt &_ssa_db,
+    ssa_unwindert &_ssa_unwinder,
+    ssa_inlinert &_ssa_inliner):
+    summarizer_fwt(
+      _options, _summary_db, _ssa_db, _ssa_unwinder, _ssa_inliner)
+  {
+  }
+protected:
+    virtual void compute_summary_rec(const function_namet &,
+            const exprt &, bool);
+
+    virtual void do_summary(const function_namet &,
+     local_SSAt &SSA, summaryt &summary, exprt cond,
+     bool context_sensitive, bool recursive);
+};
+
+#endif /* SUMMARIZER_REC_FWT_H */
+
diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp
index 6ca775df8..e0d106440 100644
--- a/src/ssa/local_ssa.cpp
+++ b/src/ssa/local_ssa.cpp
@@ -578,16 +578,12 @@ void local_SSAt::build_function_call(locationt loc)
     unsigned i=0;
     for(exprt &a : f.arguments())
     {
-      if(a.is_constant() ||
-         (a.id()==ID_typecast && to_typecast_expr(a).op().is_constant()))
-      {
-        const std::string arg_name=
-          id2string(fname)+"#arg"+i2string(i)+"#"+
-            i2string(loc->location_number);
-        symbol_exprt arg(arg_name, a.type());
-        n_it->equalities.push_back(equal_exprt(a, arg));
-        a=arg;
-      }
+      const std::string arg_name=
+        id2string(fname)+"#arg"+i2string(i)+"#"+
+          i2string(loc->location_number);
+      symbol_exprt arg(arg_name, a.type());
+      n_it->equalities.push_back(equal_exprt(a, arg));
+      a=arg;
       ++i;
     }