diff --git a/Makefile.in b/Makefile.in
index 79aa061c069e7eb4f835ed20bdd39076bc09a245..807c8acec27bbe848600ea08a09365202492dd19 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1635,74 +1635,7 @@ TRYWHY3CMO = $(addsuffix .cmo, $(TRYWHY3MODULES))
 
 $(TRYWHY3DEP) $(TRYWHY3CMO): INCLUDES += -I src/trywhy3
 
-ALTERGODIR=src/trywhy3/alt-ergo
-
-ALTERGOINCLUDES = $(addprefix -I $(ALTERGODIR)/, lib/util lib/structures lib/parsing lib/frontend lib/reasoners parsers/why)
-
-ALTERGOLIBS = \
-	util/config \
-	util/version \
-	util/emap \
-	util/myUnix \
-	util/myDynlink \
-	util/myZip \
-	util/util \
-	util/lists \
-	util/numsNumbers \
-	util/numbers \
-	util/options \
-	util/cmdline_parser \
-	util/timers \
-	util/gc_debug \
-	util/loc \
-	util/hconsing \
-	util/hstring \
-	structures/exception \
-	structures/symbols \
-	structures/ty \
-	structures/parsed \
-	structures/errors \
-	structures/typed \
-	structures/term \
-	structures/fpa_rounding \
-	structures/literal \
-	structures/formula \
-	structures/explanation \
-	structures/commands \
-	structures/profiling \
-	reasoners/matching \
-	reasoners/instances \
-	reasoners/polynome \
-	reasoners/ac \
-	reasoners/uf \
-	reasoners/use \
-	reasoners/intervals \
-	reasoners/inequalities \
-	reasoners/intervalCalculus \
-	reasoners/arith \
-	reasoners/records \
-	reasoners/bitv \
-	reasoners/arrays \
-	reasoners/sum \
-	reasoners/combine \
-	reasoners/ccx \
-	reasoners/theory \
-	reasoners/fun_sat \
-	reasoners/sat_solver \
-	frontend/triggers \
-	frontend/typechecker \
-	frontend/cnf \
-	frontend/parsed_interface \
-	frontend/frontend \
-	frontend/parsers
-
-ALTERGOPARSERS = \
-	why/why_parser \
-	why/why_lexer
-
-ALTERGOCMO = \
-	$(addprefix $(ALTERGODIR)/lib/, $(addsuffix .cmo,$(ALTERGOLIBS))) \
-	$(addprefix $(ALTERGODIR)/parsers/, $(addsuffix .cmo,$(ALTERGOPARSERS)))
+ALTERGOINCLUDES = $(addprefix -I src/trywhy3/alt-ergo/, lib/util lib/structures lib/parsing lib/frontend lib/reasoners parsers)
 
 TRYWHY3_PACK = \
 	trywhy3.js trywhy3.html trywhy3.css \
@@ -1731,7 +1664,7 @@ src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/trywhy3.con
 		--file=trywhy3.conf:/ \
 		--file=try_alt_ergo.drv:/ \
 		`find stdlib -name "*.mlw" -printf " --file=%p:/%p"` \
-	+dynlink.js +toplevel.js $<
+		+dynlink.js +toplevel.js $<
 
 src/trywhy3/why3_worker.byte: $(WHY3CMA) lib/plugins/python.cmo lib/plugins/microc.cmo \
 		$(addprefix src/trywhy3/, bindings.cmo worker_proto.cmo why3_worker.cmo)
@@ -1740,10 +1673,10 @@ src/trywhy3/why3_worker.byte: $(WHY3CMA) lib/plugins/python.cmo lib/plugins/micr
 src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
 	js_of_ocaml $(JSOO_DEBUG) +dynlink.js +toplevel.js $<
 
-src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) $(addprefix src/trywhy3/, worker_proto.cmo alt_ergo_worker.cmo)
-	$(OCAMLFIND) ocamlc -o $@ -package num -package dynlink -package str -package unix -package camlzip -package ocplib-simplex -package js_of_ocaml -linkpkg $^
+src/trywhy3/alt_ergo_worker.byte: $(addprefix src/trywhy3/, alt_ergo.cma worker_proto.cmo alt_ergo_worker.cmo)
+	$(OCAMLFIND) ocamlc -o $@ -package num -package str -package ocplib-simplex -package js_of_ocaml -linkpkg $^
 
