fix(BV): Do not call [X.make] on non-subterm, reloaded (#969)

This is a follow-up to #954

Somehow convinced myself that the cases where we perform simplifications
were fine because we would only be simplifying into a subterm, but that
is obviously not the case due to negation. Let's just do the safe thing
and always return the original term with the appropriate equalities.

All of this code should be removed in favor of doing these computations
in the relations instead anyways, which would make sure we always treat
[bv2nat] in the same way for literals and after substitution (see also
#824 )

src/lib/reasoners/bitv.ml

@@ -1324,24 +1324,26 @@ module Shostak(X : ALIEN) = struct
       let maybe_negate t =
         if negated then E.Ints.(~$$Z.(~$1 lsl sz - ~$1) - t) else t
       in
-      begin match E.term_view t with
-        | { f = Op Int2BV _; _ } ->
-          (* bv2nat will simplify: we must call [X.make] again *)
-          E.BV.bv2nat t |> maybe_negate |> X.make
-        | { ty = Tbitv n; _ } ->
-          assert (n = sz);
-          if negated then
-            (* if we are negated, we will simplify *)
-            E.BV.bv2nat t |> maybe_negate |> X.make
-          else
-            (* bv2nat will *not* simplify: become uninterpreted with interval
-               information *)
-            let t = E.BV.bv2nat t |> maybe_negate in
-            X.term_embed t,
-            [ E.Ints.(~$0 <= t) ; E.Ints.(t < ~$$Z.(~$1 lsl n)) ]
-        | { ty; _ } ->
-          Util.internal_error "expected bitv, got %a" Ty.print ty
-      end
+      let t', ctx =
+        begin match E.term_view t with
+          | { f = Op Int2BV _; _ } ->
+            (* bv2nat will simplify: we must call [X.make] again *)
+            E.BV.bv2nat t |> maybe_negate, []
+          | { ty = Tbitv n; _ } ->
+            assert (n = sz);
+            if negated then
+              (* if we are negated, we will simplify *)
+              E.BV.bv2nat t |> maybe_negate, []
+            else
+              (* bv2nat will *not* simplify: become uninterpreted with interval
+                 information *)
+              let t = E.BV.bv2nat t |> maybe_negate in
+              t, [ E.Ints.(~$0 <= t) ; E.Ints.(t < ~$$Z.(~$1 lsl n)) ]
+          | { ty; _ } ->
+            Util.internal_error "expected bitv, got %a" Ty.print ty
+        end
+      in
+      X.term_embed ot, E.Core.eq ot t' :: ctx
     | _ ->
       (* Note: we can't just call [X.make] on the result of [abstract_to_nat]
          because [X.make] should only be called on subterms. If we do it, it

tests/bitv/testfile-bitv025.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/bitv/testfile-bitv025.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 32))
+(declare-fun t () (_ BitVec 32))
+(assert (= (bvshl s (bvnot (bvmul s t))) (_ bv0 32)))
+(check-sat)