From 0c7b4480248b6599d79bc4f128d91bb755c16b22 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Wed, 28 Aug 2024 13:45:09 +0200
Subject: [PATCH] Debug message instead of error

---
 src/lib/reasoners/bitv_rel.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index 2d280f2fb..bf1df3e07 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -2279,11 +2279,11 @@ let case_split env uf ~for_model =
         let bit_interval = Intervals.Int.extract int ~ofs:bitidx ~len:1 in
         match Intervals.Int.value_opt bit_interval with
         | Some (v, _) ->
-          if Options.get_enable_assertions () then
-            Util.internal_error
-              "High bit allowed by bitlists, but not intervals."
-          else
-            const 1 v, 1
+          Log.debug (fun m ->
+              m "@[%a@]" Fmt.words
+                "High bit forced by intervals; cross-domain propagation bug?"
+            );
+          const 1 v, 1
         | None -> const 1 Z.zero, 2
       in
       if Options.get_debug_bitv () then