-src/trywhy3/alt_ergo_worker.cmo: BFLAGS += $(ALTERGOINCLUDES)
+src/trywhy3/alt_ergo_worker.cmo: INCLUDES += $(ALTERGOINCLUDES)
 
 src/trywhy3/%.cmo: src/trywhy3/%.ml
 	$(OCAMLFIND) ocamlc $(BFLAGS) -c $<
@@ -1751,9 +1684,12 @@ src/trywhy3/%.cmo: src/trywhy3/%.ml
 src/trywhy3/%.cmi: src/trywhy3/%.mli
 	$(OCAMLFIND) ocamlc $(BFLAGS) -c $<
 
-$(addprefix src/trywhy3/, worker_proto.cmo why3_worker.cmo alt_ergo_worker.cmo): BFLAGS += -package js_of_ocaml
+src/trywhy3/alt_ergo.cma:
+	$(MAKE) -C src/trywhy3 alt_ergo.cma
 
-$(addprefix src/trywhy3/, bindings.cmo trywhy3.cmo): BFLAGS += -package js_of_ocaml -package js_of_ocaml-ppx
+$(addprefix src/trywhy3/, worker_proto.cmo why3_worker.cmo alt_ergo_worker.cmo): EXTPKGS = js_of_ocaml
+
+$(addprefix src/trywhy3/, bindings.cmo trywhy3.cmo): EXTPKGS = js_of_ocaml js_of_ocaml-ppx
 
 ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
 -include $(TRYWHY3DEP)
diff --git a/src/trywhy3/Makefile b/src/trywhy3/Makefile
index 9009f0d40e31a915862cc20c98a35f0092b6e540..cb5815bdc4361b4ba7306997cbf3827cc44c7e5a 100644
--- a/src/trywhy3/Makefile
+++ b/src/trywhy3/Makefile
@@ -1,10 +1,127 @@
+ALTERGOLIBS = \
+	util/config \
+	util/version \
+	util/emap \
+	util/myUnix \
+	util/myDynlink \
+	util/util \
+	util/lists \
+	util/numsNumbers \
+	util/numbers \
+	util/options \
+	util/timers \
+	util/gc_debug \
+	util/loc \
+	util/hconsing \
+	util/hstring \
+	util/vec \
+	util/iheap \
+	structures/var \
+	structures/ty \
+	structures/symbols \
+	structures/parsed \
+	structures/errors \
+	structures/typed \
+	structures/expr \
+	structures/fpa_rounding \
+	structures/satml_types \
+	structures/explanation \
+	structures/commands \
+	structures/profiling \
+	structures/xliteral \
+	reasoners/matching \
+	reasoners/polynome \
+	reasoners/ac \
+	reasoners/adt \
+	reasoners/arith \
+	reasoners/arrays \
+	reasoners/bitv \
+	reasoners/enum \
+	reasoners/ite \
+	reasoners/records \
+	reasoners/shostak \
+	reasoners/uf \
+	reasoners/use \
+	reasoners/intervals \
+	reasoners/inequalities \
+	reasoners/intervalCalculus \
+	reasoners/records_rel \
+	reasoners/ite_rel \
+	reasoners/enum_rel \
+	reasoners/bitv_rel \
+	reasoners/arrays_rel \
+	reasoners/adt_rel \
+	reasoners/relation \
+	reasoners/ccx \
+	reasoners/theory \
+	reasoners/instances \
+	reasoners/satml \
+	reasoners/satml_frontend \
+	reasoners/satml_frontend_hybrid \
+	reasoners/fun_sat \
+	reasoners/sat_solver \
+	frontend/cnf \
+	frontend/typechecker \
+	frontend/parsed_interface \
+	frontend/frontend
 
-WHY3=moloch:/users/www-perso/projets/why3
+ALTERGOPARSERS = \
+	myZip \
+	parsers_loader \
+	parsers \
+	why_parser \
+	why_lexer
 
