diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
index d4d9b12ac..9df7efe6a 100644
--- a/src/lib/reasoners/fun_sat.ml
+++ b/src/lib/reasoners/fun_sat.ml
@@ -1847,7 +1847,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let get_unknown_reason env = env.unknown_reason
 
-  let get_value _env _t = None
+  let get_value env t =
+    match E.type_info t with
+    | Ty.Tbool ->
+      begin
+        match ME.find_opt t env.gamma with
+        | None -> Some E.faux
+        | Some _ -> Some E.vrai
+      end
+    | _ -> None
 
   let reinit_ctx () =
     (* all_models_sat_env := None; *)
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 7e7c7b1db..832229ffd 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -1249,7 +1249,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let get_unknown_reason env = env.unknown_reason
 
-  let get_value _env _t = None
+  let get_value env t =
+    match E.type_info t with
+    | Ty.Tbool ->
+      begin
+        match ME.find_opt t env.gamma with
+        | None -> Some E.faux
+        | Some _ -> Some E.vrai
+      end
+    | _ -> None
 
   let reinit_ctx () =
     Steps.reinit_steps ();