fix(CP): Make sure domains do not overflow the default domain

src/lib/reasoners/domains.ml

@@ -530,8 +530,12 @@ struct
             D.intersect (D.unknown (X.type_info repr)) @@
             D.add_explanation ~ex (Entry.domain entry)
 
-        let set_domain { entry ; explanation = ex ; _ } d =
-          Entry.set_domain entry (D.add_explanation ~ex d)
+        let set_domain { repr ; entry ; explanation = ex } d =
+          if Explanation.is_empty ex then Entry.set_domain entry d
+          else
+            Entry.set_domain entry @@
+            D.intersect (D.unknown (X.type_info repr)) @@
+            D.add_explanation ~ex d
       end
 
       type nonrec t =

src/lib/reasoners/domains_intf.ml

@@ -140,9 +140,11 @@ module type EphemeralDomainMap = sig
     (** [set_domain e d] sets the domain of entry [e] to [d]. This overwrites
         any pre-existing domain associated with [e].
 
-        {b Note}: if you need to tighten an existing domain, this must be done
-        explicitely by accessing the current domain through [domain] before
-        calling [set_domain].  See {!MakEntryNotation}. *)
+        {b Note}: the caller is responsible for ensuring that the domain is
+        a subset of the possible domains for the entry (e.g. due to type
+        constraints). The recommended way to do so is by first intersecting
+        with the existing [domain]. See also the {!EntryNotation} functor
+        which does this for you. *)
   end
 
   val entry : t -> key -> Entry.t

tests/bitv/testfile-bvshl-001.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/bitv/testfile-bvshl-001.smt2

@@ -0,0 +1,9 @@
+(set-logic ALL)
+(declare-fun T4_306 () (_ BitVec 32))
+(declare-fun T1_306 () (_ BitVec 8))
+(declare-fun T1_307 () (_ BitVec 8))
+(declare-fun T1_308 () (_ BitVec 8))
+(declare-fun T1_309 () (_ BitVec 8))
+(assert (and (xor (or (bvule (_ bv0 32) T4_306) (= T4_306 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_309) (_ bv8 32)) ((_ zero_extend 24) T1_308)) (_ bv8 32)) ((_ zero_extend 24) T1_307)) T4_306) ((_ zero_extend 24) T1_306)))) (=> (bvult (_ bv8 32) T4_306) (and true (= (_ bv0 32) (bvor (bvshl ((_ zero_extend 24) T1_306) (_ bv8 32)) ((_ zero_extend 24) T1_306))) (bvult (_ bv0 32) T4_306) (bvule (_ bv0 32) (_ bv8 32))))) (bvult (_ bv0 32) T4_306)))
+(check-sat)
+(exit)

tests/bitv/testfile-bvshl-002.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/bitv/testfile-bvshl-002.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-fun T1_7389 () (_ BitVec 8))
+(declare-fun T1_7390 () (_ BitVec 8))
+(assert (=> (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (xor (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (bvslt (bvsub (bvadd ((_ zero_extend 24) T1_7390) (bvshl ?v_0 (bvshl ?v_0 ?v_0))) (_ bv48 32)) (_ bv0 32)))) (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (bvslt (bvsub (bvadd ((_ zero_extend 24) T1_7390) (bvshl ?v_0 (bvshl ?v_0 ?v_0))) (_ bv48 32)) (_ bv0 32))))))) (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (xor (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (bvslt (bvsub (bvadd ((_ zero_extend 24) T1_7390) (bvshl ?v_0 (bvshl ?v_0 ?v_0))) (_ bv48 32)) (_ bv0 32)))) (let ((?v_0 (bvsub ((_ zero_extend 24) T1_7389) (_ bv48 32)))) (and true (bvslt (bvsub (bvadd ((_ zero_extend 24) T1_7390) (bvshl ?v_0 (bvshl ?v_0 ?v_0))) (_ bv48 32)) (_ bv0 32)))))))))
+(check-sat)
+(exit)