-install-help-microc:
-	scp help_micro-C.html $(WHY3)/micro-C/trywhy3_help.html
-	scp trywhy3_help.css $(WHY3)/micro-C/
+ALTERGOCMO = \
+	$(ALTERGOLIBS:%=alt-ergo/lib/%.cmo) \
+	$(ALTERGOPARSERS:%=alt-ergo/parsers/%.cmo)
 
-install-help-python:
-	scp help_python.html $(WHY3)/python/trywhy3_help.html
-	scp trywhy3_help.css $(WHY3)/python/
+ALTERGOINTFS = \
+	util/numbersInterface \
+	reasoners/th_util \
+	reasoners/matching_types \
+	reasoners/sig \
+	reasoners/sig_rel \
+	reasoners/sat_solver_sig
+
+ALTERGODEP = \
+	$(ALTERGOLIBS:%=alt-ergo/lib/%.dep) \
+	$(ALTERGOPARSERS:%=alt-ergo/parsers/%.dep) \
+	$(ALTERGOINTFS:%=alt-ergo/lib/%.dep) \
+
+INCLUDES = $(addprefix -I alt-ergo/, lib/util lib/structures lib/reasoners lib/frontend parsers)
+
+.PHONY: depend clean
+
+alt_ergo.cma: $(ALTERGOCMO)
+	ocamlfind ocamlc -a -o $@ $^
+
+alt-ergo/parsers/why_parser.ml: alt-ergo/parsers/why_parser.mly
+	menhir $<
+
+alt-ergo/parsers/why_lexer.ml: alt-ergo/parsers/why_lexer.mll
+	ocamllex $<
+
+depend: $(ALTERGODEP)
+
+%.dep: %.ml | alt-ergo/parsers/why_parser.ml alt-ergo/parsers/why_lexer.ml
+	ocamldep $(INCLUDES) $< $<i > $@
+
+%.dep: %.mli | alt-ergo/parsers/why_parser.ml alt-ergo/parsers/why_lexer.ml
+	ocamldep $(INCLUDES) $< > $@
+
+PACKAGES = $(addprefix -package , num ocplib-simplex)
+
+%.cmo: %.ml
+	ocamlfind ocamlc $(PACKAGES) $(INCLUDES) -c $<
+
+%.cmi: %.mli
+	ocamlfind ocamlc $(PACKAGES) $(INCLUDES) -c $<
+
+alt-ergo/lib/util/myUnix.cmo: PACKAGES += -package js_of_ocaml -package js_of_ocaml-ppx
+
+-include $(ALTERGODEP)
+
+clean:
+	rm -f $(ALTERGODEP) alt-ergo/parsers/why_parser.mli alt-ergo/parsers/why_parser.ml alt-ergo/parsers/why_lexer.ml
+	find alt-ergo -name '*.cm*' -delete
diff --git a/src/trywhy3/README.md b/src/trywhy3/README.md
index 6792ba4ff2473757144b05a515e6027380387f73..b3fc6bb931f571925d6f333703fd587e1047ed80 100644
--- a/src/trywhy3/README.md
+++ b/src/trywhy3/README.md
@@ -15,28 +15,18 @@ Instructions to build TryWhy3
 
   * Install Alt-Ergo
 
-      - get the sources of Alt-Ergo 2.0 and put them in directory `src/trywhy3/`,
-        e.g., in `src/trywhy3/alt-ergo/`
+      - get the sources of Alt-Ergo and put them in directory `src/trywhy3/`
 
             cd src/trywhy3
-            wget http://alt-ergo.ocamlpro.com/http/alt-ergo-2.0.0/alt-ergo-2.0.0.tar.gz
-            tar xzf alt-ergo-2.0.0.tar.gz
-            mv alt-ergo-2.0.0 alt-ergo
+            wget http://alt-ergo.ocamlpro.com/http/alt-ergo-2.3.3/alt-ergo-2.3.3.tar.gz
+            tar xzf alt-ergo-2.3.3.tar.gz
+            mv alt-ergo-2.3.3 alt-ergo
 
       - apply the patch `alt-ergo.patch`
 
