diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index c43b2a58c..ef3036ca0 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -358,7 +358,7 @@ let mk_context_opt replay replay_all_used_context replay_used_context
 let mk_execution_opt input_format parse_only ()
     preludes no_locs_in_answers colors_in_output no_headers_in_output
     no_formatting_in_output no_forced_flush_in_output pretty_output
-    type_only type_smt2
+    type_only type_smt2 imperative_mode
   =
   let answers_with_loc = not no_locs_in_answers in
   let output_with_colors = colors_in_output || pretty_output in
@@ -376,6 +376,7 @@ let mk_execution_opt input_format parse_only ()
   set_type_only type_only;
   set_type_smt2 type_smt2;
   set_preludes preludes;
+  set_imperative_mode imperative_mode;
   `Ok()
 
 let mk_internal_opt
@@ -789,12 +790,16 @@ let parse_execution_opt =
     let doc = "Stop after SMT2 typing." in
     Arg.(value & flag & info ["type-smt2"] ~docs ~doc) in
 
+  let imperative_mode =
+    let doc = "Starts Alt-Ergo in incremental mode" in
+    Arg.(value & flag & info ["incremental-mode"] ~docs ~doc)
+  in
 
   Term.(ret (const mk_execution_opt $
              input_format $ parse_only $ parsers $ preludes $
              no_locs_in_answers $ colors_in_output $ no_headers_in_output $
              no_formatting_in_output $ no_forced_flush_in_output $
-             pretty_output $ type_only $ type_smt2
+             pretty_output $ type_only $ type_smt2 $ imperative_mode
             ))
 
 let parse_halt_opt =
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 0cbe38b99..bbc81664a 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -154,7 +154,49 @@ type model = Model : 'a sat_module * 'a -> model
 type solve_res =
   | Sat of model
   | Unknown of model option
-  | Unsat
+  | Unsat of Explanation.t
+
+let check_sat_status () =
+  match Options.get_status () with
+  | Status_Unsat ->
+    recoverable_error
+      "This file is known to be Unsat but Alt-Ergo return Sat";
+  | _ -> ()
+
+let check_unsat_status () =
+  match Options.get_status () with
+  | Status_Unsat ->
+    recoverable_error
+      "This file is known to be Sat but Alt-Ergo return Unsat";
+  | _ -> ()
+
+let print_solve_res loc goal_name r =
+  let validity_mode =
+    match Options.get_output_format () with
+    | Smtlib2 _ -> false
+    | Native | Why3 | Unknown _ -> true
+  in
+  let time = O.Time.value () in
+  let steps = Steps.get_steps () in
+  match r with
+  | Sat _ ->
+    Printer.print_status_sat ~validity_mode
+      (Some loc) (Some time) (Some steps) (Some goal_name);
+    check_sat_status ();
+  | Unsat dep ->
+    Printer.print_status_unsat ~validity_mode
+      (Some loc) (Some time) (Some steps) (Some goal_name);
+    if O.get_unsat_core() &&
+       not (O.get_debug_unsat_core()) &&
+       not (O.get_save_used_context())
+    then
+      Printer.print_fmt (Options.Output.get_fmt_regular ())
+        "unsat-core:@,%a@."
+        (Explanation.print_unsat_core ~tab:true) dep;
+    check_unsat_status ()
+  | Unknown _ ->
+    Printer.print_status_unknown ~validity_mode
+      (Some loc) (Some time) (Some steps) (Some goal_name);
 
 exception StopProcessDecl
 
@@ -169,9 +211,8 @@ let process_source ?selector_inst ~print_status src =
     | _ -> raise StopProcessDecl
   in
 
-  let solve (module SAT : Sat_solver_sig.S)
+  let solve (module Api : DO.Sat_solver_api)
       all_context (cnf, goal_name) =
-    let module FE = Frontend.Make (SAT) in
     if Options.get_debug_commands () then
       Printer.print_dbg "@[<v 2>goal %s:@ %a@]@."
         ~module_name:"Solving_loop" ~function_name:"solve"
@@ -185,12 +226,12 @@ let process_source ?selector_inst ~print_status src =
           Options.Time.start ();
           Options.Time.set_timeout (Options.get_timelimit ());
         end;
-      SAT.reset_refs ();
-      let ftdn_env = FE.init_env ?selector_inst used_context in
+      Api.SAT.reset_refs ();
+      let ftdn_env = Api.FE.init_env ?selector_inst used_context in
       let () =
         try
           List.iter
-            (FE.process_decl ~hook_on_status ftdn_env)
+            (Api.FE.process_decl ~hook_on_status ftdn_env)
             cnf
         with
         | StopProcessDecl -> ()
@@ -205,30 +246,30 @@ let process_source ?selector_inst ~print_status src =
       (* If the status of the SAT environment is inconsistent,
          we have to drop the partial model in order to prevent
          printing wrong model. *)
-      match ftdn_env.FE.res with
+      match ftdn_env.Api.FE.res with
       | `Sat ->
         begin
-          let mdl = Model ((module SAT), partial_model) in
+          let mdl = Model ((module Api.SAT), partial_model) in
           if Options.(get_interpretation () && get_dump_models ()) then begin
             Fmt.pf (Options.Output.get_fmt_models ()) "%a@."
