From f7ae6f78e2c6f28133464aa7e133c241b2276c89 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?=
 <129742207+bclement-ocp@users.noreply.github.com>
Date: Mon, 11 Dec 2023 16:32:15 +0000
Subject: [PATCH] fix(BV): Treat bvand, bvor, bvxor as interpreted (#1007)

While they are not interpreted in the Shostak sense, they should still
be treated as interpreted symbols of the BV theory (in the same way as,
for instance, `**` is treated as an interpreted symbol of the Arith
theory even though it is actually not interepreted in the CC(X) sense).
---
 src/lib/reasoners/bitv.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 6aa75af21..73079f2b8 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -345,7 +345,9 @@ module Shostak(X : ALIEN) = struct
 
   let is_mine_symb sy _ =
     match sy with
-    | Sy.Bitv _ | Sy.Op (Concat | Extract _ | BV2Nat | BVnot)  -> true
+    | Sy.Bitv _
+    | Op (Concat | Extract _ | BV2Nat | BVnot | BVand | BVor | BVxor)
+      -> true
     | _ -> false
 
   let embed r =
@@ -398,7 +400,12 @@ module Shostak(X : ALIEN) = struct
     let (and+) = (and*)
 
     let other ~neg t _sz ctx =
-      let r, ctx' = X.make t in
+      let r, ctx' =
+        match E.term_view t with
+        | { f = Op (BVand | BVor | BVxor); _ } ->
+          X.term_embed t, []
+        | _ -> X.make t
+      in
       let ctx = List.rev_append ctx' ctx in
       let bv = embed r in
       if neg then negate_abstract bv, ctx else bv, ctx