-            cd alt-ergo
+            cd src/trywhy3/alt-ergo
             patch -p1 < ../alt-ergo.patch
 
-      - compile Alt-Ergo
-
-            ./configure
-            make byte
-
-  * If necessary, change the following line of `Makefile.in` to point to Alt-Ergo sources
-
-        ALTERGODIR=src/trywhy3/alt-ergo
-
   * Compile with
 
         make trywhy3
@@ -66,6 +56,6 @@ Customization
   * To add some predefined examples, put some `.mlw` files in the
     `examples/` subdirectory and generate an index as follows:
 
-        cp some_file.mlw examples/
-        cd examples/
+        cp some_file.mlw src/trywhy3/examples/
+        cd src/trywhy3/examples/
         ../gen_index.sh *.mlw > index.txt
diff --git a/src/trywhy3/alt-ergo.patch b/src/trywhy3/alt-ergo.patch
index 8264b2e08808e1db6c6a70c2ab0c96da3d93a489..06a932143c53aee3cb0d99ca777345a19193cb3d 100644
--- a/src/trywhy3/alt-ergo.patch
+++ b/src/trywhy3/alt-ergo.patch
@@ -1,42 +1,250 @@
-diff -r -u alt-ergo-2.0.0/lib/reasoners/fun_sat.ml alt-ergo/lib/reasoners/fun_sat.ml
---- alt-ergo-2.0.0/lib/reasoners/fun_sat.ml	2017-11-14 18:01:38.000000000 +0100
-+++ alt-ergo/lib/reasoners/fun_sat.ml	2018-05-24 16:10:10.418194590 +0200
-@@ -29,6 +29,7 @@
- open Options
+diff -r -u alt-ergo-2.3.3/lib/reasoners/fun_sat.ml alt-ergo/lib/reasoners/fun_sat.ml
+--- alt-ergo-2.3.3/lib/reasoners/fun_sat.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/lib/reasoners/fun_sat.ml	2021-02-04 08:04:16.651812960 +0100
+@@ -850,8 +850,7 @@
+       if steps_bound () <> -1
+       && Int64.compare !steps (Int64.of_int (steps_bound ())) > 0 then
+         begin
+-          printf "Steps limit reached: %Ld@." !steps;
+-          exit 1
++          raise Errors.StepsLimitReached
+         end;
+       { env with tbox = tbox; unit_tbox = utbox; inst = inst }
+ 
+diff -r -u alt-ergo-2.3.3/lib/reasoners/satml.ml alt-ergo/lib/reasoners/satml.ml
+--- alt-ergo-2.3.3/lib/reasoners/satml.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/lib/reasoners/satml.ml	2021-02-03 20:47:18.466852486 +0100
+@@ -780,8 +780,7 @@
+         if steps_bound () <> -1
+         && Int64.compare !steps (Int64.of_int (steps_bound ())) > 0 then
+           begin
+-            printf "Steps limit reached: %Ld@." !steps;
+-            exit 1
++            raise Errors.StepsLimitReached
+           end;
+         env.unit_tenv <- t;
+         C_none
+@@ -850,8 +849,7 @@
+           if steps_bound () <> -1
+           && Int64.compare !steps (Int64.of_int (steps_bound ())) > 0 then
+             begin
+-              printf "Steps limit reached: %Ld@." !steps;
+-              exit 1
++              raise Errors.StepsLimitReached
+             end;
+           env.tenv <- t;
+           do_case_split env Util.AfterTheoryAssume
+diff -r -u alt-ergo-2.3.3/lib/structures/errors.ml alt-ergo/lib/structures/errors.ml
+--- alt-ergo-2.3.3/lib/structures/errors.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/lib/structures/errors.ml	2021-02-03 20:40:55.202689887 +0100
+@@ -28,6 +28,8 @@
+ 
  open Format
  
 +exception StepsLimitReached
