Preserve Subst literals

src/lib/reasoners/ccx.ml

@@ -447,8 +447,16 @@ module Main : S = struct
   let make_unique sa =
     let mp =
       List.fold_left
-        (fun mp ((ra, aopt ,_ ,_) as e) ->
-           LRE.add (LR.make ra, aopt) e mp
+        (fun mp ((ra, aopt ,_ , _) as e) ->
+           (* Make sure to prefer equalities of [Subst] origin because they are
+              used for partial computations (see {!Rel_utils}). In general, we
+              want to make sure that the relations see all the equalities from
+              representative changes in the union-find. *)
+           LRE.update (LR.make ra, aopt) (function
+               | Some ((_, _, _, Th_util.Subst) as e') -> Some e'
+               | _ -> Some e
+             ) mp
+
         ) LRE.empty sa
     in
     LRE.fold (fun _ e acc -> e::acc) mp []

src/lib/reasoners/rel_utils.ml

@@ -173,33 +173,12 @@ end = struct
               | None -> eqs) se eqs) sm eqs
 
   let update env uf r1 r2 orig eqs =
-    (* The `Subst` origin is used when `r1 -> r2` is added in the
-        union-find. The `CS _` and `NCS _` origins are used for case splits. In
-        both cases, we want to be propagating the constant.
-
-        Note that equalities of `Subst` origins are oriented: for `Subst`, `r2`
-        is the (new) normal form for `r1.
-
-        Usually, this would be true of case-split equalities as well (of the
-        form `r = v` where `v` is the chosen value), but this is not true for
-        the case splits that come from the arrays theory (in fact, the array
-        theory produces *dis*equality case splits, and the equality ends up in
-        the `NCS` instead), so we don't try to be smart and pay the (small)
-        performance cost.
-
-        `Other` cases should (I believe...) be subsumed by `Subst`. The original
-        code in the arithmetic theory that this is lifted from from was only
-        considering `Subst`, and was allowing possibly incorrect models.
-
-        Note that we need to handle `CS` and `NCS` here to produce correct
-        models, but also this can cause eager enumeration, so by excess of
-        caution we only use it when model generation has been requested. It is
-        unknown whether eager enumeration would be an actual problem in
-        practice. *)
+    (* The `Subst` origin is used when `r1 -> r2` is added in the union-find, so
+       we want to be propagating the constant on the RHS.
+
+       The other origins are subsumed. *)
     match orig with
     | Th_util.Subst when X.is_constant r2 -> update env uf r1 eqs
-    | CS _ | NCS _ when Options.get_interpretation () ->
-      update env uf r2 (update env uf r1 eqs)
     | _ -> eqs
 
 

tests/issues/883.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/issues/883.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-const x Int)
+(assert (= ((_ int2bv 2) x) #b11))
+(assert (<= x 0))
+(assert (<= 0 x))
+(check-sat)