From 44787785513d14445478255613a030d233ba696b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Mon, 11 Dec 2023 15:13:57 +0100 Subject: [PATCH] fix(BV): Treat bvand, bvor, bvxor as interpreted 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