- 
- module Th = Theory.Main
- open Sig
-@@ -691,8 +692,7 @@
-     if steps_bound () <> -1
-       && Int64.compare !steps (Int64.of_int (steps_bound ())) > 0 then
-       begin
--	printf "Steps limit reached: %Ld@." !steps;
--	exit 1
-+        raise StepsLimitReached
-       end;
-     { env with tbox = tbox; unit_tbox = utbox; inst = inst }
- 
-diff -r -u alt-ergo-2.0.0/lib/reasoners/fun_sat.mli alt-ergo/lib/reasoners/fun_sat.mli
---- alt-ergo-2.0.0/lib/reasoners/fun_sat.mli	2017-11-14 18:01:38.000000000 +0100
-+++ alt-ergo/lib/reasoners/fun_sat.mli	2018-05-24 16:10:45.622082786 +0200
-@@ -27,3 +27,5 @@
++
+ type error =
+   | BitvExtract of int*int
+   | BitvExtractRange of int*int
+diff -r -u alt-ergo-2.3.3/lib/structures/errors.mli alt-ergo/lib/structures/errors.mli
+--- alt-ergo-2.3.3/lib/structures/errors.mli	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/lib/structures/errors.mli	2021-02-03 20:41:04.670694850 +0100
+@@ -26,6 +26,8 @@
+ (*                                                                            *)
  (******************************************************************************)
  
- include Sat_solver_sig.S
-+
 +exception StepsLimitReached
