diff --git a/headers/gensym/state_tsnt.hpp b/headers/gensym/state_tsnt.hpp
index 6ac113d7..3e45e21c 100644
--- a/headers/gensym/state_tsnt.hpp
+++ b/headers/gensym/state_tsnt.hpp
@@ -163,13 +163,15 @@ class Frame {
   public:
     using Env = std::map<Id, PtrVal>;
     using Cont = std::function<std::monostate(SS&, PtrVal)>;
-    Cont cont;
+    size_t prev_stack_size;
+    Cont k;
   private:
     Env env;
   public:
-    Frame(Cont ct): cont(ct), env() {}
+    Frame() : env() {}
     Frame(Env env) : env(std::move(env)) {}
-    Frame() : env(std::map<Id, PtrVal>{}) {}
+    Frame(size_t ss, Cont k): prev_stack_size(ss), k(k), env() {}
+
     size_t size() { return env.size(); }
     PtrVal lookup_id(Id id) const { return env.at(id); }
     Frame&& assign(Id id, PtrVal v) {
@@ -204,12 +206,16 @@ class Stack {
       return std::move(*this);
     }
     PtrVal error_loc() { return errno_location; }
-    typename Frame::Cont pop(size_t keep) {
-      auto &it = env.at(env.size() - 1);
-      auto ret = it.cont;
+    Stack&& pop(size_t keep) {
       mem.take(keep);
       env.take(env.size() - 1);
-      return ret;
+      return std::move(*this);
+    }
+    std::monostate pop(SS& s, PtrVal v) {
+      auto f = env.at(env.size() - 1);
+      mem.take(f.prev_stack_size);
+      env.take(env.size() - 1);
+      return f.k(s, v);
     }
     Stack&& push() {
       return push(Frame());
@@ -218,8 +224,8 @@ class Stack {
       env.push_back(std::move(f));
       return std::move(*this);
     }
-    Stack&& push(std::function<std::monostate(SS&, PtrVal)> cont) {
-      return push(Frame(cont));
+    Stack&& push(size_t ss, std::function<std::monostate(SS&, PtrVal)> k) {
+      return push(Frame(ss, k));
     }
 
     Stack&& assign(Id id, PtrVal val) {
@@ -382,10 +388,10 @@ class SS {
       return read_res;
     }
     PtrVal at_simpl(PtrVal addr) {
-        auto loc = addr->to_LocV();
-        ASSERT(loc != nullptr, "Lookup an non-address value");
-        if (loc->k == LocV::kStack) return stack.at(loc->l);
-        return heap.at(loc->l);
+      auto loc = addr->to_LocV();
+      ASSERT(loc != nullptr, "Lookup an non-address value");
+      if (loc->k == LocV::kStack) return stack.at(loc->l);
+      return heap.at(loc->l);
     }
     PtrVal at(PtrVal addr, size_t size) {
       if (auto loc = addr->to_LocV()) {
@@ -461,12 +467,16 @@ class SS {
       stack.push();
       return std::move(*this);
     }
-    SS&& push(std::function<std::monostate(SS&, PtrVal)> cont) {
-      stack.push(cont);
+    SS&& push(size_t ss, std::function<std::monostate(SS&, PtrVal)> cont) {
+      stack.push(ss, cont);
+      return std::move(*this);
+    }
+    SS&& pop(size_t keep) {
+      stack.pop(keep);
       return std::move(*this);
     }
-    typename Frame::Cont pop(size_t keep) {
-      return stack.pop(keep);
+    std::monostate pop(PtrVal v) {
+      return stack.pop(*this, v);
     }
     SS&& assign(Id id, PtrVal val) {
       stack.assign(id, val);
@@ -586,8 +596,8 @@ inline std::monostate cps_apply(PtrVal v, SS ss, List<PtrVal> args, std::functio
   ABORT("cps_apply: not applicable");
 }
 
-inline std::monostate cont_apply(std::function<std::monostate(SS&, PtrVal)> cont, SS& ss, PtrVal val) {
-  return cont(ss, val);
+inline std::monostate pop_cont_apply(SS& ss, PtrVal val) {
+  return ss.pop(val);
 }
 
 #endif
diff --git a/src/main/scala/gensym/Codegen.scala b/src/main/scala/gensym/Codegen.scala
index b5ca43fe..cd3f380b 100644
--- a/src/main/scala/gensym/Codegen.scala
+++ b/src/main/scala/gensym/Codegen.scala
@@ -107,6 +107,34 @@ trait GenericGSCodeGen extends CppSAICodeGenBase {
     case _ => super.traverse(n)
   }
 
+  // Note: this enhances the EmitHelper in lms-clean, to be merged
+  implicit class EmitHelperExt(val sc: StringContext) {
+    def realEmit(x: Any): Unit = x match {
+      case (x: Def) => shallow(x)
+      case (n: Node) => shallow(n)
+      case (s: String) => emit(s)
+      case (i: Int) => emit(i.toString)
+      case (args: List[Def]) =>
+        if (args.nonEmpty) {
+          realEmit(args(0))
+          args.tail.foreach { arg => emit(", "); realEmit(arg) }
+        }
+    }
+    def es(args: Any*): Unit = {
+      val strings = sc.parts.iterator
+      val expressions = args.iterator
+      emit(strings.next)
+      while(strings.hasNext) {
+        realEmit(expressions.next)
+        emit(strings.next)
+      }
+    }
+    def esln(args: Any*): Unit = {
+      es(args:_*)
+      emitln()
+    }
+  }
+
   override def shallow(n: Node): Unit = n match {
     case n @ Node(s, "P", List(x), _) => es"std::cout << $x << std::endl"
     case Node(s,"kStack", _, _) => emit("LocV::kStack")
@@ -138,9 +166,8 @@ trait GenericGSCodeGen extends CppSAICodeGenBase {
     case Node(s, "ss-update", List(ss, k, v, sz), _) => es"$ss.update($k, $v, $sz)"
     case Node(s, "ss-update", List(ss, k, v), _) => es"$ss.update($k, $v)"
     case Node(s, "ss-update-seq", List(ss, k, v), _) => es"$ss.update_seq($k, $v)"
-    case Node(s, "ss-push", List(ss), _) => es"$ss.push()"
-    case Node(s, "ss-push", List(ss, k), _) => es"$ss.push($k)"
-    case Node(s, "ss-pop", List(ss, n), _) => es"$ss.pop($n)"
+    case Node(s, "ss-push", ss::args, _) => es"$ss.push($args)"
+    case Node(s, "ss-pop", ss::args, _) => es"$ss.pop($args)"
     case Node(s, "ss-addpc", List(ss, e), _) => es"$ss.add_PC($e)"
     case Node(s, "add-pc", List(pc, e), _) => es"$pc.add($e)"
     case Node(s, "ss-addpcset", List(ss, es), _) => es"$ss.add_PC_set($es)"
diff --git a/src/main/scala/gensym/EngineBase.scala b/src/main/scala/gensym/EngineBase.scala
index f0032565..e5c55994 100644
--- a/src/main/scala/gensym/EngineBase.scala
+++ b/src/main/scala/gensym/EngineBase.scala
@@ -58,10 +58,14 @@ trait EngineBase extends SAIOps { self: BasicDefs with ValueDefs =>
   def info(msg: String) = unchecked("INFO(\"" + msg + "\")")
 
   val mainRename = "gs_main"
-  def getRealFunName(funName: String): String = {
-    val newFname = if (funName != "@main") "__GS_USER_"+funName.tail else mainRename
-    newFname.replaceAllLiterally(".","_")
-  }
+  val gsPrefix = "__GS_USER_"
+
+  def getRealFunName(funName: String, prefix: String = gsPrefix): String =
+    if (funName != "@main") gsPrefix + funName.tail.replaceAllLiterally(".", "_")
+    else mainRename
+    
+  def strippedFunName(funName: String): String = getRealFunName(funName, "")
+
   def getRealBlockFunName(ctx: Ctx): String = blockNameMap(Counter.block.get(ctx.toString))
 
   def compile(funName: String, b: BB): Unit = {
@@ -100,7 +104,7 @@ trait EngineBase extends SAIOps { self: BasicDefs with ValueDefs =>
     }
     val fn = repExternFun(f, ret, argTypes)
     val node = Unwrap(fn).asInstanceOf[Backend.Sym]
-    funNameMap(node) = "__GS_NATIVE_EXTERNAL_"+mangledName.tail
+    funNameMap(node) = "__GS_NATIVE_"+mangledName.tail
     FunFuns(mangledName) = fn
   }
 
@@ -148,7 +152,6 @@ trait EngineBase extends SAIOps { self: BasicDefs with ValueDefs =>
         // "When indexing into a (optionally packed) structure, only i32 integer
         //  constants are allowed"
         // TODO: the align argument for getTySize
-        // TODO: test this
         val indexCst: List[Long] = index.map { case IntV(n, _) => n.toLong }
         IntV(calculateOffsetStatic(ty, indexCst), DEFAULT_INDEX_BW)
       case PackedStruct(types) =>
@@ -159,7 +162,7 @@ trait EngineBase extends SAIOps { self: BasicDefs with ValueDefs =>
   }
 
   // Note: we can also assign symbolic values here
-  def uninitValue: Rep[Value] = IntV(0, 8) //NullPtr()
+  def uninitValue: Rep[Value] = IntV(0, 8)
 
   def evalHeapAtomicConst(v: Constant, ty: LLVMType): Rep[Value] = v match {
     case BoolConst(b) => IntV(if (b) 1 else 0, 1)
diff --git a/src/main/scala/gensym/GenericDefs.scala b/src/main/scala/gensym/GenericDefs.scala
index 81793b93..3b12c53e 100644
--- a/src/main/scala/gensym/GenericDefs.scala
+++ b/src/main/scala/gensym/GenericDefs.scala
@@ -35,6 +35,7 @@ object Counter {
   val block = Counter()
   val variable = Counter()
   val function = Counter()
+  val cont = Counter()
   val branchStat: HashMap[Int, Int] = HashMap[Int, Int]()
   def setBranchNum(ctx: Ctx, n: Int): Unit = {
     val blockId = Counter.block.get(ctx.toString)
@@ -339,16 +340,16 @@ trait ValueDefs { self: SAIOps with BasicDefs with Opaques =>
   }
 
   object IntOp2 {
-    def applyNoOpt(op: String, o1: Rep[Value], o2: Rep[Value]): Rep[Value] =
+    def primOp2(op: String, o1: Rep[Value], o2: Rep[Value]): Rep[Value] =
       "int_op_2".reflectWith[Value](op, o1, o2)
-    def apply(op: String, o1: Rep[Value], o2: Rep[Value]): Rep[Value] =
-      if (!Config.opt) applyNoOpt(op, o1, o2)
-      else op match {
-        case "neq" => neq(o1, o2)
-        case "eq" => eq(o1, o2)
-        case "add" => add(o1, o2)
-        case _ => applyNoOpt(op, o1, o2)
-      }
+
+    def apply(op: String, o1: Rep[Value], o2: Rep[Value]): Rep[Value] = op match {
+      case "neq" => neq(o1, o2)
+      case "eq" => eq(o1, o2)
+      case "add" => add(o1, o2)
+      case "mul" => mul(o1, o2)
+      case _ => primOp2(op, o1, o2)
+    }
 
     def unapply(v: Rep[Value]): Option[(String, Rep[Value], Rep[Value])] = Unwrap(v) match {
       case gNode("int_op_2", bConst(x: String)::(o1: bSym)::(o2: bSym)::_) =>
@@ -357,32 +358,32 @@ trait ValueDefs { self: SAIOps with BasicDefs with Opaques =>
     }
 
     def add(v1: Rep[Value], v2: Rep[Value]): Rep[Value] = (v1, v2) match {
-      case (IntV(n1, bw1), IntV(n2, bw2)) if (bw1 == bw2) => IntV(n1 + n2, bw1)
-      case _ => applyNoOpt("add", v1, v2)
+      case (IntV(n1, bw1), IntV(n2, bw2)) if (bw1 == bw2) && Config.opt => IntV(n1 + n2, bw1)
+      case _ => primOp2("add", v1, v2)
     }
 
     def mul(v1: Rep[Value], v2: Rep[Value]): Rep[Value] = (v1, v2) match {
-      case (IntV(n1, bw1), IntV(n2, bw2)) if (bw1 == bw2) => IntV(n1 * n2, bw1)
-      case _ => applyNoOpt("mul", v1, v2)
+      case (IntV(n1, bw1), IntV(n2, bw2)) if (bw1 == bw2) && Config.opt => IntV(n1 * n2, bw1)
+      case _ => primOp2("mul", v1, v2)
     }
 
     def neq(o1: Rep[Value], o2: Rep[Value]): Rep[Value] = (Unwrap(o1), Unwrap(o2)) match {
       case (gNode("bv_sext", (e1: bExp)::bConst(bw1: Int)::_),
-            gNode("bv_sext", (e2: bExp)::bConst(bw2: Int)::_)) if bw1 == bw2 =>
+            gNode("bv_sext", (e2: bExp)::bConst(bw2: Int)::_)) if bw1 == bw2 && Config.opt =>
         val v1 = Wrap[Value](e1)
         val v2 = Wrap[Value](e2)
-        if (v1.bw == v2.bw) applyNoOpt("neq", v1, v2)
-        else applyNoOpt("neq", o1, o2)
-      case _ => applyNoOpt("neq", o1, o2)
+        if (v1.bw == v2.bw) neq(v1, v2)
+        else primOp2("neq", o1, o2)
+      case _ => primOp2("neq", o1, o2)
     }
     def eq(o1: Rep[Value], o2: Rep[Value]): Rep[Value] = (Unwrap(o1), Unwrap(o2)) match {
       case (gNode("bv_sext", (e1: bExp)::bConst(bw1: Int)::_),
-            gNode("bv_sext", (e2: bExp)::bConst(bw2: Int)::_)) if bw1 == bw2 =>
+            gNode("bv_sext", (e2: bExp)::bConst(bw2: Int)::_)) if bw1 == bw2 && Config.opt =>
         val v1 = Wrap[Value](e1)
         val v2 = Wrap[Value](e2)
-        if (v1.bw == v2.bw) applyNoOpt("eq", v1, v2)
-        else applyNoOpt("eq", o1, o2)
-      case _ => applyNoOpt("eq", o1, o2)
+        if (v1.bw == v2.bw) eq(v1, v2)
+        else primOp2("eq", o1, o2)
+      case _ => primOp2("eq", o1, o2)
     }
   }
 
@@ -390,8 +391,15 @@ trait ValueDefs { self: SAIOps with BasicDefs with Opaques =>
     def apply(op: String, o1: Rep[Value], o2: Rep[Value]) = "float_op_2".reflectWith[Value](op, o1, o2)
   }
 
+  object ContOpt {
+    def dummyCont[W[_]](implicit m: Manifest[W[SS]]): ContOpt[W] = ContOpt[W]((s, v) => ())
+    def fromRepCont[W[_]](k: Rep[PCont[W]])(implicit m: Manifest[W[SS]]) = ContOpt[W]((s, v) => k(s, v))
+  }
+
   case class ContOpt[W[_]](k: (Rep[W[SS]], Rep[Value]) => Rep[Unit])(implicit m: Manifest[W[SS]]) {
-    lazy val repK = fun(k(_, _))
+    lazy val repK: Rep[PCont[W]] =
+      if (Config.onStackCont && !usingPureEngine) unchecked[PCont[W]]("pop_cont_apply")
+      else fun(k(_, _))
     def apply(s: Rep[W[SS]], v: Rep[Value]): Rep[Unit] = k(s, v)
   }
 
@@ -433,25 +441,23 @@ trait ValueDefs { self: SAIOps with BasicDefs with Opaques =>
         case _ => "direct_apply".reflectWith[List[(SS, Value)]](v, s, args)
       }
 
-    // The CPS version
-    // W[_] is parameterized over pass-by-value (Id) or pass-by-ref (Ref) of SS
-    def apply[W[_]](s: Rep[W[SS]], args: Rep[List[Value]], k: Rep[PCont[W]])(implicit m: Manifest[W[SS]]): Rep[Unit] =
-      v match {
-        case ExternalFun("noop", ty) if Config.opt => k(s, defaultRetVal(ty))
-        case ExternalFun(f, ty) => f.reflectWith[Unit](s, args, k)
-        case CPSFunV(f) => f(s, args, k)                       // direct call
-        case _ => "cps_apply".reflectWith[Unit](v, s, args, k) // indirect call
-      }
-
+    // This `apply` works for the CPS version that takes an optimizable continuation `ContOpt`.
+    // Using `ContOpt`, we may choose to call the continuation at staging-time, or to generate
+    // the continuation function into the second stage.
+    // W[_] is parameterized over pass-by-value (Id[_]) or pass-by-ref (Ref[_]) of SS.
     def apply[W[_]](s: Rep[W[SS]], args: Rep[List[Value]], k: ContOpt[W])(implicit m: Manifest[W[SS]]): Rep[Unit] =
       v match {
-        case ExternalFun("noop", ty) if Config.opt => k(s, defaultRetVal(ty))
-        case ExternalFun(f, ty) if ExternalFun.isDeterministic(f) && !usingPureEngine =>
+        case ExternalFun("noop", ty) if Config.opt =>
+          // Avoids generating continuations for the `noop` function.
+          k(s, defaultRetVal(ty))
+        case ExternalFun(f, ty) if Config.opt && ExternalFun.isDeterministic(f) && !usingPureEngine =>
+          // Avoids generating continuations for the _imperative_ CPS engine if the function is deterministic.
           // Be careful: since the state is not passed/returned, with the imperative backend it means
           // the state must be passed by reference to f_det! Currently not all deterministic functions
           // defined in backend works in this way (see external_shared.hpp).
           k(s, (f+"_det").reflectCtrlWith[Value](s, args))
-        case ExternalFun(f, ty) if ExternalFun.isDeterministic(f) && usingPureEngine =>
+        case ExternalFun(f, ty) if Config.opt && ExternalFun.isDeterministic(f) && usingPureEngine =>
+          // Avoids generating continuations for the _pure_ engine if the function is deterministic.
           val sv = (f+"_det").reflectCtrlWith[(W[SS], Value)](s, args)
           k(sv._1, sv._2)
         case ExternalFun(f, ty) => f.reflectWith[Unit](s, args, k.repK)
@@ -464,22 +470,22 @@ trait ValueDefs { self: SAIOps with BasicDefs with Opaques =>
     val foldableOp = StaticSet[String]("make_SymV", "make_IntV", "bv_sext", "bv_zext")
 
     def sExt(bw: Int): Rep[Value] = Unwrap(v) match {
-      case gNode(s, (v1: bExp)::bConst(bw1: Int)::_) if (foldableOp(s) && (bw1 == bw)) => v
-      case gNode("make_IntV", (v1: bExp)::bConst(bw1: Int)::_) if bw > bw1 =>
+      case gNode(s, (v1: bExp)::bConst(bw1: Int)::_) if foldableOp(s) && (bw1 == bw) && Config.opt => v
+      case gNode("make_IntV", (v1: bExp)::bConst(bw1: Int)::_) if bw > bw1 && Config.opt =>
         // sExt(IntV(n, bw1), bw) ⇒ IntV(n, bw)
         IntV(Wrap[Long](v1), bw)
-      case gNode("bv_sext", (v1: bExp)::bConst(bw1: Int)::_) if bw > bw1=>
+      case gNode("bv_sext", (v1: bExp)::bConst(bw1: Int)::_) if bw > bw1 && Config.opt =>
         // sExt(sExt(n, bw1), bw) ⇒ sExt(n, bw)
         Wrap[Value](v1).sExt(bw)
       case _ => "bv_sext".reflectWith[Value](v, bw)
     }
 
     def zExt(bw: Int): Rep[Value] = Unwrap(v) match {
-      case gNode(s, (v1: bExp)::bConst(bw1: Int)::_) if (foldableOp(s) && (bw1 == bw)) => v
-      case gNode("make_IntV", (v1: bExp)::bConst(bw1: Int)::_) if bw > bw1 =>
+      case gNode(s, (v1: bExp)::bConst(bw1: Int)::_) if foldableOp(s) && (bw1 == bw) && Config.opt => v
+      case gNode("make_IntV", (v1: bExp)::bConst(bw1: Int)::_) if bw > bw1 && Config.opt =>
         // zExt(IntV(n, bw1), bw) ⇒ IntV(n, bw)
         IntV(Wrap[Long](v1), bw)
-      case gNode("bv_zext", (v1: bExp)::bConst(bw1: Int)::_) if bw > bw1=>
+      case gNode("bv_zext", (v1: bExp)::bConst(bw1: Int)::_) if bw > bw1 && Config.opt =>
         // zExt(sExt(n, bw1), bw) ⇒ zExt(n, bw)
         Wrap[Value](v1).zExt(bw)
       case _ => "bv_zext".reflectWith[Value](v, bw)
@@ -502,6 +508,7 @@ trait ValueDefs { self: SAIOps with BasicDefs with Opaques =>
     def *(rhs: Rep[Value]): Rep[Value] = IntOp2.mul(v, rhs)
     def &(rhs: Rep[Value]): Rep[Value] = IntOp2("and", v, rhs)
     def |(rhs: Rep[Value]): Rep[Value] = IntOp2("or", v, rhs)
+    def ≡(rhs: Rep[Value]): Rep[Value] = IntOp2.eq(v, rhs)
     def unary_! : Rep[Value] = IntOp1.neg(v)
     def unary_~ : Rep[Value] = IntOp1.bvnot(v)
 
diff --git a/src/main/scala/gensym/RunGenSym.scala b/src/main/scala/gensym/RunGenSym.scala
index 403472cb..32da9fab 100644
--- a/src/main/scala/gensym/RunGenSym.scala
+++ b/src/main/scala/gensym/RunGenSym.scala
@@ -23,21 +23,27 @@ object Config {
   val (o0, o1, o2, o3) = ("O0", "O1", "O2", "O3")
 
   /* Global compile-time configurations */
+
+  // use first-stage compile-time optimizations
   var opt: Boolean = true
+  // compile `select` instructions to ITE or branches
   var iteSelect: Boolean = true
+  // generate Makefile with -g and -DDEBUG
   var genDebug: Boolean = false
+  // generate a map from source variable names to their compiled name
   var emitVarIdMap: Boolean = true
+  // generate a map from source block labels to their compiled name
   var emitBlockIdMap: Boolean = true
+  // merge same switch targets to disjunctive conditions instead of forking
   var switchType: SwitchType = Merge
-  var runCode: Boolean = true
+  // generate code that records executed instruction numbers
   var recordInstNum: Boolean = false
+  // push continuations onto stack or pass continuations as arguments (applicable for ImpCPS engine)
+  var onStackCont: Boolean = true
 
   def disableOpt: Unit = opt = false
   def enableOpt: Unit = opt = true
 
-  def disableRunCode: Unit = runCode = false
-  def enableRunCode: Unit = runCode = true
-
   def symArg(n: Int) = Config(n, false, o3)
   def useArgv = Config(0, true, o3)
   def noArg = Config(0, false, o3)
@@ -72,6 +78,8 @@ object RunGenSym {
     |--switch-type=<string>  - compilation variants of `switch` statement (default=nonMerge)
     |  =merge                - only fork `m` paths of distinct targets
     |  =nonMerge             - fork `n` paths where `n` is the total number of feasible cases (including default)
+    |--on-stack-cont         - push continuations onto stack, otherwise continuations are passed as argument (only applicable for ImpCPS engine, default=true)
+    |                        -   push continuations onto stack avoids generating nested C++ closures
     |--help                  - print this help message
     """
 
@@ -86,6 +94,7 @@ object RunGenSym {
       case (options, r"emit-block-id-map") => options + ("blockIdMap" -> true)
       case (options, r"emit-var-id-map") => options + ("varIdMap" -> true)
       case (options, r"--switch-type=(\w+)$t") => options + ("switchType" -> SwitchType.fromString(t))
+      case (options, r"--on-stack-cont") => options + ("onStackCont" -> true)
       case (options, r"--lib=([-_A-Za-z0-9\/\.]+)$p") => options + ("lib" -> p)
       case (options, "--help") => println(usage.stripMargin); sys.exit(0)
       case (options, input) => options + ("input" -> input)
@@ -101,6 +110,7 @@ object RunGenSym {
     val emitBlockIdMap = options.getOrElse("blockIdMap", Config.emitBlockIdMap).asInstanceOf[Boolean]
     val emitVarIdMap = options.getOrElse("varIdMap", Config.emitVarIdMap).asInstanceOf[Boolean]
     val switchType = options.getOrElse("switchType", SwitchType.NonMerge).asInstanceOf[SwitchType]
+    val onStackCont = options.getOrElse("onStackCont", Config.onStackCont).asInstanceOf[Boolean]
     val libPath = options.get("lib").asInstanceOf[Option[String]]
 
     val gensym = engine match {
@@ -115,9 +125,11 @@ object RunGenSym {
     Config.emitBlockIdMap = emitBlockIdMap
     Config.emitVarIdMap = emitVarIdMap
     Config.switchType = switchType
+    Config.onStackCont = onStackCont
     val info = s"""Running $engine with
     |  filepath=$filepath, entrance=$entrance, output=$output,
-    |  nSym=$nSym, useArgv=$useArgv, optimize=$optimize, mainOpt=$mainOpt, switchType=$switchType"""
+    |  nSym=$nSym, useArgv=$useArgv, optimize=$optimize, mainOpt=$mainOpt, switchType=$switchType
+    |  onStackCont=$onStackCont"""
     println(info.stripMargin)
     gensym.run(parseFile(filepath), output, entrance, Config(nSym, useArgv, mainOpt), libPath)
   }
diff --git a/src/main/scala/gensym/Transform.scala b/src/main/scala/gensym/Transform.scala
index 1d9acff5..2a05d414 100644
--- a/src/main/scala/gensym/Transform.scala
+++ b/src/main/scala/gensym/Transform.scala
@@ -7,7 +7,7 @@ import lms.core.stub.{While => _, _}
 import gensym.imp.Mut
 
 import scala.collection.immutable.{List => StaticList}
-import scala.collection.mutable.{HashMap,HashSet}
+import scala.collection.mutable.{HashMap, HashSet}
 
 object AssignElim {
   type Subst = HashMap[Sym, Exp]
diff --git a/src/main/scala/gensym/engines/ImpCPSEngine.scala b/src/main/scala/gensym/engines/ImpCPSEngine.scala
index ac0dfa4b..18846249 100644
--- a/src/main/scala/gensym/engines/ImpCPSEngine.scala
+++ b/src/main/scala/gensym/engines/ImpCPSEngine.scala
@@ -45,8 +45,11 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
     "async_exec_block".reflectWriteWith[Unit](unchecked[String](realBlockFunName), ss, k)(Adapter.CTRL)
   }
 
-  def contApply(cont: Rep[Cont], ss: Rep[SS], v: Rep[Value]): Rep[Unit] = {
-    "cont_apply".reflectWriteWith[Unit](cont, ss, v)(Adapter.CTRL)
+  def compileCont(k: (Rep[Ref[SS]], Rep[Value]) => Rep[Unit])(implicit ctx: Ctx): Rep[Cont] = {
+    val repK = fun(k)
+    val node = Unwrap(repK).asInstanceOf[Backend.Sym]
+    funNameMap(node) = strippedFunName(ctx.funName) + "_k_" + Counter.cont.fresh
+    repK
   }
 
   def eval(v: LLVMValue, ty: LLVMType, ss: Rep[SS], argTypes: Option[List[LLVMType]] = None)(implicit ctx: Ctx): Rep[Value] =
@@ -97,7 +100,7 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
       case InlineASM() => NullPtr[Value]
       case ZeroInitializerConst =>
         System.out.println("Warning: Evaluate zeroinitialize in body")
-        NullPtr[Value] // FIXME: use uninitValue
+        uninitValue
       case NullConst => NullLoc()
       case NoneConst => NullPtr[Value]
     }
@@ -108,83 +111,87 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
   def evalFloatOp2(op: String, lhs: LLVMValue, rhs: LLVMValue, ty: LLVMType, ss: Rep[SS])(implicit ctx: Ctx): Rep[Value] =
     FloatOp2(op, eval(lhs, ty, ss), eval(rhs, ty, ss))
 
-  def execValueInst(inst: ValueInstruction, ss: Rep[SS], k: (Rep[SS], Rep[Value], Rep[Cont]) => Rep[Unit])(implicit ctx: Ctx, kk: Rep[Cont]): Rep[Unit] = {
+  def selectValue(bb: Rep[BlockLabel], vs: List[() => Rep[Value]], labels: List[BlockLabel]): Rep[Value] =
+    if (bb == labels(0) || labels.length == 1) vs(0)()
+    else selectValue(bb, vs.tail, labels.tail)
+
+  def execValueInst(inst: ValueInstruction, ss: Rep[SS])(k: (Rep[Ref[SS]], Rep[Value]) => Rep[Unit])(implicit ctx: Ctx): Rep[Unit] = {
     inst match {
       // Memory Access Instructions
       case AllocaInst(ty, align) =>
         val typeSize = ty.size
         val sz = ss.stackSize
         ss.allocStack(typeSize, align.n)
-        k(ss, LocV(sz, LocV.kStack, typeSize.toLong), kk)
+        k(ss, LocV(sz, LocV.kStack, typeSize.toLong))
       case LoadInst(valTy, ptrTy, value, align) =>
         val isStruct = getRealType(valTy) match {
           case Struct(types) => 1
           case _ => 0
         }
         val v = eval(value, ptrTy, ss)
-        k(ss, ss.lookup(v, valTy.size, isStruct), kk)
+        k(ss, ss.lookup(v, valTy.size, isStruct))
       case GetElemPtrInst(_, baseType, ptrType, ptrValue, typedValues) =>
         val vs = typedValues.map(tv => eval(tv.value, tv.ty, ss))
         val offset = calculateOffset(ptrType, vs)
         val v = eval(ptrValue, ptrType, ss).asRepOf[LocV] + offset
-        k(ss, v, kk)
+        k(ss, v)
       // Arith Unary Operations
-      case FNegInst(ty, op) => k(ss, evalFloatOp2("fsub", FloatConst(-0.0), op, ty, ss), kk)
+      case FNegInst(ty, op) => k(ss, evalFloatOp2("fsub", FloatConst(-0.0), op, ty, ss))
       // Arith Binary Operations
-      case AddInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("add", lhs, rhs, ty, ss), kk)
-      case SubInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("sub", lhs, rhs, ty, ss), kk)
-      case MulInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("mul", lhs, rhs, ty, ss), kk)
-      case SDivInst(ty, lhs, rhs) => k(ss, evalIntOp2("sdiv", lhs, rhs, ty, ss), kk)
-      case UDivInst(ty, lhs, rhs) => k(ss, evalIntOp2("udiv", lhs, rhs, ty, ss), kk)
-      case FAddInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fadd", lhs, rhs, ty, ss), kk)
-      case FSubInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fsub", lhs, rhs, ty, ss), kk)
-      case FMulInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fmul", lhs, rhs, ty, ss), kk)
-      case FDivInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fdiv", lhs, rhs, ty, ss), kk)
-      case URemInst(ty, lhs, rhs) => k(ss, evalIntOp2("urem", lhs, rhs, ty, ss), kk)
-      case SRemInst(ty, lhs, rhs) => k(ss, evalIntOp2("srem", lhs, rhs, ty, ss), kk)
+      case AddInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("add", lhs, rhs, ty, ss))
+      case SubInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("sub", lhs, rhs, ty, ss))
+      case MulInst(ty, lhs, rhs, _) => k(ss, evalIntOp2("mul", lhs, rhs, ty, ss))
+      case SDivInst(ty, lhs, rhs) => k(ss, evalIntOp2("sdiv", lhs, rhs, ty, ss))
+      case UDivInst(ty, lhs, rhs) => k(ss, evalIntOp2("udiv", lhs, rhs, ty, ss))
+      case FAddInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fadd", lhs, rhs, ty, ss))
+      case FSubInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fsub", lhs, rhs, ty, ss))
+      case FMulInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fmul", lhs, rhs, ty, ss))
+      case FDivInst(ty, lhs, rhs) => k(ss, evalFloatOp2("fdiv", lhs, rhs, ty, ss))
+      case URemInst(ty, lhs, rhs) => k(ss, evalIntOp2("urem", lhs, rhs, ty, ss))
+      case SRemInst(ty, lhs, rhs) => k(ss, evalIntOp2("srem", lhs, rhs, ty, ss))
       // Bitwise Operations
-      case ShlInst(ty, lhs, rhs) => k(ss, evalIntOp2("shl", lhs, rhs, ty, ss), kk)
-      case LshrInst(ty, lhs, rhs) => k(ss, evalIntOp2("lshr", lhs, rhs, ty, ss), kk)
-      case AshrInst(ty, lhs, rhs) => k(ss, evalIntOp2("ashr", lhs, rhs, ty, ss), kk)
-      case AndInst(ty, lhs, rhs) => k(ss, evalIntOp2("and", lhs, rhs, ty, ss), kk)
-      case OrInst(ty, lhs, rhs) => k(ss, evalIntOp2("or", lhs, rhs, ty, ss), kk)
-      case XorInst(ty, lhs, rhs) => k(ss, evalIntOp2("xor", lhs, rhs, ty, ss), kk)
+      case ShlInst(ty, lhs, rhs) => k(ss, evalIntOp2("shl", lhs, rhs, ty, ss))
+      case LshrInst(ty, lhs, rhs) => k(ss, evalIntOp2("lshr", lhs, rhs, ty, ss))
+      case AshrInst(ty, lhs, rhs) => k(ss, evalIntOp2("ashr", lhs, rhs, ty, ss))
+      case AndInst(ty, lhs, rhs) => k(ss, evalIntOp2("and", lhs, rhs, ty, ss))
+      case OrInst(ty, lhs, rhs) => k(ss, evalIntOp2("or", lhs, rhs, ty, ss))
+      case XorInst(ty, lhs, rhs) => k(ss, evalIntOp2("xor", lhs, rhs, ty, ss))
       // Conversion Operations
       case ZExtInst(from, value, IntType(size)) =>
-        k(ss, eval(value, from, ss).zExt(size), kk)
+        k(ss, eval(value, from, ss).zExt(size))
       case SExtInst(from, value, IntType(size)) =>
-        k(ss, eval(value, from, ss).sExt(size), kk)
+        k(ss, eval(value, from, ss).sExt(size))
       case TruncInst(from@IntType(fromSz), value, IntType(toSz)) =>
-        k(ss, eval(value, from, ss).trunc(fromSz, toSz), kk)
+        k(ss, eval(value, from, ss).trunc(fromSz, toSz))
       case FpExtInst(from, value, to) =>
-        k(ss, eval(value, from, ss), kk)
+        k(ss, eval(value, from, ss))
       case FpTruncInst(from, value, to) =>
-        k(ss, eval(value, from, ss), kk)
+        k(ss, eval(value, from, ss))
       case FpToUIInst(from, value, IntType(size)) =>
-        k(ss, eval(value, from, ss).fromFloatToUInt(size), kk)
+        k(ss, eval(value, from, ss).fromFloatToUInt(size))
       case FpToSIInst(from, value, IntType(size)) =>
-        k(ss, eval(value, from, ss).fromFloatToSInt(size), kk)
+        k(ss, eval(value, from, ss).fromFloatToSInt(size))
       case UiToFPInst(from, value, to) =>
-        k(ss, eval(value, from, ss).fromUIntToFloat, kk)
+        k(ss, eval(value, from, ss).fromUIntToFloat)
       case SiToFPInst(from, value, to) =>
-        k(ss, eval(value, from, ss).fromSIntToFloat, kk)
+        k(ss, eval(value, from, ss).fromSIntToFloat)
       case PtrToIntInst(from, value, to) =>
         val v = eval(value, from, ss)
         val toSize = to.asInstanceOf[IntType].size
-        k(ss, if (ARCH_WORD_SIZE == toSize) v else v.trunc(ARCH_WORD_SIZE, toSize), kk)
+        k(ss, if (ARCH_WORD_SIZE == toSize) v else v.trunc(ARCH_WORD_SIZE, toSize))
       case IntToPtrInst(from, value, to) =>
-        k(ss, eval(value, from, ss), kk)
-      case BitCastInst(from, value, to) => k(ss, eval(value, to, ss), kk)
+        k(ss, eval(value, from, ss))
+      case BitCastInst(from, value, to) => k(ss, eval(value, to, ss))
       // Aggregate Operations
       case ExtractValueInst(ty, struct, indices) =>
         val idxList = indices.asInstanceOf[List[IntConst]].map(x => x.n)
         val idx = calculateOffsetStatic(ty, idxList)
         // v is expected to be StructV in backend
         val v = eval(struct, ty, ss)
-        k(ss, v.structAt(idx), kk)
+        k(ss, v.structAt(idx))
       // Arithm comparison operations
-      case FCmpInst(pred, ty, lhs, rhs) => k(ss, evalFloatOp2(pred.op, lhs, rhs, ty, ss), kk)
-      case ICmpInst(pred, ty, lhs, rhs) => k(ss, evalIntOp2(pred.op, lhs, rhs, ty, ss), kk)
+      case FCmpInst(pred, ty, lhs, rhs) => k(ss, evalFloatOp2(pred.op, lhs, rhs, ty, ss))
+      case ICmpInst(pred, ty, lhs, rhs) => k(ss, evalIntOp2(pred.op, lhs, rhs, ty, ss))
       // Other operations
       case CallInst(ty, f, args) =>
         val argValues: List[LLVMValue] = extractValues(args)
@@ -192,47 +199,55 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
         val fv = eval(f, VoidType, ss, Some(argTypes))
         val vs = argValues.zip(argTypes).map { case (v, t) => eval(v, t, ss) }
         val stackSize = ss.stackSize
-        ss.push(kk)
-        def fK(s: Rep[Ref[SS]], v: Rep[Value]): Rep[Unit] = k(s, v, s.pop(stackSize))
+        if (Config.onStackCont) {
+          ss.push(stackSize, compileCont(k))
+          // Note: in this case, even we have compiled cont k, fK still will be used only when 
+          // we want to apply the continuation at staing-time (as an optimization);
+          // we will not reify `fK` into second stage. Instead, backend-defined `pop_cont_apply`
+          // that will be used to apply the pushed continuation with returned value.
+          // TODO: this is still not ideal, since `compileCont(k)` will anyway generate/push
+          // a continuation function, even though we can statically reduce it some time.
+          // See an example in @merge_%while.end64 of merge_sort; we also want to eliminate dummy
+          // push/pop pair, which benefits the case if not using onStackCont.
+        } else {
+          ss.push
+        }
+        def fK(s: Rep[Ref[SS]], v: Rep[Value]): Rep[Unit] = { s.pop(stackSize); k(s, v) }
         fv[Ref](ss, List(vs: _*), ContOpt(fK))
       case PhiInst(ty, incs) =>
-        def selectValue(bb: Rep[BlockLabel], vs: List[() => Rep[Value]], labels: List[BlockLabel]): Rep[Value] = {
-          if (bb == labels(0) || labels.length == 1) vs(0)()
-          else selectValue(bb, vs.tail, labels.tail)
-        }
         val incsValues: List[LLVMValue] = incs.map(_.value)
         val incsLabels: List[BlockLabel] = incs.map(i => Counter.block.get(ctx.withBlock(i.label)))
         val vs = incsValues.map(v => () => eval(v, ty, ss))
-        k(ss, selectValue(ss.incomingBlock, vs, incsLabels), kk)
+        k(ss, selectValue(ss.incomingBlock, vs, incsLabels))
       case SelectInst(cndTy, cndVal, thnTy, thnVal, elsTy, elsVal) if Config.iteSelect =>
-        k(ss, ITE(eval(cndVal, cndTy, ss), eval(thnVal, thnTy, ss), eval(elsVal, elsTy, ss)), kk)
+        k(ss, ITE(eval(cndVal, cndTy, ss), eval(thnVal, thnTy, ss), eval(elsVal, elsTy, ss)))
       case SelectInst(cndTy, cndVal, thnTy, thnVal, elsTy, elsVal) =>
         val cnd = eval(cndVal, cndTy, ss)
         val repK = fun(k)
         if (cnd.isConc) {
-          if (cnd.int == 1) repK(ss, eval(thnVal, thnTy, ss), kk)
-          else repK(ss, eval(elsVal, elsTy, ss), kk)
+          if (cnd.int == 1) repK(ss, eval(thnVal, thnTy, ss))
+          else repK(ss, eval(elsVal, elsTy, ss))
         } else {
           // TODO: check cond via solver
           val s1 = ss.fork
           ss.addPC(cnd)
-          repK(ss, eval(thnVal, thnTy, ss), kk)
+          repK(ss, eval(thnVal, thnTy, ss))
           s1.addPC(!cnd)
           Coverage.incPath(1)
-          repK(s1, eval(elsVal, elsTy, s1), kk)
+          repK(s1, eval(elsVal, elsTy, s1))
         }
     }
   }
 
   def execTerm(inst: Terminator, k: Rep[Cont])(implicit ss: Rep[SS], ctx: Ctx): Rep[Unit] = {
     inst match {
-      case Unreachable => contApply(k, ss, IntV(-1))
+      case Unreachable => k(ss, IntV(-1))
       case RetTerm(ty, v) =>
         val ret = v match {
           case Some(value) => eval(value, ty, ss)
           case None => NullPtr[Value]
         }
-        contApply(k, ss, ret)
+        k(ss, ret)
       case BrTerm(lab) if (cfg.pred(ctx.funName, lab).size == 1) =>
         execBlockEager(findBlock(ctx.funName, lab).get, ss, k)(Ctx(ctx.funName, lab))
       case BrTerm(lab) =>
@@ -242,7 +257,6 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
         Counter.setBranchNum(ctx, 2)
         ss.addIncomingBlock(ctx)
         val cndVal = eval(cnd, ty, ss)
-        //branch(ss, cndVal.toSym, cndVal.toSymNeg, thnLab, elsLab, funName, k)
         if (cndVal.isConc) {
           if (cndVal.int == 1) {
             Coverage.incBranch(ctx, 0)
@@ -255,30 +269,33 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
           symExecBr(ss, cndVal, !cndVal, thnLab, elsLab, k)
         }
       case SwitchTerm(cndTy, cndVal, default, swTable) =>
-        type MergedCase = (String, (Rep[Boolean], Rep[Value]))
+        // Given a case, GSCase stores its label, concrete condition expr,
+        // and symbolic condition expr.
+        case class GSCase(label: String, concCond: Rep[Boolean], symCond: Rep[Value])
         val v = eval(cndVal, cndTy, ss)
-        val mergedSwTable: StaticList[MergedCase] =
+        val mergedSwTable: StaticList[GSCase] =
           swTable.foldLeft(StaticMap[String, (Rep[Boolean], Rep[Value])]())({
             case (m, LLVMCase(_, n, tgt)) if (Config.switchType == Merge) && m.contains(tgt) =>
-              m + (tgt -> (m(tgt)._1 || v.int == n, IntOp2("or", m(tgt)._2, IntOp2("eq", v, IntV(n)))))
+              m + (tgt -> (m(tgt)._1 || v.int == n, m(tgt)._2 | v ≡ IntV(n)))
             case (m, LLVMCase(_, n, tgt)) =>
-              m + (tgt -> (v.int == n, IntOp2("eq", v, IntV(n))))
-          }).toList
+              m + (tgt -> (v.int == n, v ≡ IntV(n)))
+          }).map({ case (l, (c, s)) => GSCase(l, c, s) }).toList
+
         Counter.setBranchNum(ctx, mergedSwTable.size+1)
         System.out.println(s"Shrinking switch table from ${swTable.size+1} cases to ${mergedSwTable.size+1}")
 
         val nPath: Var[Int] = var_new(0)
-        def switch(s: Rep[SS], table: List[MergedCase]): Rep[Unit] = table match {
+        def switch(s: Rep[SS], table: List[GSCase]): Rep[Unit] = table match {
           case Nil =>
             Coverage.incBranch(ctx, mergedSwTable.size) // Note: the default case has the last branch ID
             execBlock(ctx.funName, default, s, k)
-          case (tgt, (concCnd, _))::rest =>
+          case GSCase(tgt, concCnd, _)::rest =>
             if (concCnd) {
               Coverage.incBranch(ctx, mergedSwTable.size - table.size)
               execBlock(ctx.funName, tgt, s, k)
             } else switch(s, table.tail)
         }
-        def switchSym(s: Rep[SS], table: List[MergedCase]): Rep[Unit] = table match {
+        def switchSym(s: Rep[SS], table: List[GSCase]): Rep[Unit] = table match {
           case Nil =>
             if (checkPC(s.pc)) {
               nPath += 1
@@ -286,7 +303,7 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
               Coverage.incBranch(ctx, mergedSwTable.size)
               execBlock(ctx.funName, default, newState, k)
             }
-          case (tgt, (_, symCnd))::rest =>
+          case GSCase(tgt, _, symCnd)::rest =>
             val st = s.copy
             s.addPC(symCnd)
             if (checkPC(s.pc)) {
@@ -310,30 +327,28 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
     }
   }
 
-  def execInst(inst: Instruction, ss: Rep[SS], k: (Rep[SS], Rep[Cont]) => Rep[Unit])(implicit ctx: Ctx, kk: Rep[Cont]): Rep[Unit] = {
+  def execInst(inst: Instruction, ss: Rep[SS], k: Rep[SS] => Rep[Unit])(implicit ctx: Ctx): Rep[Unit] = {
     inst match {
       case AssignInst(x, valInst) =>
-        execValueInst(valInst, ss, { case (s, v, kk) =>
+        execValueInst(valInst, ss) { (s, v) =>
           s.assign(x, v)
-          k(s, kk)
-        })
+          k(s)
+        }
       case StoreInst(ty1, val1, ty2, val2, align) =>
         val v1 = eval(val1, ty1, ss)
         val v2 = eval(val2, ty2, ss)
         ss.update(v2, v1, ty1.size)
-        k(ss, kk)
-      case CallInst(ty, f, args) =>
-        val argValues: List[LLVMValue] = extractValues(args)
-        val argTypes: List[LLVMType] = extractTypes(args)
-        val fv = eval(f, VoidType, ss, Some(argTypes))
-        val vs = argValues.zip(argTypes).map { case (v, t) => eval(v, t, ss) }
-        val stackSize = ss.stackSize
-        ss.push(kk)
-        def fK(s: Rep[Ref[SS]], v: Rep[Value]): Rep[Unit] = k(s, s.pop(stackSize))
-        fv[Ref](ss, List(vs: _*), ContOpt(fK))
+        k(ss)
+      case call@CallInst(ty, f, args) =>
+        execValueInst(call, ss) { (s, v) => k(s) }
     }
   }
 
+  def execInsts(insts: List[Instruction], s: Rep[SS])(k: Rep[SS] => Rep[Unit])(implicit ctx: Ctx): Rep[Unit] = insts match {
+    case Nil => k(s)
+    case i::inst => execInst(i, s, s => execInsts(inst, s)(k))
+  }
+
   def execBlock(funName: String, label: String, s: Rep[SS], k: Rep[Cont]): Rep[Unit] =
     execBlock(funName, findBlock(funName, label).get, s, k)
 
@@ -343,15 +358,11 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
   }
 
   def execBlockEager(block: BB, s: Rep[SS], k: Rep[Cont])(implicit ctx: Ctx): Rep[Unit] = {
-    def runInst(insts: List[Instruction], t: Terminator, s: Rep[SS], k: Rep[Cont]): Rep[Unit] =
-      insts match {
-        case Nil =>
-          Coverage.incInst(block.ins.size+1)
-          execTerm(t, k)(s, ctx)
-        case i::inst => execInst(i, s, (s1, k1) => runInst(inst, t, s1, k1))(ctx, k)
-      }
     s.coverBlock(ctx)
-    runInst(block.ins, block.term, s, k)
+    execInsts(block.ins, s) { s =>
+      Coverage.incInst(block.ins.size+1)
+      execTerm(block.term, k)(s, ctx)
+    }
   }
 
   override def repBlockFun(b: BB)(implicit ctx: Ctx): BFTy = {
@@ -409,9 +420,10 @@ trait ImpCPSGSEngine extends ImpSymExeDefs with EngineBase {
     Coverage.incPath(1)
     val ss = initState(preHeap.asRepOf[Mem])
     val fv = eval(GlobalId(fname), VoidType, ss)
-    ss.push
+    if (Config.onStackCont) ss.push(0, k)
+    else ss.push
     ss.updateArg
     ss.initErrorLoc
-    fv[Ref](ss, args, k)
+    fv[Ref](ss, args, ContOpt.fromRepCont[Ref](k))
   }
 }
diff --git a/src/main/scala/gensym/engines/ImpEngine.scala b/src/main/scala/gensym/engines/ImpEngine.scala
index cfd3633b..c20ff6ef 100644
--- a/src/main/scala/gensym/engines/ImpEngine.scala
+++ b/src/main/scala/gensym/engines/ImpEngine.scala
@@ -310,21 +310,8 @@ trait ImpGSEngine extends ImpSymExeDefs with EngineBase {
         val v2 = eval(val2, ty2, ss)
         ss.update(v2, v1, ty1.size)
         k(ss)
-      case CallInst(ty, f, args) =>
-        val argValues: List[LLVMValue] = extractValues(args)
-        val argTypes: List[LLVMType] = extractTypes(args)
-        val fv = eval(f, VoidType, ss, Some(argTypes))
-        val vs = argValues.zip(argTypes).map {
-          case (v, t) => eval(v, t, ss)
-        }
-        ss.push
-        val stackSize = ss.stackSize
-        val res: Rep[List[(SS, Value)]] = fv[Ref](ss, List(vs: _*))
-        res.flatMap { case sv =>
-          val s = sv._1
-          s.pop(stackSize)
-          k(s)
-        }
+      case call@CallInst(ty, f, args) =>
+        execValueInst(call, ss, { case (s, v) => k(s) })
     }
   }
 
diff --git a/src/main/scala/gensym/engines/PureCPSEngine.scala b/src/main/scala/gensym/engines/PureCPSEngine.scala
index d8192f2e..26f355c3 100644
--- a/src/main/scala/gensym/engines/PureCPSEngine.scala
+++ b/src/main/scala/gensym/engines/PureCPSEngine.scala
@@ -306,13 +306,8 @@ trait PureCPSGSEngine extends SymExeDefs with EngineBase {
         val v1 = eval(val1, ty1, ss)
         val v2 = eval(val2, ty2, ss)
         k(ss.update(v2, v1, ty1.size))
-      case CallInst(ty, f, args) =>
-        val argValues: List[LLVMValue] = extractValues(args)
-        val argTypes: List[LLVMType] = extractTypes(args)
-        val fv = eval(f, VoidType, ss, Some(argTypes))
-        val vs = argValues.zip(argTypes).map { case (v, t) => eval(v, t, ss) }
-        def fK(s: Rep[SS], v: Rep[Value]): Rep[Unit] = k(s.pop(ss.stackSize))
-        fv[Id](ss.push, List(vs: _*), ContOpt[Id](fK))
+      case call@CallInst(ty, f, args) =>
+        execValueInst(call, ss, { case (s, v) => k(s) })
     }
   }
 
@@ -386,6 +381,6 @@ trait PureCPSGSEngine extends SymExeDefs with EngineBase {
     Coverage.incPath(1)
     val ss = initState(preHeap.asRepOf[Mem])
     val fv = eval(GlobalId(fname), VoidType, ss)
-    fv[Id](ss.push.updateArg.initErrorLoc, args, k)
+    fv[Id](ss.push.updateArg.initErrorLoc, args, ContOpt.fromRepCont[Id](k))
   }
 }
diff --git a/src/main/scala/gensym/engines/PureEngine.scala b/src/main/scala/gensym/engines/PureEngine.scala
index 4ea4956b..348b5c72 100644
--- a/src/main/scala/gensym/engines/PureEngine.scala
+++ b/src/main/scala/gensym/engines/PureEngine.scala
@@ -393,17 +393,7 @@ trait GSEngine extends StagedNondet with SymExeDefs with EngineBase {
           v2 <- eval(val2, ty2)
           _ <- updateMem(v2, v1, ty1.size)
         } yield ()
-      case CallInst(ty, f, args) =>
-        val argValues: List[LLVMValue] = extractValues(args)
-        val argTypes: List[LLVMType] = extractTypes(args)
-        for {
-          fv <- eval(f, VoidType, Some(argTypes))
-          vs <- mapM2Tup(argValues)(argTypes)(eval(_, _, None))
-          _ <- pushFrame
-          s <- getState
-          v <- reflect(fv[Id](s, List(vs:_*)))
-          _ <- popFrame(s.stackSize)
-        } yield ()
+      case call@CallInst(ty, f, args) => for { _ <- execValueInst(call) } yield ()
     }
   }
 
diff --git a/src/main/scala/gensym/states/ImpSymExeState.scala b/src/main/scala/gensym/states/ImpSymExeState.scala
index bd9c173c..c3725b12 100644
--- a/src/main/scala/gensym/states/ImpSymExeState.scala
+++ b/src/main/scala/gensym/states/ImpSymExeState.scala
@@ -111,9 +111,13 @@ trait ImpSymExeDefs extends SAIOps with BasicDefs with ValueDefs with Opaques wi
 
     // push before function call could be DCE-ed, due to high-level function dependency issue.
     def push: Rep[Unit] = reflectWrite[Unit]("ss-push", ss)(ss, Adapter.CTRL)
-    def push(cont: Rep[Cont]): Rep[Unit] = reflectWrite[Unit]("ss-push", ss, cont)(ss, Adapter.CTRL)
+    def push(k: Rep[Cont]): Rep[Unit] = reflectWrite[Unit]("ss-push", ss, k)(ss, Adapter.CTRL)
+    def push(stackSize: Rep[Int], k: Rep[Cont]): Rep[Unit] = reflectWrite[Unit]("ss-push", ss, stackSize, k)(ss, Adapter.CTRL)
     // XXX: since pop is used in a map, will be DCE-ed if no CTRL
-    def pop(keep: Rep[Int]): Rep[Cont] = reflectWrite[Cont]("ss-pop", ss, keep)(ss, Adapter.CTRL)
+    def pop(keep: Rep[Int]): Rep[Unit] = reflectWrite[Unit]("ss-pop", ss, keep)(ss, Adapter.CTRL)
+    def popRet(v: Rep[Value]): Rep[Unit] = reflectWrite[Unit]("ss-pop", ss, v)(ss, Adapter.CTRL)
+      //"pop_cont_apply".reflectUnsafeWith[Unit](ss, v) // Note: we want to inline this
+
     def addPC(e: Rep[Value]): Rep[Unit] = reflectWrite[Unit]("ss-addpc", ss, e)(ss)
     def addPCSet(es: Rep[List[Value]]): Rep[Unit] = reflectWrite[Unit]("ss-addpcset", ss, es)(ss)
     def pc: Rep[PC] = reflectRead[PC]("get-pc", ss)(ss)
diff --git a/src/main/scala/lms/ListOps.scala b/src/main/scala/lms/ListOps.scala
index 1a4e0189..c5ce9d1f 100644
--- a/src/main/scala/lms/ListOps.scala
+++ b/src/main/scala/lms/ListOps.scala
@@ -293,7 +293,7 @@ trait CppCodeGen_List extends ExtendedCCodeGen {
       emit("{")
       if (!xs.isEmpty) {
         shallow(xs.head)
-        xs.tail.map { x =>
+        xs.tail.foreach { x =>
           emit(", ")
           shallow(x)
         }
diff --git a/src/test/scala/gensym/TestGS.scala b/src/test/scala/gensym/TestGS.scala
index 52e84215..a61a3891 100644
--- a/src/test/scala/gensym/TestGS.scala
+++ b/src/test/scala/gensym/TestGS.scala
@@ -138,7 +138,8 @@ class Coreutils extends TestGS {
   }
   testGS(new ImpCPSGS, cases)
 
-  //testGS(new ImpCPSGS, TestPrg(cat_linked, "cat_linked_posix", "@main", noMainFileOpt, "--argv=./cat.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(28567)++status(0)))
+  lazy val cat_linked = parseFile("benchmarks/gs_posix/cat_linked.ll")
+  testGS(new ImpCPSGS, TestPrg(cat_linked, "cat_linked_posix", "@main", noMainFileOpt, "--argv=./cat.bc --sym-stdout --sym-stdin 2 --sym-arg 2", nPath(28567)++status(0), runCode = false))
 }
 */
 
@@ -150,9 +151,11 @@ class TestLibrary extends TestGS {
 class Playground extends TestGS {
   import gensym.llvm.parser.Parser._
   Config.enableOpt
-  val gs = new ImpGS
+  val gs = new ImpCPSGS
+  //testGS(gs, TestPrg(assumeTest, "assumeTest", "@main", noArg, noOpt, nPath(1)++status(0)))
 
-  //testGS(gs, TestPrg(mergesort, "mergeSortTest1", "@main", noArg, noOpt, nPath(720)))
+  testGS(gs, TestPrg(mergesort, "mergeSortTest", "@main", noArg, noOpt, nPath(720)))
+  //testGS(gs, TestPrg(kmpmatcher, "kmp", "@main", noArg, noOpt, nPath(1287)))
   //testGS(new PureCPSGS, TestPrg(arrayFlow, "arrayFlow", "@main", noArg, noOpt, nPath(15)++status(0)))
   //testGS(new ImpCPSGS, TestPrg(arrayFlow, "arrayFlow2", "@main", noArg, noOpt, nPath(15)++status(0)))
 
diff --git a/third-party/immer b/third-party/immer
index e5d79ed8..93ab7151 160000
--- a/third-party/immer
+++ b/third-party/immer
@@ -1 +1 @@
-Subproject commit e5d79ed80ec74d511cc4f52fb68feeac66507f2c
+Subproject commit 93ab7151cd7b3482e59fe0e4d43549ac3f1520b4