diff --git a/src/lib/reasoners/domains.ml b/src/lib/reasoners/domains.ml
index f8b49076c..ee6edc0d7 100644
--- a/src/lib/reasoners/domains.ml
+++ b/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 =
diff --git a/tests/bitv/testfile-bvshl-001.expected b/tests/bitv/testfile-bvshl-001.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/bitv/testfile-bvshl-001.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/bitv/testfile-bvshl-001.smt2 b/tests/bitv/testfile-bvshl-001.smt2
new file mode 100644
index 000000000..159537e19
--- /dev/null
+++ b/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)
diff --git a/tests/bitv/testfile-bvshl-002.expected b/tests/bitv/testfile-bvshl-002.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/bitv/testfile-bvshl-002.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/bitv/testfile-bvshl-002.smt2 b/tests/bitv/testfile-bvshl-002.smt2
new file mode 100644
index 000000000..4d25fbb00
--- /dev/null
+++ b/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)