-diff -r -u alt-ergo-2.0.0/lib/util/numbers.ml alt-ergo/lib/util/numbers.ml
---- alt-ergo-2.0.0/lib/util/numbers.ml	2017-11-14 18:01:38.000000000 +0100
-+++ alt-ergo/lib/util/numbers.ml	2018-05-24 16:12:31.849745671 +0200
++
+ type error =
+   | BitvExtract of int*int
+   | BitvExtractRange of int*int
+diff -r -u alt-ergo-2.3.3/lib/structures/profiling.ml alt-ergo/lib/structures/profiling.ml
+--- alt-ergo-2.3.3/lib/structures/profiling.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/lib/structures/profiling.ml	2021-02-04 08:04:56.195796125 +0100
+@@ -83,6 +83,8 @@
+   }
+ 
+ let set_sigprof () =
++()
++(*
+   let tm =
+     let v = Options.profiling_period () in
+     if (Stdlib.compare v 0.) = 1 then v else -. v
+@@ -90,6 +92,7 @@
+   ignore
+     (Unix.setitimer Unix.ITIMER_PROF
+        { Unix.it_value = tm; Unix.it_interval = 0. })
++*)
+ 
+ let init () =
+   state.decisions := 0;
+diff -r -u alt-ergo-2.3.3/lib/util/config.ml alt-ergo/lib/util/config.ml
+--- alt-ergo-2.3.3/lib/util/config.ml	2021-02-04 08:10:48.087636935 +0100
++++ alt-ergo/lib/util/config.ml	2021-02-03 16:11:06.112770857 +0100
+@@ -0,0 +1,5 @@
++let libdir = ""
++let pluginsdir = ""
++let preludesdir = ""
++let datadir = ""
++let mandir = ""
+diff -r -u alt-ergo-2.3.3/lib/util/myDynlink.ml alt-ergo/lib/util/myDynlink.ml
+--- alt-ergo-2.3.3/lib/util/myDynlink.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/lib/util/myDynlink.ml	2021-02-03 17:21:24.168796159 +0100
+@@ -28,4 +28,8 @@
+ 
+ end
+ 
++(*
+ include Dynlink
++*)
++
++include DummyDL
+diff -r -u alt-ergo-2.3.3/lib/util/myUnix.ml alt-ergo/lib/util/myUnix.ml
+--- alt-ergo-2.3.3/lib/util/myUnix.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/lib/util/myUnix.ml	2021-02-03 17:27:48.105065186 +0100
+@@ -11,6 +11,7 @@
+ 
+ (** TODO: use the newly available Sys.backend_type to simplify things ? *)
+ 
++(*
+ module Default_Unix = struct
+ 
+   open Unix
+@@ -37,20 +38,19 @@
+ end
+ 
+ include Default_Unix
++*)
+ 
+-(* !! This commented code is used when compiling to javascript !!
+    module JavaScript_Unix = struct
+ 
+    let cur_time () =
+-    let today = jsnew Js.date_now () in
+-    let t = Js.to_float (today##getTime()) in
++    let today = new%js Js_of_ocaml.Js.date_now in
++    let t = Js_of_ocaml.Js.to_float (today##getTime) in
+     t /. 1000.
+ 
+-   let set_timeout _ = ()
++   let set_timeout ~is_gui _ = ()
+ 
+-   let unset_timeout () = ()
++   let unset_timeout ~is_gui = ()
+ 
+    end
+ 
+    include JavaScript_Unix
+-*)
+diff -r -u alt-ergo-2.3.3/lib/util/numbers.ml alt-ergo/lib/util/numbers.ml
+--- alt-ergo-2.3.3/lib/util/numbers.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/lib/util/numbers.ml	2021-02-03 15:46:11.353288338 +0100
 @@ -26,7 +26,7 @@
  (*                                                                            *)
  (******************************************************************************)
  
 -module MyZarith = ZarithNumbers
 +module MyZarith = NumsNumbers
+ [@@@ocaml.warning "-60"]
  module MyNums = NumsNumbers
  
- module Z = MyZarith.Z
+Seulement dans alt-ergo: Makefile.config
+diff -r -u alt-ergo-2.3.3/parsers/myZip.ml alt-ergo/parsers/myZip.ml
+--- alt-ergo-2.3.3/parsers/myZip.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/parsers/myZip.ml	2021-02-03 17:21:36.932810413 +0100
+@@ -12,6 +12,7 @@
+ (** A wrapper of the Zip module of CamlZip: we use Zip except when we want to
+     generate the.js file for try-Alt-Ergo **)
+ 
++(*
+ module ZipWrapper = struct
+   include Zip
+   let filename e = e.Zip.filename
+@@ -19,8 +20,8 @@
+ end
+ 
+ include ZipWrapper
++*)
+ 
+-(* !! This commented code is used when compiling to javascript !!
+    module DummyZip = struct
+    type entry = unit
+    type in_file = unit
+@@ -36,4 +37,3 @@
+    end
+ 
+    include DummyZip
+-*)
+diff -r -u alt-ergo-2.3.3/parsers/parsers_loader.ml alt-ergo/parsers/parsers_loader.ml
+--- alt-ergo-2.3.3/parsers/parsers_loader.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/parsers/parsers_loader.ml	2021-02-03 17:19:17.828627883 +0100
+@@ -8,7 +8,6 @@
+ (*                                                                            *)
+ (******************************************************************************)
+ 
+-open AltErgoLib
+ open Options
+ open Format
+ 
+diff -r -u alt-ergo-2.3.3/parsers/parsers.ml alt-ergo/parsers/parsers.ml
+--- alt-ergo-2.3.3/parsers/parsers.ml	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/parsers/parsers.ml	2021-02-03 16:24:44.546348838 +0100
+@@ -26,7 +26,6 @@
+ (*                                                                            *)
+ (******************************************************************************)
+ 
+-open AltErgoLib
+ open Options
+ open Format
+ 
+diff -r -u alt-ergo-2.3.3/parsers/parsers.mli alt-ergo/parsers/parsers.mli
+--- alt-ergo-2.3.3/parsers/parsers.mli	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/parsers/parsers.mli	2021-02-03 16:24:48.590340768 +0100
+@@ -26,8 +26,6 @@
+ (*                                                                            *)
+ (******************************************************************************)
+ 
+-open AltErgoLib
+-
+ module type PARSER_INTERFACE = sig
+   val file : Lexing.lexbuf -> Parsed.file
+   val expr : Lexing.lexbuf -> Parsed.lexpr
+diff -r -u alt-ergo-2.3.3/parsers/why_lexer.mll alt-ergo/parsers/why_lexer.mll
+--- alt-ergo-2.3.3/parsers/why_lexer.mll	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/parsers/why_lexer.mll	2021-02-03 16:25:07.826302670 +0100
+@@ -28,7 +28,6 @@
+ 
+ {
+   [@@@ocaml.warning "-33"]
+-  open AltErgoLib
+   open Options
+ 
+   open Lexing
+diff -r -u alt-ergo-2.3.3/parsers/why_parser.mly alt-ergo/parsers/why_parser.mly
+--- alt-ergo-2.3.3/parsers/why_parser.mly	2020-08-19 11:32:19.000000000 +0200
++++ alt-ergo/parsers/why_parser.mly	2021-02-03 16:22:55.302575286 +0100
+@@ -28,7 +28,6 @@
+ 
+ %{
+   [@@@ocaml.warning "-33"]
+-  open AltErgoLib
+   open Options
+   open Parsed_interface
+ %}
+@@ -73,13 +72,13 @@
+ 
+ /* Entry points */
+ 
+-%type <AltErgoLib.Parsed.lexpr list * bool> trigger_parser
++%type <Parsed.lexpr list * bool> trigger_parser
+ %start trigger_parser
+ 
+-%type <AltErgoLib.Parsed.lexpr> lexpr_parser
++%type <Parsed.lexpr> lexpr_parser
+ %start lexpr_parser
+ 
+-%type <AltErgoLib.Parsed.file> file_parser
++%type <Parsed.file> file_parser
+ %start file_parser
+ %%
+ 
diff --git a/src/trywhy3/alt_ergo_worker.ml b/src/trywhy3/alt_ergo_worker.ml
index f7427d295ac7a5326c3ffc9d1db3576c3a1547f5..cf5df2914039f2503bf466c92911baf1404a9449 100644
--- a/src/trywhy3/alt_ergo_worker.ml
+++ b/src/trywhy3/alt_ergo_worker.ml
@@ -13,44 +13,31 @@ open Format
 open Worker_proto
 
 module Worker = Js_of_ocaml.Worker
-module SAT = (val (Sat_solver.get_current ()) : Sat_solver_sig.S)
+module SATCont = (val (Sat_solver.get_current ()) : Sat_solver_sig.SatContainer)
+module SAT = SATCont.Make(Theory.Main_Default)
 module FE = Frontend.Make (SAT)
 
-let print_status fmt _d status steps =
-  match status with
-  | FE.Unsat _dep ->
-    fprintf fmt "Proved (%Ld steps)" steps
-  | FE.Inconsistent -> ()
-    (* fprintf fmt "Inconsistent assumption" *)
-  | FE.Unknown _t | FE.Sat _t ->
-      fprintf fmt "Unknown (%Ld steps)@." steps
-
-
 let report_status report _d status _steps =
   match status with
-  | FE.Unsat _dep -> report Valid
-  | FE.Inconsistent -> ()
-  | FE.Unknown _t | FE.Sat _t -> report (Unknown "unknown")
+  | FE.Unsat _ -> report Valid
+  | _ -> report (Unknown "unknown")
 
 let run_alt_ergo_on_task text =
   let lb = Lexing.from_string text in
 (* from Alt-Ergo, src/main/frontend.ml *)
   let a = Why_parser.file_parser Why_lexer.parse_token lb in
   Parsing.clear_parser ();
-  let ltd, _typ_env = Typechecker.file false Typechecker.empty_env a in
-  match Typechecker.split_goals ltd with
-  | [d] ->
-    let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
-    SAT.reset_refs ();
-    let stat = ref (Invalid "no answer from Alt-Ergo") in
-    let f s = stat := s in
-    begin
+  let ltd, _typ_env = Typechecker.type_file a in
+  match Typechecker.split_goals_and_cnf ltd with
+  | [pb, _] -> begin
+      let ctxt = FE.init_all_used_context () in
       try
-        let _x = Queue.fold (FE.process_decl (report_status f))
-          (SAT.empty (), true, Explanation.empty) d
-        in
-        !stat
-      with Fun_sat.StepsLimitReached -> Unknown "steps limit reached"
+        let _, consistent, _ =
+          List.fold_left (fun acc d ->
+              FE.process_decl (fun _ _ -> ()) ctxt acc d
+            ) (SAT.empty (), true, Explanation.empty) pb in
+        if consistent then (Unknown "unknown") else Valid
+      with Errors.StepsLimitReached -> Unknown "steps limit reached"
     end
   | _ -> Invalid "zero or more than 1 goal to solve"