-              FE.print_model partial_model
+              Api.FE.print_model partial_model
           end;
           Sat mdl
         end
       | `Unknown ->
         begin
-          let mdl = Model ((module SAT), partial_model) in
+          let mdl = Model ((module Api.SAT), partial_model) in
           if Options.(get_interpretation () && get_dump_models ()) then begin
-            let ur = SAT.get_unknown_reason partial_model in
+            let ur = Api.SAT.get_unknown_reason partial_model in
             Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
               "@[<v 0>Returned unknown reason = %a@]"
               Sat_solver_sig.pp_ae_unknown_reason_opt ur;
             Fmt.pf (Options.Output.get_fmt_models ()) "%a@."
-              FE.print_model partial_model
+              Api.FE.print_model partial_model
           end;
           Unknown (Some mdl)
         end
-      | `Unsat -> Unsat
+      | `Unsat -> Unsat Explanation.empty
     with Util.Timeout ->
       (* It is still necessary to leave this catch here, because we may
          trigger this exception in between calls of the sat solver. *)
@@ -248,6 +289,36 @@ let process_source ?selector_inst ~print_status src =
     State.create_key ~pipe:"" "named_terms"
   in
 
+  (* Set to true when a query is performed, states for the following SMT
+     instructions that they are working on an environment in which some formulae
+     have been decided and must be reverted back to the one before the check-sat
+     before starting to assert again. *)
+  let is_decision_env : bool State.key =
+    State.create_key ~pipe:"" "is_decision_env"
+  in
+
+  (* Before each query, we push the current environment. This allows to keep a
+     fresh one for the next assertions. *)
+  let push_before_query st =
+    assert (not (State.get is_decision_env st));
+    let module Api = (val (DO.SatSolverModule.get st)) in
+    Api.FE.push 1 Api.env;
+    State.set is_decision_env true st
+  in
+
+  (* The pop corresponding to the previous push. It is applied everytime the
+     mode goes from Sat/Unsat to Assert. *)
+  let pop_if_post_query st =
+    if State.get is_decision_env st then
+      begin
+        let module Api = (val (DO.SatSolverModule.get st)) in
+        Api.FE.pop 1 Api.env;
+        State.set is_decision_env false st
+      end
+    else
+      st
+  in
+
   let set_steps_bound i st =
     try DO.Steps.set i st with
       Invalid_argument _ -> (* Raised by Steps.set_steps_bound *)
@@ -285,7 +356,11 @@ let process_source ?selector_inst ~print_status src =
       recoverable_error "%t" msg; st
     | Util.Timeout ->
       Printer.print_status_timeout None None None None;
-      exit_as_timeout ()
+      (* TODO: Is it an artefact? *)
+      if not (Options.get_timelimit_per_goal ()) then
+        exit_as_timeout ()
+      else
+        st
     | Errors.Error e ->
       recoverable_error "%a" Errors.report e;
       st
@@ -307,7 +382,7 @@ let process_source ?selector_inst ~print_status src =
   in
   let set_partial_model_and_mode solve_res st =
     match solve_res with
-    | Unsat ->
+    | Unsat _ ->
       set_mode Unsat st
     | Unknown None ->
       set_mode Sat st
@@ -390,6 +465,7 @@ let process_source ?selector_inst ~print_status src =
     |> State.set solver_ctx_key solver_ctx
     |> State.set partial_model_key None
     |> State.set named_terms Util.MS.empty
+    |> State.set is_decision_env false
     |> DO.init
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
       ~size_limit ~response_file
@@ -400,10 +476,24 @@ let process_source ?selector_inst ~print_status src =
     |> Typer_Pipe.init ~type_check
   in
 
+  (* Initializing hooks in the mode handler.
+     When we perform a check-sat, the environment we are working on is specific
+     to the Sat or Unsat mode we end up in. If we start asserting again, we must
+     do it in the previous environment. *)
+  let init_full_incremental_hooks () =
+    DO.Mode.reset_hooks ();
+    DO.Mode.add_hook
+      (fun _ ~old:_ ~new_ st ->
+         match new_ with
+         | Assert -> pop_if_post_query st
+         | _ -> st
+      )
+  in
+
   let print_wrn_opt ~loc ~name ty value =
-    warning
-      "%a The option %s expects a %s, got %a"
-      pp_loc loc name ty DStd.Term.print value
+    warning ~loc
+      "The option %s expects a %s, got %a"
+      name ty DStd.Term.print value
   in
 
   let set_sat_solver sat st =
@@ -547,8 +637,8 @@ let process_source ?selector_inst ~print_status src =
   in
 
   let handle_optimize_stmt ~loc ~is_max id (term : DStd.Expr.Term.t) st =
-    let module Sat = (val DO.SatSolverModule.get st) in
-    if not Sat.supports_optimization then (
+    let module Api = (val DO.SatSolverModule.get st) in
+    if not Api.SAT.supports_optimization then (
       let logic_file = State.get State.logic_file st in
       let loc = DStd.Loc.loc logic_file.loc loc in
       recoverable_error ~loc
@@ -570,10 +660,10 @@ let process_source ?selector_inst ~print_status src =
   in
 
   let handle_get_objectives ~loc (_args : DStd.Expr.Term.t list) st =
-    let module Sat = (val DO.SatSolverModule.get st) in
+    let module Api = (val DO.SatSolverModule.get st) in
     let () =
       if Options.get_interpretation () then
-        if not Sat.supports_optimization then
+        if not Api.SAT.supports_optimization then
           recoverable_error ~loc
             "the selected solver does not support optimization"
         else
@@ -714,7 +804,7 @@ let process_source ?selector_inst ~print_status src =
       assignments
   in
 
-  let handle_stmt :
+  let handle_stmt_legacy :
     Frontend.used_context -> State.t ->
     'a D_loop.Typer_Pipe.stmt -> State.t =
     let goal_cnt = ref 0 in
@@ -886,16 +976,395 @@ let process_source ?selector_inst ~print_status src =
           { solver_ctx with ctx = cnf }
         ) st
   in
-  let handle_stmts all_context st l =
+
+  let assume_axiom st name t loc attrs : unit =
+    let module Api = (val (DO.SatSolverModule.get st)) in
+    (* Dolmen adds information about theory extensions and case splits in the
+       [attrs] field of the parsed statements. [attrs] can be arbitrary terms,
+       where the information we care about is encoded as a [Colon]-list of
+       symbols.
+       The few helper functions below are used to extract the information from
+       the [attrs]. More specifically:
+       - "case split" statements have the [DStd.Id.case_split] symbol as an
+          attribute
+       - Theory elements have a 3-length list of symbols as an attribute, of
+          the form [theory_decl; name; extends], where [theory_decl] is the
+          symbol [DStd.Id.theory_decl] and [name] and [extends] are the theory
+          extension name and the base theory name, respectively.
+    *)
+    let rec symbols = function
+      | DStd.Term. { term = Colon ({ term = Symbol sy; _ }, xs); _ } ->
+        Option.bind (symbols xs) @@ fun sys ->
+        Some (sy :: sys)
+      | { term = Symbol sy; _ } -> Some [sy]
+      | _ -> None
+    in
+    let sy_attrs = List.filter_map symbols attrs in
+    let is_case_split =
+      let is_case_split = function
+        | [ sy ] when DStd.Id.(equal sy case_split) -> true
+        | _ -> false
+      in
+      List.exists is_case_split sy_attrs
+    in
+    let theory =
+      let theory =
+        let open DStd.Id in
+        function
+        | [ td; name; extends] when DStd.Id.(equal td theory_decl) ->
+          let name = match name.name with
+            | Simple name -> name
+            | _ ->
+              Fmt.failwith
+                "Internal error: invalid theory extension: %a"
+                print name
+          in
+          let extends = match extends.name with
+            | Simple name ->
+              begin match Util.th_ext_of_string name with
+                | Some extends -> extends
+                | None ->
+                  Errors.typing_error (ThExtError name) loc
+              end
+            | _ ->
+              Fmt.failwith
+                "Internal error: invalid base theory name: %a"
+                print extends
+          in
+          Some (name, extends)
+        | _ -> None
+      in
+      match List.filter_map theory sy_attrs with
+      | [] -> None
+      | [name, extends] -> Some (name, extends)
+      | _ ->
+        Fmt.failwith
+          "%a: Internal error: multiple theories."
+          pp_loc loc
+    in
+    match theory with
+    | Some (th_name, extends) ->
+      let axiom_kind =
+        if is_case_split then Util.Default else Util.Propagator
+      in
+      let e = Translate.make_form name t loc ~decl_kind:Expr.Dtheory in
+      let th_elt = {
+        Expr.th_name;
+        axiom_kind;
+        extends;
+        ax_form = e;
+        ax_name = name;
+      } in
+      Api.FE.th_assume ~loc th_elt Api.env
+    | None ->
+      let e = Translate.make_form name t loc ~decl_kind:Expr.Daxiom in
+      Api.FE.assume ~loc (name, e, true) Api.env
+  in
+
+  (* Push the current environment and performs the query.
+     If an assertion is performed, we have to pop it back. This is handled by
+     the hook on D_state_option.Mode. *)
+  let handle_query ~loc st id attrs contents =
+    let module Api = (val (DO.SatSolverModule.get st)) in
+    let name =
+      match id.DStd.Id.name with
+      | Simple name -> name
+      | Indexed _ | Qualified _ -> assert false
+    in
+    (* First, we check the environment if it already concluded. *)
+    let solve_res =
+      match Api.env.res with
+      | `Unsat -> Unsat Api.env.expl
+      | `Sat
+      | `Unknown ->
+        (* The environment did not conclude yet, or concluded with SAT. We
+           add additional constraints which may change this result. *)
+        begin
+          (* Preprocessing query. *)
+          let goal_sort =
+            match contents with
+            | `Goal _ -> Ty.Thm
+            | `Check _ -> Ty.Sat
+          in
+          let hyps, t =
+            match contents with
+            | `Goal t ->
+              Translate.pp_query t
+            | `Check hyps ->
+              Translate.pp_query ~hyps (DStd.Expr.Term.(of_cst Const._false))
+          in
+          let () =
+            List.iter (
+              fun t ->
+                let name = Ty.fresh_hypothesis_name goal_sort in
+                assume_axiom st name t loc attrs
+            ) hyps
+          in
+          let e = Translate.make_form "" t loc ~decl_kind:Expr.Dgoal in
+          (* Performing the query. *)
+          Api.FE.query ~loc (name, e, goal_sort) Api.env;
+          (* Treatment of the result. *)
+          let partial_model = Api.env.sat_env in
+          (* If the status of the SAT environment is inconsistent,
+             we have to drop the partial model in order to prevent
+             printing wrong model. *)
+          match Api.env.res with
+          | `Sat ->
+            begin
+              let mdl = Model ((module Api.SAT), partial_model) in
+              let () =
+                if Options.(get_interpretation () && get_dump_models ()) then
+                  Api.FE.print_model
+                    (Options.Output.get_fmt_models ())
+                    partial_model
+              in
+              Sat mdl
+            end
+          | `Unknown ->
+            begin
+              let mdl = Model ((module Api.SAT), partial_model) in
+              if Options.(get_interpretation () && get_dump_models ()) then
+                begin
+                  let ur = Api.SAT.get_unknown_reason partial_model in
+                  Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+                    "@[<v 0>Returned unknown reason = %a@]"
+                    Sat_solver_sig.pp_ae_unknown_reason_opt ur;
+                  Api.FE.print_model
+                    (Options.Output.get_fmt_models ())
+                    partial_model
+                end;
+              Unknown (Some mdl)
+            end
+          | `Unsat -> Unsat Api.env.expl
+        end
+    in
+    (* Prints the result. *)
+    print_solve_res loc name solve_res;
+    (* Updates the dolmen state. *)
+    set_partial_model_and_mode solve_res st
+  in
+
+  let handle_solve =
+    let goal_cnt = ref 0 in
+    fun ~loc st id contents attrs ->
+      let module Api = (val DO.SatSolverModule.get st) in
+      let id =
+        match (State.get State.logic_file st).lang with
+        | Some (Smtlib2 _) ->
+          DStd.Id.mk DStd.Namespace.term @@
+          "g_" ^ string_of_int (incr goal_cnt; !goal_cnt)
+        | _ -> id
+      in
+      let contents =
+        match contents with
+        | `Solve (hyps, []) -> `Check hyps
+        | `Solve ([], [t]) -> `Goal t
+        | _ ->
+          fatal_error ~loc "internal error: unknown statement"
+      in
+      (* Performing the query *)
+      handle_query ~loc st id attrs contents
+  in
+
+  (* TODO: reset options to their initial value. *)
+  let reset_state st =
+    st
+    |> State.set partial_model_key None
+    |> State.set solver_ctx_key empty_solver_ctx
+    |> State.set is_decision_env false
+    |> DO.Mode.clear
+    |> DO.ProduceAssignment.clear
+    |> DO.init
+    |> State.set named_terms Util.MS.empty
+  in
+
+  let handle_stmt_full_incremental :
+    Frontend.used_context ->
+    State.t ->
+    [< Typer_Pipe.typechecked | `Check of 'a ] D_loop.Typer_Pipe.stmt ->
+    State.t =
+    fun _all_context st td ->
+      let module Api = (val (DO.SatSolverModule.get st)) in
+      let file = (State.get State.logic_file st).loc in
+      let loc = DStd.Loc.loc file td.loc in
+      match td with
+      (* Set logic *)
+      | { contents = `Set_logic _; _} ->
+        cmd_on_modes st [Start] "set-logic";
+        DO.Mode.set Util.Assert st
+      (* Goal definition *)
+      | { id; attrs; contents = (`Goal _) as contents; _ } ->
+        (* In the non imperative mode, the Solve instruction is handled
+           differently (i.e. no pop/push). *)
+        (* assert (not (Options.get_imperative_mode ())); *)
+        cmd_on_modes st [Assert; Sat; Unsat] "goal";
+        let st = pop_if_post_query st in
+        (* Pushing the environment once. This allows to keep a trace of the old
+           environment in case we want to assert afterwards.
+           The `pop` instruction is handled by the hook on the mode: when we
+           assert anything, we must make sure to go back to `Assert` mode. *)
+        let st = push_before_query st in
+        handle_query ~loc st id attrs contents
+
+      (* Axiom definitions *)
+      | { id = DStd.Id.{name = Simple name; _}; contents = `Hyp t; attrs; _ } ->
+        let st = DO.Mode.set Util.Assert st in
+        assume_axiom st name t loc attrs;
+        st
+
+      | { contents = `Defs defs; _ } ->
+        let st = DO.Mode.set Util.Assert st in
+        let defs = Translate.make_defs defs loc in
+        let () =
+          List.iter
+            (function
+              | `Assume (name, e) ->
+                  Api.FE.assume ~loc (name, e, true) Api.env
+              | `PredDef (e, name) ->
+                  Api.FE.pred_def ~loc (name, e) Api.env
+            )
+            defs
+        in
+        st
+
+      | { contents = `Decls l; _ } ->
+        let st = DO.Mode.set Util.Assert st in
+        let decls = Translate.make_decls l in
+        List.iter (fun decl -> Api.FE.declare ~loc decl Api.env) decls;
+        st
+
+      (* When the next statement is a goal, the solver is called and provided
+         the goal and the current context *)
+      | { id; contents = (`Solve _ as contents); attrs; _ } ->
+        (* In the non imperative mode, the Solve instruction is handled
+           differently (i.e. no pop/push). *)
+        (* assert (not (Options.get_imperative_mode ())); *)
+        cmd_on_modes st [Assert; Unsat; Sat] "check-sat";
+        let st = pop_if_post_query st in
+        (* Pushing the environment once. This allows to keep a trace of the old
+           environment in case we want to assert afterwards.
+           The `pop` instruction is handled by the hook on the mode: when we
+           assert anything, we must make sure to go back to `Assert` mode. *)
+        let st = push_before_query st in
+        handle_solve ~loc st id contents attrs
+
+      | {contents = `Set_option
+             { DStd.Term.term =
+                 App ({ term = Symbol { name = Simple name; _ }; _ }, [value]);
+               _
+             }; _ } ->
+        handle_option ~loc name value st
+
+      | {contents = `Set_option _; _} ->
+        recoverable_error "Invalid set-option";
+        st
+
+      | {contents = `Get_model; _ } ->
+        cmd_on_modes st [Sat] "get-model";
+        if Options.get_interpretation () then
+          let () = match State.get partial_model_key st with
+            | Some (Model ((module SAT), env)) ->
+              let module FE = Frontend.Make (SAT) in
+              Fmt.pf (Options.Output.get_fmt_regular ()) "%a@."
+                FE.print_model env
+            | None ->
+              recoverable_error ~loc "No model produced."
+          in
+          st
+        else
+          begin
+            recoverable_error ~loc
+              "Model generation disabled (try --produce-models)";
+            st
+          end
+
+      | {contents = `Reset; _} ->
+        let () = Steps.reset_steps () in
+        reset_state st
+
+      | {contents = `Exit; _} -> raise Exit
+
+      | {contents = `Echo str; _} ->
+        let new_str = String.concat "\"\"" (String.split_on_char '"' str) in
+        Fmt.pf
+          (Options.Output.get_fmt_regular ())
+          "\"%s\"@."
+          new_str;
+        st
+
+      | {contents = `Get_info kind; _ } ->
+        handle_get_info ~loc st kind;
+        st
+
+      | {contents = `Get_assignment; _} ->
+        begin
+          cmd_on_modes st [Sat] "get-assignment";
+          match State.get partial_model_key st with
+          | Some Model ((module SAT), partial_model) ->
+            if DO.ProduceAssignment.get st then
+              handle_get_assignment
+                ~get_value:(SAT.get_value partial_model)
+                st
+            else
+              recoverable_error ~loc
+                "Produce assignments disabled; \
+                 add (set-option :produce-assignments true)";
+            st
+          | None ->
+            recoverable_error ~loc
+              "No model produced, cannot execute get-assignment.";
+            st
+        end
+
+      | {contents = `Other (custom, args); loc; _} ->
+        handle_custom_statement ~loc custom args st
+
+      | {contents = `Pop n; _} ->
+        Api.FE.pop ~loc n Api.env; st
+        |> set_mode Assert
+
+      | {contents = `Push n; _} ->
+        Api.FE.push ~loc n Api.env; st
+        |> set_mode Assert
+
+      | td ->
+        Printer.print_dbg ~header:true
+          "Ignoring statement: %a" Typer_Pipe.print td;
+        st
+  in
+
+  (* Handle each statement one after the other.
+     Still experimental due to push & pop issues. *)
+  let handle_stmts_full_incremental all_context st l =
+    let rec aux named_map st = function
+      | [] -> State.set named_terms named_map st
+      | stmt :: tl ->
+        let st = handle_stmt_full_incremental all_context st stmt in
+        let named_map = add_if_named ~acc:named_map stmt in
+        aux named_map st tl
+    in
+    aux (State.get named_terms st) st l
+  in
+
+  let handle_stmts_legacy all_context st l =
     let rec aux named_map st = function
       | [] -> State.set named_terms named_map st
       | stmt :: tl ->
-        let st = handle_stmt all_context st stmt in
+        let st = handle_stmt_legacy all_context st stmt in
         let named_map = add_if_named ~acc:named_map stmt in
         aux named_map st tl
     in
     aux (State.get named_terms st) st l
   in
+
+  let handle_stmts =
+    if Options.get_imperative_mode () then (
+      init_full_incremental_hooks ();
+      handle_stmts_full_incremental
+    ) else
+      handle_stmts_legacy
+  in
+
   let d_fe src =
     let logic_file, st = mk_state src in
     let () = on_strict_mode (O.get_strict_mode ()) in
diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml
index d655bfcd3..ff5804117 100644
--- a/src/lib/frontend/d_state_option.ml
+++ b/src/lib/frontend/d_state_option.ml
@@ -20,47 +20,79 @@ module O = Options
 module State = D_loop.State
 module Typer = D_loop.Typer
 
+type 'a hook =
+  'a D_loop.State.key ->
+  old:'a ->
+  new_:'a ->
+  D_loop.Typer.state ->
+  D_loop.Typer.state
+
 module type Accessor = sig
-  (** The data saved in the state. *)
   type t
 
-  (** Returns the option stored in the state. If it has not been registered,
-      fetches the default option in the module Options. *)
   val get : D_loop.Typer.state -> t
 end
 
 module type S = sig
   include Accessor
 
-  (** Sets the option on the dolmen state. *)
   val set : t -> D_loop.Typer.state -> D_loop.Typer.state
-
-  (** Clears the option from the state. *)
   val clear : D_loop.Typer.state -> D_loop.Typer.state
 end
 
+module type S_with_hooks = sig
+  include S
+
+  val reset_hooks : unit -> unit
+  val add_hook : t hook -> unit
+end
+
 let create_opt
     (type t)
-    ?(on_update=(fun _ _ -> Fun.id))
+    ?on_update
     (key : string)
-    (get : unit -> t) : (module S with type t = t) =
+    (default_get : unit -> t) : (module S_with_hooks with type t = t) =
   (module struct
     type nonrec t = t
 
+    let on_update_base =
+      match on_update with
+      | None -> []
+      | Some f -> [f]
+
+    let on_update_list = ref on_update_base
+
     let key = State.create_key ~pipe:"" key
 
-    let set opt st =
-      st
-      |> on_update key opt
-      |> State.set key opt
+    let apply_hooks ~old ~new_ st =
+      List.fold_left
+        (fun acc f -> f key ~old ~new_ acc)
+        st
+        !on_update_list
 
     let unsafe_get st = State.get key st
 
-    let clear st = State.update_opt key (fun _ -> None) st
-
     let get st =
       try unsafe_get st with
-      | State.Key_not_found _ -> get ()
+      | State.Key_not_found _ -> default_get ()
+
+    let set new_ st =
+      let old = get st in
+      let st = apply_hooks ~old ~new_ st in
+      State.set key new_ st
+
+    let clear st =
+      let old = get st in
+      let new_ = default_get () in
+      st
+      |> apply_hooks ~old ~new_
+      |> State.update_opt key (fun _ -> None)
+    (* S: [clear] rebuilds a new default value for the hooks, but does not put
+       it back on the state. *)
+
+    let reset_hooks () = on_update_list := on_update_base
+
+    let add_hook h = on_update_list := h :: !on_update_list
   end)
 
 (* The current mode of the sat solver. Serves as a flag for some options that
@@ -71,12 +103,12 @@ module Mode = (val (create_opt "start_mode") (fun _ -> Util.Start))
    in start mode. *)
 let create_opt_only_start_mode
     (type t)
-    ?(on_update=(fun _ _ -> Fun.id))
+    ?(on_update=(fun _ ~old:_ ~new_:_ -> Fun.id))
     (key : string)
-    (get : unit -> t) : (module S with type t = t) =
-  let on_update k opt st =
+    (get : unit -> t) : (module S_with_hooks with type t = t) =
+  let on_update k ~old ~new_ st =
     match Mode.get st with
-    | Util.Start -> on_update k opt st
+    | Util.Start -> on_update k ~old ~new_ st
     | curr_mode -> Errors.invalid_set_option curr_mode key
   in
   create_opt ~on_update key get
@@ -91,14 +123,28 @@ module StrictMode =
 module ProduceAssignment =
   (val (create_opt_only_start_mode "produce_assignment" (fun _ -> false)))
 
+module type Sat_solver_api = sig
+  module SAT : Sat_solver_sig.S
+  module FE : Frontend.S with type sat_env = SAT.t
+
+  val env : FE.env
+end
+
 let get_sat_solver
     ?(sat = O.get_sat_solver ())
     ?(no_th = O.get_no_theory ())
-    () =
+    () : (module Sat_solver_api) =
   let module SatCont =
     (val (Sat_solver.get sat) : Sat_solver_sig.SatContainer) in
   let module TH = (val Sat_solver.get_theory ~no_th) in
-  (module SatCont.Make(TH) : Sat_solver_sig.S)
+  let module SAT : Sat_solver_sig.S = SatCont.Make(TH) in
+  let module FE : Frontend.S with type sat_env = SAT.t = Frontend.Make (SAT) in
+  (module struct
+    module SAT = SAT
+    module FE = FE
+
+    let env = FE.init_env (Frontend.init_all_used_context ())
+  end)
 
 module SatSolverModule =
   (val (
@@ -107,15 +153,17 @@ module SatSolverModule =
        (fun _ -> get_sat_solver ())))
 
 let msatsolver =
-  let on_update _ sat st =
-    SatSolverModule.set (get_sat_solver ~sat ()) st
+  let on_update _ ~old:_ ~new_ st =
+    SatSolverModule.set (get_sat_solver ~sat:new_ ()) st
   in
   (create_opt_only_start_mode ~on_update "sat_solver" O.get_sat_solver)
 
 module SatSolver = (val msatsolver)
 
 let msteps =
-  let on_update _ sat st = Steps.set_steps_bound sat; st in
+  let on_update _ ~old:_ ~new_ st =
+    Steps.set_steps_bound new_; st
+  in
   (create_opt_only_start_mode ~on_update "steps_bound" O.get_steps_bound)
 
 module Steps = (val msteps)
diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli
index 1c31f6ddf..58cd31ebe 100644
--- a/src/lib/frontend/d_state_option.mli
+++ b/src/lib/frontend/d_state_option.mli
@@ -20,6 +20,14 @@
     an option that can be set, fetched et reset independently from the
     Options module, which is used as a static reference. *)
 
+(** A hook which is called when an option is updated. *)
+type 'a hook =
+  'a D_loop.State.key ->
+  old:'a ->
+  new_:'a ->
+  D_loop.Typer.state ->
+  D_loop.Typer.state
+
 module type Accessor = sig
   (** The data saved in the state. *)
   type t
@@ -37,10 +45,26 @@ module type S = sig
 
   (** Resets the option to its default value in Options. *)
   val clear : D_loop.Typer.state -> D_loop.Typer.state
+
+  (** Sets the option on the dolmen state. *)
+  val set : t -> D_loop.Typer.state -> D_loop.Typer.state
+
+  (** Clears the option from the state. *)
+  val clear : D_loop.Typer.state -> D_loop.Typer.state
+end
+
+module type S_with_hooks = sig
+  include S
+
+  (** Resets all hooks, except the one registered at initialization. *)
+  val reset_hooks : unit -> unit
+
+  (** Adds a hook which is called during the update of the value. *)
+  val add_hook : t hook -> unit
 end
 
 (** The current mode of the solver. *)
-module Mode : S with type t = Util.mode
+module Mode : S_with_hooks with type t = Util.mode
 
 (** Options are divided in two categories:
     1. options that can be updated anytime;
@@ -59,9 +83,17 @@ module ProduceAssignment : S with type t = bool
 (** The Sat solver used. When set, updates the SatSolverModule defined below. *)
 module SatSolver : S with type t = Util.sat_solver
 
+module type Sat_solver_api = sig
+  module SAT : Sat_solver_sig.S
+
+  module FE : Frontend.S with type sat_env = SAT.t
+
+  val env : FE.env
+end
+
 (** The Sat solver module used for the calculation. This option's value depends
     on SatSolver: when SatSolver is updated, this one also is. *)
-module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S)
+module SatSolverModule : Accessor with type t = (module Sat_solver_api)
 
 (** Option for setting the max number of steps. Interfaces with the toplevel
     Steps module.
diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
index b0d884f5f..28e7f052f 100644
--- a/src/lib/frontend/frontend.ml
+++ b/src/lib/frontend/frontend.ml
@@ -139,6 +139,8 @@ module type S = sig
 
   val init_env : ?selector_inst:(Expr.t -> bool) -> used_context -> env
 
+  val declare : Id.typed process
+
   val push : int process
 
   val pop : int process
@@ -425,6 +427,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
   let wrap_f f ?loc x env =
     check_if_over (handle_sat_exn f ?loc x) env
 
+  let declare = wrap_f internal_decl
+
   let push = wrap_f internal_push
 
   let pop = wrap_f internal_pop
diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli
index 68265856e..09dff1c52 100644
--- a/src/lib/frontend/frontend.mli
+++ b/src/lib/frontend/frontend.mli
@@ -66,6 +66,8 @@ module type S = sig
       the user. *)
   type 'a process = ?loc:Dolmen.Std.Loc.loc -> 'a -> env -> unit
 
+  val declare : Id.typed process
+
   val push : int process
 
   val pop : int process
diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml
index eef3e7487..487886483 100644
--- a/src/lib/frontend/translate.ml
+++ b/src/lib/frontend/translate.ml
@@ -1758,6 +1758,134 @@ let rec is_pure_term t =
   | Sy.Op Tite -> false
   | _ -> List.for_all is_pure_term xs
 
+let make_defs defs loc =
+  (* For a mutually recursive definition, we have to add all the function
+     names in a row. *)
+  List.iter (fun (def : Typer_Pipe.def) ->
+      match def with
+      | `Term_def (_, ({ path; _ } as tcst), _, _, _) ->
+        let name_base = get_basename path in
+        let sy = Sy.name ~defined:true name_base in
+        Cache.store_sy tcst sy
+      | `Type_alias _ -> ()
+      | `Instanceof _ ->
+        (* These statements are only used in models when completing a
+           polymorphic partially-defined bulitin and should not end up
+           here. *)
+        assert false
+    ) defs;
+  List.filter_map (fun (def : Typer_Pipe.def) ->
+      match def with
+      | `Term_def ( _, ({ path; tags; _ } as tcst), tyvars, terml, body) ->
+        Cache.store_tyvl tyvars;
+        let name_base = get_basename path in
+
+        let binders, defn =
+          let rty = dty_to_ty body.term_ty in
+          let binders, rev_args =
+            List.fold_left (
+              fun (binders, acc) (DE.{ path; id_ty; _ } as tv) ->
+                let ty = dty_to_ty id_ty in
+                let v = Var.of_string (get_basename path) in
+                let sy = Sy.var v in
+                Cache.store_sy tv sy;
+                let e = E.mk_term sy [] ty in
+                Var.Map.add v ty binders, e :: acc
+            ) (Var.Map.empty, []) terml
+          in
+          let sy = Cache.find_sy tcst in
+          let e = E.mk_term sy (List.rev rev_args) rty in
+          binders, e
+        in
+
+        begin match DStd.Tag.get tags DE.Tags.predicate with
+          | Some () ->
+            let decl_kind = E.Dpredicate defn in
+            let ff = mk_expr ~loc ~name_base ~toplevel:false ~decl_kind body in
+            let qb = E.mk_eq ~iff:true defn ff in
+            let ff =
+              E.mk_forall name_base
+                Dolmen.Std.Loc.dummy binders [] qb ~toplevel:true
+                ~decl_kind
+            in
+            assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
+            let ff = E.purify_form ff in
+            let e =
+              if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
+              else
+                E.mk_forall name_base loc
+                  Var.Map.empty [] ff ~toplevel:true ~decl_kind
+            in
+            Some (`PredDef (e, name_base))
+          | None ->
+            let decl_kind = E.Dfunction defn in
+            let ff =
+              mk_expr ~loc ~name_base
+                ~toplevel:false ~decl_kind body
+            in
+            let iff = Ty.equal (Expr.type_info defn) (Ty.Tbool) in
+            let qb = E.mk_eq ~iff defn ff in
+            let ff =
+              E.mk_forall name_base DStd.Loc.dummy binders [] qb ~toplevel:true
+                ~decl_kind
+            in
+            assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
+            let ff = E.purify_form ff in
+            let e =
+              if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
+              else
+                E.mk_forall name_base loc
+                  Var.Map.empty [] ff ~toplevel:true ~decl_kind
+            in
+            if Options.get_verbose () then
+              Format.eprintf "defining term of %a@." DE.Term.print body;
+            Some (`Assume (name_base, e))
+        end
+      | `Type_alias _ -> None
+      | `Instanceof _ ->
+        (* These statements are only used in models when completing a
+           polymorphic partially-defined bulitin and should not end up
+           here. *)
+        assert false
+    ) defs
+
+let make_decls = function
+  | [] -> assert false (* We could probably just return (). *)
+  | [td] ->
+    begin
+      match td with
+      | `Type_decl (td, _def) -> mk_ty_decl td; []
+      | `Term_decl td -> [mk_term_decl td];
+    end
+  | dcl ->
+    let rec aux term_acc acc tdl =
+      (* for now, when acc has more than one element it is assumed that the
+         types are mutually recursive. Which is not necessarily the case.
+         But it doesn't affect the execution.
+      *)
+      match tdl with
+      | `Term_decl td :: tl ->
+        begin match acc with
+          | [] -> ()
+          | [otd] -> mk_ty_decl otd
+          | _ -> mk_mr_ty_decls (List.rev acc)
+        end;
+        let t = mk_term_decl td in
+        aux (t :: term_acc) [] tl
+
+      | `Type_decl (td, _def) :: tl ->
+        aux term_acc (td :: acc) tl
+
+      | [] ->
+        begin match acc with
+          | [] -> ()
+          | [otd] -> mk_ty_decl otd
+          | _ ->  mk_mr_ty_decls (List.rev acc)
+        end;
+        term_acc
+    in
+    aux [] [] dcl
+
 let make file acc stmt =
   let rec aux acc (stmt: _ Typer_Pipe.stmt) =
     let st_loc = Dolmen.Std.Loc.loc file stmt.loc in
diff --git a/src/lib/frontend/translate.mli b/src/lib/frontend/translate.mli
index f54422fc0..7c4e9524d 100644
--- a/src/lib/frontend/translate.mli
+++ b/src/lib/frontend/translate.mli
@@ -29,8 +29,7 @@ val dty_to_ty : ?update:bool -> ?is_var:bool -> D_loop.DStd.Expr.ty -> Ty.t
     - If [dty] is a type application, or an arrow type, only its return type
       is converted since those have no counterpart in AE's [Ty] module. The
       function arguments' types or the type paramters ought to be converted
-      individually.
-*)
+      individually. *)
 
 val make_form :
   string ->
@@ -52,6 +51,62 @@ val make :
     type-checked statement [stmt] and appends them to [acc].
 *)
 
+val make_defs :
+  D_loop.Typer_Pipe.def list ->
+  Dolmen.Std.Loc.loc ->
+  [> `Assume of string * Expr.t  | `PredDef of Expr.t * string ] list
+(** [make_defs dlist loc]
+    Transforms the dolmen definition list [dlist] into an Alt-Ergo definition.
+    Dolmen definitions can be:
+    - Definitions, that either are predicates (transformed in `PredDef) or
+      simple definitions (transformed in `Assume);
+    - Type aliases (filtered out);
+    - Statements used in models (they must not be in the input list, otherwise
+      this function fails). *)
+
+val mk_expr :
+  ?loc:Dolmen.Std.Loc.loc ->
+  ?name_base:string ->
+  ?toplevel:bool ->
+  decl_kind:Expr.decl_kind -> D_loop.DStd.Expr.term -> Expr.t
+(** [make_expr ~loc ~name_base ~toplevel ~decl_kind term]
+
+    Builds an Alt-Ergo hashconsed expression from a dolmen term. *)
+
+val make_form :
+  string ->
+  D_loop.DStd.Expr.term ->
+  Dolmen.Std.Loc.loc ->
+  decl_kind:Expr.decl_kind ->
+  Expr.t
+(** [make_form name term loc decl_kind]
+    Same as `make_expr`, but for formulas. It applies a purification step and
+    processes free variables by adding a forall quantifier. *)
+
+val pp_query :
+  ?hyps:D_loop.DStd.Expr.term list ->
+  D_loop.DStd.Expr.term ->
+  D_loop.DStd.Expr.term list * D_loop.DStd.Expr.term
+(** Preprocesses the body of a goal by:
+    - removing the top-level universal quantifiers and considering their
+      quantified variables as uninsterpreted symbols.
+    - transforming a given formula: [a[1] -> a[2] -> ... -> a[n]] in which
+      the [a[i]]s are subformulas and [->] is a logical implication, to a set of
+      hypotheses [{a[1]; ...; a[n-1]}], and a goal [a[n]] whose validity is
+      verified by the solver.
+      If additional hypotheses are provided in [hyps], they are preprocessed and
+      added to the set of hypotheses in the same way as the left-hand side of
+      implications. In other words, [pp_query ~hyps:[h1; ...; hn] t] is the same
+      as [pp_query (h1 -> ... -> hn t)], but more convenient if the some
+      hypotheses are already separated from the goal.
+      Returns a list of hypotheses and the new goal body. *)
+
+val make_decls :
+  D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list
+(** Registers the declarations in the cache. If there are more than one element
+    in the list, it is assumed they are mutually recursive (but if it is not the
+    case, it still work). *)
+
 val builtins :
   Dolmen_loop.State.t ->
   D_loop.Typer.lang ->
diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml
index 761a4b943..9c1325e11 100644
--- a/src/lib/util/options.ml
+++ b/src/lib/util/options.ml
@@ -286,6 +286,7 @@ let preludes = ref []
 let theory_preludes = ref Theories.default_preludes
 let type_only = ref false
 let type_smt2 = ref false
+let imperative_mode = ref false
 
 let set_answers_with_loc b = answers_with_loc := b
 let set_output_with_colors b = output_with_colors := b
@@ -300,6 +301,8 @@ let set_theory_preludes t = theory_preludes := t
 let set_type_only b = type_only := b
 let set_type_smt2 b = type_smt2 := b
 
+let set_imperative_mode b = imperative_mode := b
+
 let get_answers_with_locs () = !answers_with_loc
 let get_output_with_colors () = !output_with_colors
 let get_output_with_headers () = !output_with_headers
@@ -311,6 +314,7 @@ let get_preludes () = !preludes
 let get_theory_preludes () = !theory_preludes
 let get_type_only () = !type_only
 let get_type_smt2 () = !type_smt2
+let get_imperative_mode () = !imperative_mode
 
 (** Internal options *)
 
diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli
index f67d8e76a..622895e3e 100644
--- a/src/lib/util/options.mli
+++ b/src/lib/util/options.mli
@@ -294,6 +294,9 @@ val set_triggers_var : bool -> unit
 (** Set [type_smt2] accessible with {!val:get_type_smt2} *)
 val set_type_smt2 : bool -> unit
 
+(** Set [imperative_mode] accessible with {!val:get_imperative_mode} *)
+val set_imperative_mode : bool -> unit
+
 (** Set [unsat_core] accessible with {!val:get_unsat_core} *)
 val set_unsat_core : bool -> unit
 
@@ -640,6 +643,10 @@ val get_type_only : unit -> bool
 val get_type_smt2 : unit -> bool
 (** Default to [false] *)
 
+(** [true] if the solving loop works in a imperative mode. *)
+val get_imperative_mode : unit -> bool
+(** Default to [false] *)
+
 (** {4 Internal options} *)
 
 (** [true] if the GC is prevented from collecting hashconsed data structrures
diff --git a/tools/gentest.ml b/tools/gentest.ml
index b6e20987a..0443624e1 100644
--- a/tools/gentest.ml
+++ b/tools/gentest.ml
@@ -353,6 +353,9 @@ let () =
   let solvers = [
     ("runtest-quick", "default",
      [ "--output=smtlib2"])
+  ; ("runtest-quick", "incremental",
+     [ "--output=smtlib2"
+     ; "--incremental-mode"])
   ; ("runtest-quick", "tableaux",
      [ "--output=smtlib2"
      ; "--sat-solver Tableaux" ])