diff --git a/dune-project b/dune-project
index 3f65bce47..5660ff498 100644
--- a/dune-project
+++ b/dune-project
@@ -61,5 +61,5 @@
   (crowbar :with-test)
   (graphics :dev)
   (tiny_httpd :dev)
-  encoding
+  (encoding (>= 0.0.3))
   xmlm))
diff --git a/owi.opam b/owi.opam
index 927f5e70d..d091c3edb 100644
--- a/owi.opam
+++ b/owi.opam
@@ -30,7 +30,7 @@ depends: [
   "crowbar" {with-test}
   "graphics" {dev}
   "tiny_httpd" {dev}
-  "encoding"
+  "encoding" {>= "0.0.3"}
   "xmlm"
 ]
 build: [
diff --git a/src/choice_monad.ml b/src/choice_monad.ml
index be5434c6e..4d6c5d677 100644
--- a/src/choice_monad.ml
+++ b/src/choice_monad.ml
@@ -112,28 +112,25 @@ struct
     let pc = Thread.pc state in
     let sym_int = Expr.simplify sym_int in
     let orig_pc = pc in
-    let pc, sym = fix_symbol sym_int pc in
+    let pc, symbol = fix_symbol sym_int pc in
     match sym_int.e with
     | Val (Num (I32 i)) -> M.return (i, state)
     | _ ->
       let module Solver = (val solver_module) in
       let rec find_values values =
-        let additionnal = M.to_list @@ M.map (not_value sym) values in
+        let additionnal = M.to_list @@ M.map (not_value symbol) values in
         if not (Solver.check solver (additionnal @ pc)) then M.empty
         else begin
-          let model = Solver.model ~symbols:[ sym ] solver in
+          let model = Solver.model ~symbols:[ symbol ] solver in
           match model with
           | None -> assert false (* ? *)
           | Some model -> (
             Format.pp_std "Model:@.%a@." Model.pp model;
-            let v = Model.evaluate model sym in
+            let v = Model.evaluate model symbol in
             match v with
             | None -> assert false (* ? *)
-            | Some (Num (I32 i) as v) -> begin
-              let cond =
-                Expr.(
-                  Relop (Eq, mk_symbol sym, Val v @: Ty_bitv S32) @: Ty_bitv S32 )
-              in
+            | Some (Num (I32 i)) -> begin
+              let cond = Expr.Bitv.I32.(Expr.mk_symbol symbol = v i) in
               let pc = cond :: pc in
               let case = (i, { state with pc }) in
               M.cons case (find_values (M.cons i values))
@@ -570,8 +567,8 @@ module MT = struct
 
   let spawn_producer _i global =
     let module Mapping = Z3_mappings.Fresh.Make () in
-    let module Batch = Batch.Make (Mapping) in
-    let solver = Batch.create () in
+    let module Batch = Solver.Batch (Mapping) in
+    let solver = Batch.create ~logic:QF_BVFP () in
     let solver : Thread.solver = S ((module Batch), solver) in
     let st = { solver; next = None; global } in
     let rec producer (H (thread, t, cont)) =
diff --git a/src/symbolic_value.ml b/src/symbolic_value.ml
index c4aad6e6c..bd2a94fcb 100644
--- a/src/symbolic_value.ml
+++ b/src/symbolic_value.ml
@@ -287,7 +287,7 @@ module S = struct
 
     let wrap_i64 x = cvtop ty WrapI64 x
 
-    let extend_s _ = assert false
+    let extend_s n x = cvtop ty (ExtS n) x
   end
 
   module I64 = struct
@@ -385,7 +385,7 @@ module S = struct
 
     let reinterpret_f64 x = cvtop ty Reinterpret_float x
 
-    let extend_s _ = assert false
+    let extend_s n x = cvtop ty (ExtS n) x
 
     let extend_i32_s x = cvtop ty (ExtS 32) x
 
diff --git a/src/thread.ml b/src/thread.ml
index 98e041b22..c26c5c5f5 100644
--- a/src/thread.ml
+++ b/src/thread.ml
@@ -2,7 +2,7 @@
 (* Copyright © 2021 Léo Andrès *)
 (* Copyright © 2021 Pierre Chambart *)
 
-module Solver = Encoding.Batch.Make (Encoding.Z3_mappings)
+module Solver = Encoding.Solver.Batch (Encoding.Z3_mappings)
 
 type 'a solver_module = (module Encoding.Solver_intf.S with type t = 'a)
 
@@ -29,7 +29,7 @@ let globals t = t.globals
 let solver_mod : Solver.t solver_module = (module Solver)
 
 let create () =
-  let solver = S (solver_mod, Solver.create ()) in
+  let solver = S (solver_mod, Solver.create ~logic:QF_BVFP ()) in
   { solver
   ; pc = []
   ; memories = Symbolic_memory.init ()