diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re
index 89633ed371..8006642e85 100644
--- a/src/haz3lcore/dynamics/Evaluator.re
+++ b/src/haz3lcore/dynamics/Evaluator.re
@@ -21,6 +21,8 @@ module Result = {
 
 open Result;
 
+// ======== Non-tail recursive evaluator (Obselete) ===========
+
 module EvaluatorEVMode: {
   type status =
     | Final
@@ -74,15 +76,118 @@ module EvaluatorEVMode: {
 };
 module Eval = Transition(EvaluatorEVMode);
 
+// let rec evaluate = (state, env, d) => {
+//   let u = Eval.transition(evaluate, state, env, d);
+//   switch (u) {
+//   | (Final, x) => (Final, x)
+//   | (Uneval, x) => evaluate(state, env, x)
+//   };
+// };
+
+// ======== Evaluator with internal stack (Current) ===========
+
+// This module defines the stack machine for the evaluator.
+module Trampoline = {
+  type t('a) =
+    | Bind(t('b), 'b => t('a)): t('a)
+    | Next(unit => t('a)): t('a)
+    | Done('a): t('a);
+
+  type callstack('a, 'b) =
+    | Finished: callstack('a, 'a)
+    | Continue('a => t('b), callstack('b, 'c)): callstack('a, 'c);
+
+  let rec run: type a b. (t(b), callstack(b, a)) => a =
+    (t: t(b), callstack: callstack(b, a)) => (
+      switch (t) {
+      | Bind(t, f) => (run(t, Continue(f, callstack)): a)
+      | Next(f) => run(f(), callstack)
+      | Done(x) =>
+        switch (callstack) {
+        | Finished => x
+        | Continue(f, callstack) => run(f(x), callstack)
+        }
+      }: a
+    );
+
+  let run = run(_, Finished);
+
+  let return = x => Done(x);
+
+  let bind = (t, f) => Bind(t, f);
+
+  module Syntax = {
+    let (let.trampoline) = (x, f) => bind(x, f);
+  };
+};
+
+module TrampolineEVMode: {
+  include
+    EV_MODE with
+      type state = ref(EvaluatorState.t) and
+      type result = Trampoline.t((EvaluatorEVMode.status, DHExp.t));
+} = {
+  open Trampoline.Syntax;
+
+  type result = Trampoline.t((EvaluatorEVMode.status, DHExp.t));
+  type requirement('a) = Trampoline.t('a);
+  type requirements('a, 'b) = Trampoline.t(('a, 'b));
+
+  type state = ref(EvaluatorState.t);
+  let update_test = (state, id, v) =>
+    state := EvaluatorState.add_test(state^, id, v);
+
+  let req_final = (f, _, x) => {
+    let.trampoline x' = Next(() => f(x));
+    Trampoline.return(x' |> snd);
+  };
+  let rec req_all_final = (f, i, xs) =>
+    switch (xs) {
+    | [] => Trampoline.return([])
+    | [x, ...xs] =>
+      let.trampoline x' = req_final(f, x => x, x);
+      let.trampoline xs' = req_all_final(f, i, xs);
+      Trampoline.return([x', ...xs']);
+    };
+
+  let otherwise = (_, c) => Trampoline.return(((), c));
+  let (and.) = (t1, t2) => {
+    let.trampoline (x1, c1) = t1;
+    let.trampoline x2 = t2;
+    Trampoline.return(((x1, x2), c1(x2)));
+  };
+  let (let.) = (t1, s) => {
+    let.trampoline (x, c) = t1;
+    switch (s(x)) {
+    | Step({expr, state_update, is_value: true, _}) =>
+      state_update();
+      Trampoline.return((EvaluatorEVMode.Final, expr));
+    | Step({expr, state_update, is_value: false, _}) =>
+      state_update();
+      Trampoline.return((EvaluatorEVMode.Uneval, expr));
+    | Constructor
+    | Value
+    | Indet => Trampoline.return((EvaluatorEVMode.Final, c))
+    };
+  };
+};
+
+module TrampolineEval = Transition(TrampolineEVMode);
+
 let rec evaluate = (state, env, d) => {
-  let u = Eval.transition(evaluate, state, env, d);
+  open Trampoline.Syntax;
+  let.trampoline u = TrampolineEval.transition(evaluate, state, env, d);
   switch (u) {
-  | (Final, x) => (Final, x)
-  | (Uneval, x) => evaluate(state, env, x)
+  | (Final, x) => (EvaluatorEVMode.Final, x) |> Trampoline.return
+  | (Uneval, x) => Trampoline.Next(() => evaluate(state, env, x))
   };
 };
 
-let evaluate = (env, {d}: Elaborator.Elaboration.t) => {
+let evaluate = (state, env, d) => {
+  evaluate(state, env, d) |> Trampoline.run;
+};
+
+let evaluate' = (env, {d, _}: Elaborator.Elaboration.t) => {
   let state = ref(EvaluatorState.init);
   let env = ClosureEnvironment.of_environment(env);
   let result = evaluate(state, env, d);
diff --git a/src/haz3lweb/util/WorkerClient.re b/src/haz3lweb/util/WorkerClient.re
index 92faffe6a9..276eedff01 100644
--- a/src/haz3lweb/util/WorkerClient.re
+++ b/src/haz3lweb/util/WorkerClient.re
@@ -2,7 +2,7 @@ open Js_of_ocaml;
 open WorkerServer;
 
 let name = "worker.js"; // Worker file name
-let timeoutDuration = 20000; // Worker timeout in ms
+let timeoutDuration = 200000000; // Worker timeout in ms
 
 let initWorker = () => Worker.create(name);