diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index dbda63748..e0e936fdb 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -664,7 +664,7 @@ let case_split env uf ~for_model =
 let optimizing_objective _env _uf _o = None
 
 let query _env uf (ra, _, ex, _) =
-  if Options.get_disable_adts () then None
+  if Options.get_disable_adts () then Th_util.Unknown
   else
     let domains = Uf.GlobalDomains.find (module Domains) (Uf.domains uf) in
     try
@@ -672,16 +672,17 @@ let query _env uf (ra, _, ex, _) =
       | Xliteral.Builtin(true, Sy.IsConstr c, [r]) ->
         let rr, _ = Uf.find_r uf r in
         ignore (assume_is_constr ~ex rr c domains);
-        None
+        Unknown
 
       | Xliteral.Builtin(false, Sy.IsConstr c, [r]) ->
         let rr, _ = Uf.find_r uf r in
         ignore (assume_not_is_constr ~ex rr c domains);
-        None
+        Unknown
 
       | _ ->
-        None
+        Unknown
     with
-    | Domain.Inconsistent ex -> Some (ex, Uf.cl_extract uf)
+    | Domain.Inconsistent ex ->
+      Entailed { ex; classes = Uf.cl_extract uf }
 
 (* ################################################################ *)
diff --git a/src/lib/reasoners/arrays_rel.ml b/src/lib/reasoners/arrays_rel.ml
index 1042bf697..32dcbc4cd 100644
--- a/src/lib/reasoners/arrays_rel.ml
+++ b/src/lib/reasoners/arrays_rel.ml
@@ -237,23 +237,23 @@ module type UF = module type of Uf
    (respectively [q]) is already true, we do not add the consequence. *)
 let update_env (module Uf : UF) uf dep env acc gi si p p_ded n n_ded =
   match Uf.are_equal uf ~added_terms:true gi si, Uf.are_distinct uf gi si with
-  | Some (idep, _) , None ->
+  | Entailed { ex = idep; _ }, Unknown ->
     let conseq = LRmap.add n n_ded dep env.conseq in
     {env with conseq = conseq},
     Conseq.add (p_ded, Ex.union dep idep) acc
 
-  | None, Some (idep, _) ->
+  | Unknown, Entailed { ex = idep; _ } ->
     let conseq = LRmap.add p p_ded dep env.conseq in
     {env with conseq = conseq},
     Conseq.add (n_ded, Ex.union dep idep) acc
 
-  | None, None ->
+  | Unknown, Unknown ->
     let sp = LRset.add p env.split in
     let conseq = LRmap.add p p_ded dep env.conseq in
     let conseq = LRmap.add n n_ded dep conseq in
     { env with split = sp; conseq = conseq }, acc
 
-  | Some _,  Some _ ->
+  | Entailed _,  Entailed _ ->
     (* This case cannot occur because we cannot have `gi = si` and
        `gi <> si` at the same time. *)
     assert false
@@ -290,8 +290,8 @@ let get_of_set (module Uf : UF) uf gtype (env, acc) =
            let n_ded = E.mk_eq ~iff:false get get_stab in
            let dep =
              match Uf.are_equal uf ~added_terms:true gtab set with
