fix(BV): Properly set fully interpreted operators

Alt-Ergo calls "fully interpreted" symbols that are fully internalized
in semantic values and do not need to be taken into consideration by the
CC(X) algorithm (see function `congruents` in `ccx.ml`).

(Note that `fully_interpreted` is only called for the Shostak theory
associated with the symbol according to `is_min_symb`.)

The BV theory incorrectly states that all its symbols are fully
interpreted, including `bv2nat`, `int2bv`, etc.; however, only `concat`,
`extract` and `bv2nat` are fully interpreted. This means that Alt-Ergo
never performs congruence closure for these functions, leading to missed
reasoning opportunities.

src/lib/reasoners/bitv.ml

@@ -1464,7 +1464,10 @@ module Shostak(X : ALIEN) = struct
       let compare = compare_mine
     end)
 *)
-  let fully_interpreted _ = true
+  let fully_interpreted sb =
+    match sb with
+    | Sy.Op (Concat | Extract _ | BVnot) -> true
+    | _ -> false
 
   let term_extract _ = None, false
 

src/lib/reasoners/sig.mli

@@ -92,6 +92,9 @@ module type SHOSTAK = sig
 
   val print : Format.formatter -> t -> unit
 
+  (** return true if the symbol is fully interpreted by the theory, i.e. it
+      is fully embedded into semantic values and does not need term-level
+      congruence *)
   val fully_interpreted : Symbols.t -> bool
 
   val abstract_selectors : t -> (r * r) list -> r * (r * r) list