-             | Some (dep, _) -> dep
-             | None -> assert false
+             | Entailed { ex; _ } -> ex
+             | Unknown -> assert false
            in
            let env =
              {env with new_terms =
@@ -362,8 +362,8 @@ let get_and_set (module Uf : UF) uf gtype (env, acc) =
            let n_ded = E.mk_eq ~iff:false gt_of_st get_stab in
            let dep =
              match Uf.are_equal uf ~added_terms:true gtab stab with
-             | Some (dep, _) -> dep
-             | None -> assert false
+             | Entailed { ex; _ } -> ex
+             | Unknown -> assert false
            in
            let env =
              {env with
@@ -471,7 +471,7 @@ let assume env uf la =
   in
   env, Uf.domains uf, { Sig_rel.assume = l; remove = [] }
 
-let query _ _ _ = None
+let query _ _ _ = Th_util.Unknown
 let add env uf _ _ = env, Uf.domains uf, []
 
 let new_terms env = env.new_terms
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index 0a1eec3ad..262172289 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -2210,7 +2210,7 @@ let assume env uf la =
   Uf.GlobalDomains.add (module Interval_domains) int_domain ds,
   result
 
-let query _ _ _ = None
+let query _ _ _ = Th_util.Unknown
 
 let case_split env uf ~for_model =
   if not for_model && Stdlib.(env.size_splits >= Options.get_max_split ()) then
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index 5d9f56787..a0e0655a8 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -264,9 +264,10 @@ module Main : S = struct
 
   let explain_equality env ex t1 t2 =
     if E.equal t1 t2 then ex
-    else match Uf.are_equal env.uf t1 t2 ~added_terms:true with
-      | Some (dep, _) -> Ex.union ex dep
-      | None -> raise Exit
+    else
+      match Uf.are_equal env.uf t1 t2 ~added_terms:true with
+      | Entailed { ex = ex'; _ } -> Ex.union ex ex'
+      | Unknown -> raise Exit
 
   let equal_only_by_congruence env (facts: r Sig_rel.facts) t1 t2 =
     if not (E.equal t1 t2) then
@@ -353,11 +354,11 @@ module Main : S = struct
                let ty_y = Expr.type_info y in
                if Ty.equal ty_x ty_y then
                  begin match Uf.are_distinct env.uf t1 t2 with
-                   | Some (ex_r, _) ->
+                   | Entailed { ex = ex_r; _ } ->
                      let a = E.mk_distinct ~iff:false [x; y] in
                      Debug.contra_congruence a ex_r;
                      Q.push (Literal.LTerm a, ex_r, Th_util.Other) facts.diseqs
-                   | None -> assert false
+                   | Unknown -> assert false
                  end
              | _ -> ()
           ) (Uf.class_of env.uf bol)
@@ -739,7 +740,8 @@ module Main : S = struct
     {env with relation = Rel.assume_th_elt env.relation th_elt dep}
 
   let are_equal env t1 t2 ~init_terms =
-    if E.equal t1 t2 then Some (Ex.empty, [])
+    if E.equal t1 t2 then
+      Th_util.Entailed { ex = Ex.empty; classes = [] }
     else
     if init_terms then
       let facts = empty_facts() in
@@ -748,7 +750,8 @@ module Main : S = struct
       try
         let env, _ = assume_literals env [] facts in
         Uf.are_equal env.uf t1 t2 ~added_terms:true
-      with Ex.Inconsistent (ex,cl) -> Some (ex, cl)
+      with Ex.Inconsistent (ex, classes) ->
+        Entailed { ex; classes }
     else
       Uf.are_equal env.uf t1 t2 ~added_terms:false
 
diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
index 88c845c54..62d3dc9ab 100644
--- a/src/lib/reasoners/fun_sat.ml
+++ b/src/lib/reasoners/fun_sat.ml
@@ -678,8 +678,10 @@ module Make (Th : Theory.S) = struct
     with Not_found ->
       assert (E.is_ground a);
       match Th.query a env.tbox with
-      | None -> tmp_cache := ME.add a None !tmp_cache; None
-      | Some (ex,_) as y ->
+      | Unknown ->
+        tmp_cache := ME.add a Th_util.Unknown !tmp_cache;
+        Unknown
+      | Entailed { ex; _ } as y ->
         if Options.get_tableaux_cdcl () then
           cdcl_learn_clause true env ex (ff.E.ff);
         learn_clause env ff ex;
@@ -689,43 +691,50 @@ module Make (Th : Theory.S) = struct
     match E.form_view ff.E.ff with
     | E.Literal a ->
       let ans = query_of tcp_cache tmp_cache ff a env in
-      if ans != None then
-        begin
-          Options.tool_req 2 "TR-Sat-Bcp-Elim-2";
-          if Options.get_profiling() then Profiling.elim false;
-        end;
+      let () =
+        match ans with
+        | Entailed _ ->
+          begin
+            Options.tool_req 2 "TR-Sat-Bcp-Elim-2";
+            if Options.get_profiling() then Profiling.elim false;
+          end
+        | Unknown -> ()
+      in
       ans
     | E.Unit _ | E.Clause _ | E.Lemma _ | E.Skolem _
-    | E.Let _ | E.Iff _ | E.Xor _ -> None
+    | E.Let _ | E.Iff _ | E.Xor _ -> Unknown
 
   let red tcp_cache tmp_cache ff env tcp =
     let nf = E.neg ff.E.ff in
     let nff = {ff with E.ff = nf} in
     try
       let _, ex = ME.find nf !(env.unit_facts_cache) in
-      Some(ex, []), true
+      Th_util.Entailed { ex; classes = [] }, true
     with Not_found ->
     try
       let _, ex, _, _ = ME.find nf env.gamma in
-      let r = Some (ex, Th.cl_extract env.tbox) in
       Options.tool_req 2 "TR-Sat-Bcp-Red-1";
-      r, true
+      Entailed { ex; classes = Th.cl_extract env.tbox }, true
     with Not_found ->
-      if not tcp then None, false
+      if not tcp then Unknown, false
       else match E.form_view nf with
         | E.Literal a ->
           let ans = query_of tcp_cache tmp_cache nff a env in
-          if ans != None then Options.tool_req 2 "TR-Sat-Bcp-Red-2";
+          let () =
+            match ans with
+            | Entailed _ -> Options.tool_req 2 "TR-Sat-Bcp-Red-2"
+            | _ -> ()
+          in
           ans, false
         | E.Unit _ | E.Clause _ | E.Lemma _ | E.Skolem _
-        | E.Let _ | E.Iff _ | E.Xor _ -> None, false
+        | E.Let _ | E.Iff _ | E.Xor _ -> Unknown, false
 
   let red tcp_cache tmp_cache ff env tcp =
     match red tcp_cache tmp_cache ff env tcp with
-    | (Some _, _)  as ans -> ans
-    | None, b ->
+    | Entailed _, _  as ans -> ans
+    | Unknown, b ->
       if not (Options.get_tableaux_cdcl ()) then
-        None, b
+        Th_util.Unknown, b
       else
         match CDCL.is_true !(env.cdcl) (E.neg ff.E.ff) with
         | Some (ex, _lvl) ->
@@ -733,9 +742,9 @@ module Make (Th : Theory.S) = struct
           if Options.(get_debug_sat () && get_verbose ()) then
             Printer.print_dbg "red thanks to satML";
           assert (cdcl_known_decisions ex env);
-          Some(ex, []), true
+          Entailed { ex; classes = [] }, true
         | None ->
-          None, b
+          Unknown, b
 
   let add_dep f dep =
     match E.form_view f with
@@ -790,16 +799,16 @@ module Make (Th : Theory.S) = struct
             let u =
               match th_elim tcp_cache tmp_cache gf1 env,
                     th_elim tcp_cache tmp_cache gf2 env with
-              | None, None -> raise Exit
-              | Some _, _ | _, Some _ when gf1.E.theory_elim -> u
+              | Unknown, Unknown -> raise Exit
+              | Entailed _, _ | _, Entailed _ when gf1.E.theory_elim -> u
 
-              | Some _, Some _ ->
+              | Entailed _, Entailed _ ->
                 u (* eliminate if both are true ? why ? *)
               (*(gf1, Ex.union d d1) :: (gf2, Ex.union d d2) :: u*)
 
-              | Some (d1, _), _ -> (gf1, Ex.union d d1) :: u
+              | Entailed { ex = d1; _ }, _ -> (gf1, Ex.union d d1) :: u
 
-              | _, Some (d2, _) -> (gf2, Ex.union d d2) :: u
+              | _, Entailed { ex = d2; _ } -> (gf2, Ex.union d d2) :: u
             in
             cl, u
           with Exit ->
@@ -809,27 +818,28 @@ module Make (Th : Theory.S) = struct
                 red tcp_cache tmp_cache gf1 env tcp,
                 red tcp_cache tmp_cache gf2 env tcp
               with
-              | (Some (d1, c1), b1) , (Some (d2, c2), b2) ->
+              | (Entailed { ex = d1; classes = c1 }, b1),
+                (Entailed { ex = d2; classes = c2 }, b2) ->
                 if Options.get_profiling() then Profiling.bcp_conflict b1 b2;
                 let expl = Ex.union (Ex.union d d1) d2 in
                 let c = List.rev_append c1 c2 in
                 raise (Ex.Inconsistent (expl, c))
 
-              | (Some(d1, _), b) , (None, _) ->
+              | (Entailed { ex = d1; _ }, b), (Unknown, _) ->
                 if Options.get_profiling() then Profiling.red b;
                 let gf2 =
                   {gf2 with E.nb_reductions = gf2.E.nb_reductions + 1} in
                 let gf2 = update_distances env gf2 f1 in
                 cl, (gf2,Ex.union d d1) :: u
 
-              | (None, _) , (Some(d2, _),b) ->
+              | (Unknown, _) , (Entailed { ex = d2; _ }, b) ->
                 if Options.get_profiling() then Profiling.red b;
                 let gf1 =
                   {gf1 with E.nb_reductions = gf1.E.nb_reductions + 1} in
                 let gf1 = update_distances env gf1 f2 in
                 cl, (gf1,Ex.union d d2) :: u
 
-              | (None, _) , (None, _) -> fd::cl , u
+              | (Unknown, _) , (Unknown, _) -> fd::cl , u
             end
       ) acc delta
 
@@ -1185,9 +1195,9 @@ module Make (Th : Theory.S) = struct
            | E.Literal a ->
              begin
                match query_of tcp_cache tmp_cache {gf with E.ff=f} a env with
-               | Some (ex, _) ->
+               | Entailed { ex; _ } ->
                  Ex.union dep ex, ({gf with E.ff=f}, ex) :: acc
-               | None ->
+               | Unknown ->
                  Printer.print_err
                    "Bad inst! Hyp %a is not true!" E.print f;
                  assert false
diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index 5e037b74a..1b4eeb7f9 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -794,9 +794,10 @@ let cannot_be_equal_to_zero env p ip =
   try
     let z = alien_of (P.create [] Q.zero (P.type_info p)) in
     match X.solve (alien_of p) z with
-    | [] -> None (* p is equal to zero *)
+    | [] -> Th_util.Unknown (* p is equal to zero *)
     | _ -> I.doesnt_contain_0 ip
-  with Util.Unsolvable -> Some (Explanation.empty, env.classes)
+  with Util.Unsolvable ->
+    Entailed { ex = Explanation.empty; classes = env.classes }
 
 
 let rec init_monomes_of_poly are_eq env p use_p expl =
@@ -867,22 +868,23 @@ and update_monome are_eq expl use_x env x =
             let env, ib =
               init_alien are_eq expl pb npb use_x env in
             let ib = I.add_explanation ib eb in (* take repr into account*)
-            let ia, ib = match cannot_be_equal_to_zero env pb ib with
-              | Some (ex, _) when Q.equal ca cb
-                               && P.compare pa' pb' = 0 ->
+            let ia, ib =
+              match cannot_be_equal_to_zero env pb ib with
+              | Entailed { ex; _ }
+                when Q.equal ca cb && P.compare pa' pb' = 0 ->
                 let expl = Explanation.union ex expl in
                 I.point da ty expl, I.point db ty expl
-              | Some (ex, _) ->
+              | Entailed { ex; _ } ->
                 begin
                   match are_eq a b with
-                  | Some (ex_eq, _) ->
+                  | Th_util.Entailed { ex = ex_eq; _ } ->
                     let expl = Explanation.union ex expl in
                     let expl = Explanation.union ex_eq expl in
                     I.point Q.one ty expl,
                     I.point Q.one ty expl
-                  | None -> ia, ib
+                  | Unknown -> ia, ib
                 end
-              | None -> ia, ib
+              | Unknown -> ia, ib
             in
             I.div ia ib, env
           | _ -> I.undefined ty, env
@@ -1743,8 +1745,9 @@ let assume ~query env uf la =
 let query env uf a_ex =
   try
     ignore(assume ~query:true env uf [a_ex]);
-    None
-  with Ex.Inconsistent (expl, classes) -> Some (expl, classes)
+    Th_util.Unknown
+  with Ex.Inconsistent (ex, classes) ->
+    Entailed { ex; classes }
 
 let case_split_polynomes env =
   let o = MP.fold
@@ -1824,7 +1827,10 @@ let default_case_split env uf ~for_model =
 
 let add =
   let are_eq t1 t2 =
-    if E.equal t1 t2 then Some (Explanation.empty, []) else None
+    if E.equal t1 t2 then
+      Th_util.Entailed { ex = Explanation.empty; classes = [] }
+    else
+      Unknown
   in
   fun env new_uf r t ->
     Debug.env env;
diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml
index 61e2a96a1..141518459 100644
--- a/src/lib/reasoners/intervals.ml
+++ b/src/lib/reasoners/intervals.ml
@@ -757,17 +757,16 @@ module Legacy = struct
     | _ -> Fmt.invalid_arg "point: %a (as %a)" Q.pp_print v Ty.print ty
 
   let doesnt_contain_0 u =
-    Option.map (fun ex -> (ex, [])) @@
     match u with
     | Real u -> Real.(
         match intersect u (of_interval @@ Interval.singleton Q.zero) with
-        | NonEmpty _ -> None
-        | Empty ex -> Some ex
+        | NonEmpty _ -> Th_util.Unknown
+        | Empty ex -> Entailed { ex; classes = [] }
       )
     | Int u -> Int.(
         match intersect u (of_interval @@ Interval.singleton Z.zero) with
-        | NonEmpty _ -> None
-        | Empty ex -> Some ex
+        | NonEmpty _ -> Unknown
+        | Empty ex -> Entailed { ex; classes = [] }
       )
 
   let is_strict_smaller u1 u2 =
diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml
index ccbf93145..4e9aee4b0 100644
--- a/src/lib/reasoners/ite_rel.ml
+++ b/src/lib/reasoners/ite_rel.ml
@@ -216,7 +216,7 @@ let case_split _env _uf ~for_model:_ = []
 
 let optimizing_objective _env _uf _o = None
 
-let query _ _ _ = None
+let query _ _ _ = Th_util.Unknown
 
 let new_terms _ = E.Set.empty
 let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []
diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml
index 55e2bf782..fba07b40e 100644
--- a/src/lib/reasoners/matching.ml
+++ b/src/lib/reasoners/matching.ml
@@ -297,7 +297,11 @@ module Make (X : Arg) : S with type theory = X.t = struct
       max_t_depth =
     if SubstE.mem f s_t then
       let s = SubstE.find f s_t in
-      if are_equal_full tbox t s == None then raise Echec;
+      let () =
+        match are_equal_full tbox t s with
+        | Th_util.Unknown -> raise Echec
+        | Th_util.Entailed _ -> ()
+      in
       sg
     else
       let t =
@@ -394,8 +398,13 @@ module Make (X : Arg) : S with type theory = X.t = struct
       try
         let s_ty = Ty.matching s_ty ty_pat (E.type_info t) in
         let gsb = { sg with sty = s_ty } in
-        if E.is_ground pat &&
-           are_equal_light tbox pat t != None then
+        let ignore_match =
+          E.is_ground pat &&
+          (match are_equal_light tbox pat t with
+           | Entailed _ -> true
+           | _ -> false)
+        in
+        if ignore_match then
           [gsb]
         else
           let cl = if mconf.Util.no_ematching then E.Set.singleton t
diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml
index 78eb6699a..862bf71bb 100644
--- a/src/lib/reasoners/relation.ml
+++ b/src/lib/reasoners/relation.ml
@@ -104,8 +104,8 @@ let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a
     k =
   match Timers.with_timer R.timer Timers.F_query
     @@ fun () -> R.query env uf a with
-  | Some r -> Some r
-  | None -> k ()
+  | Th_util.Entailed _ as r -> r
+  | Th_util.Unknown -> k ()
 
 let query env uf a =
   Options.exec_thread_yield ();
@@ -113,7 +113,7 @@ let query env uf a =
   try_query (module Rel2) env.r2 uf a @@ fun () ->
   try_query (module Rel3) env.r3 uf a @@ fun () ->
   try_query (module Rel4) env.r4 uf a @@ fun () ->
-  try_query (module Rel5) env.r5 uf a @@ fun () -> None
+  try_query (module Rel5) env.r5 uf a @@ fun () -> Th_util.Unknown
 
 let case_split env uf ~for_model =
   Options.exec_thread_yield ();
diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
index 0d9906910..fc0bbbd09 100644
--- a/src/lib/reasoners/satml.ml
+++ b/src/lib/reasoners/satml.ml
@@ -1136,11 +1136,11 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
             | LSem _ -> false
             | LTerm lit ->
               match Th.query lit env.tenv with
-              | Some _ ->
+              | Entailed _ ->
                 a.timp <- 1;
                 a.neg.timp <- 1;
                 true
-              | None ->
+              | Unknown ->
                 false
           else
             ta.timp = 1
@@ -1751,15 +1751,15 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       | LSem _ -> None
       | LTerm lit ->
         match Th.query lit tenv with
-        | Some (d,_) ->
+        | Entailed { ex; _ } ->
           a.timp <- 1;
-          Some (clause_of_dep d a)
-        | None  ->
+          Some (clause_of_dep ex a)
+        | Unknown ->
           match Th.query (E.neg lit) tenv with
-          | Some (d,_) ->
+          | Entailed { ex; _ } ->
             a.neg.timp <- 1;
-            Some (clause_of_dep d a.Atom.neg)
-          | None -> None
+            Some (clause_of_dep ex a.Atom.neg)
+          | Unknown -> None
 
   let make_decision env atom =
     match th_entailed env.tenv atom with
diff --git a/src/lib/reasoners/th_util.ml b/src/lib/reasoners/th_util.ml
index 318c81609..d62f8cfe5 100644
--- a/src/lib/reasoners/th_util.ml
+++ b/src/lib/reasoners/th_util.ml
@@ -25,7 +25,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type answer = (Explanation.t * Expr.Set.t list) option
+type answer =
+  | Entailed of { ex : Explanation.t; classes : Expr.Set.t list }
+  | Unknown
 
 type theory =
   | Th_arith
diff --git a/src/lib/reasoners/th_util.mli b/src/lib/reasoners/th_util.mli
index 523c8367e..c78c6f21b 100644
--- a/src/lib/reasoners/th_util.mli
+++ b/src/lib/reasoners/th_util.mli
@@ -25,7 +25,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type answer = (Explanation.t * Expr.Set.t list) option
+(** Type of answers returned by theory queries for ground literals. *)
+type answer =
+  | Entailed of { ex : Explanation.t; classes : Expr.Set.t list }
+  (** The literal is entailed by the theory environment:
+      - The explanation [ex] justifies why the literal holds in the
+        environment.
+      - [classes] is used for debugging purpose only. *)
+
+  | Unknown
+  (** One does not encounter a contradiction when assuming the negation of the
+      literal. It does not imply that the literal is false in the environment,
+      as the decision procedures might be incomplete. *)
 
 type theory =
   | Th_arith
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 9a6905d3f..95609678f 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -781,7 +781,7 @@ module Main_Default : S = struct
       { t with gamma = gamma }
     in
     fun a t ->
-      if Options.get_no_tcp () then None
+      if Options.get_no_tcp () then Th_util.Unknown
       else begin
         if Options.get_profiling() then Profiling.query();
         Options.exec_thread_yield ();
@@ -800,7 +800,7 @@ module Main_Default : S = struct
           | E.Distinct _ | E.Eql _ ->
             (* we only assume toplevel distinct with more that one arg.
                not interesting to do a query in this case ?? or query ? *)
-            None
+            Th_util.Unknown
 
           | E.Pred (t1,b) ->
             let t = add_and_process_conseqs a t in
@@ -812,8 +812,8 @@ module Main_Default : S = struct
             let na = E.neg a in
             let t = add_and_process_conseqs na t in
             CC_X.query t.gamma na
-        with Ex.Inconsistent (d, classes) ->
-          Some (d, classes)
+        with Ex.Inconsistent (ex, classes) ->
+          Th_util.Entailed { ex; classes }
       end
 
   let add_term_in_gm gm t =
@@ -921,7 +921,7 @@ module Main_Empty : S = struct
     in
     {assumed_set}, E.Set.empty, 0
 
-  let query _ _ = None
+  let query _ _ = Th_util.Unknown
 
   let cl_extract _ = []
   let extract_ground_terms _ = Expr.Set.empty
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 0d94864e6..4d9cbc439 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -923,7 +923,8 @@ let distinct env rl dep =
   env
 
 let are_equal env t1 t2 ~added_terms =
-  if E.equal t1 t2 then Some (Ex.empty, cl_extract env)
+  if E.equal t1 t2 then
+    Th_util.Entailed { ex = Ex.empty; classes = cl_extract env }
   else
     let lookup =
       if added_terms then Env.lookup_by_t
@@ -931,8 +932,10 @@ let are_equal env t1 t2 ~added_terms =
     in
     let r1, ex_r1 = lookup t1 env in
     let r2, ex_r2 = lookup t2 env in
-    if X.equal r1 r2 then Some (Ex.union ex_r1 ex_r2, cl_extract env)
-    else None
+    if X.equal r1 r2 then
+      Th_util.Entailed { ex = Ex.union ex_r1 ex_r2; classes = cl_extract env }
+    else
+      Th_util.Unknown
 
 let are_distinct env t1 t2 =
   Debug.are_distinct t1 t2;
@@ -940,8 +943,9 @@ let are_distinct env t1 t2 =
   let r2, ex_r2 = Env.lookup_by_t t2 env in
   try
     ignore (union env r1 r2 (Ex.union ex_r1 ex_r2));
-    None
-  with Ex.Inconsistent (ex, classes) -> Some (ex, classes)
+    Th_util.Unknown
+  with Ex.Inconsistent (ex, classes) ->
+    Th_util.Entailed { ex; classes }
 
 let already_distinct env lr =
   let d = LX.mk_distinct false lr in