Backporting 2.5.1 (#821)

* Do not discard `bvnot` applied to uninterpreted terms

In PR #745 we correctly handled the case where uninterpreted terms
appear deep within a bit-vector terms, but we accidentally missed the
case where the whole bit-vector is itself an uninterpreted term, leading
to unsoundness (see the attached test).

This patch fixes the code to properly deal with `bvnot` applied to an
uninterpreted term.

* Update the changes log for v2.5.1

* Review changes

---------

Co-authored-by: Basile Clément <bc@ocamlpro.com>

CHANGES.md

@@ -1,5 +1,10 @@
 ## unreleased
 
+## v2.5.1
+
+### Bug fixes
+* fix a critical soundness bug with bvnot primitive (#819)
+
 ## v2.5.0
 
 ### New features

src/lib/reasoners/bitv.ml

@@ -250,15 +250,13 @@ module Shostak(X : ALIEN) = struct
     let other ~neg t sz ctx =
       let r, ctx' = X.make t in
       let ctx = List.rev_append ctx' ctx in
-      match X.extract r with
-      | Some bv ->
-        if neg then
-          try negate_abstract bv, ctx with
-          | Failure _ ->
-            [ { bv = Other (X.term_embed (E.BV.bvnot t)); sz } ], ctx
-        else
-          bv, ctx
-      | None -> [ { bv = Other r; sz } ], ctx
+      let bv = embed r in
+      if neg then
+        try negate_abstract bv, ctx with
+        | Failure _ ->
+          [ { bv = Other (X.term_embed (E.BV.bvnot t)); sz } ], ctx
+      else
+        bv, ctx
 
     let extract_st i j ({ bv; sz } as st) =
       match bv with

tests/bitv/testfile-bvnot-term.dolmen.expected

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

tests/bitv/testfile-bvnot-term.dolmen.smt2

@@ -0,0 +1,7 @@
+(set-logic BV)
+
+(declare-const x (_ BitVec 4))
+(declare-const y (_ BitVec 4))
+(assert (= x (bvnot y)))
+(assert (distinct y x))
+(check-sat)

tests/dune.inc

@@ -117948,6 +117948,28 @@
       (diff
         testfile-bvnot.dolmen.expected
         testfile-bvnot.dolmen_dolmen.output)))
+  (rule
+   (target testfile-bvnot-term.dolmen_dolmen.output)
+   (deps (:input testfile-bvnot-term.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff
+        testfile-bvnot-term.dolmen.expected
+        testfile-bvnot-term.dolmen_dolmen.output)))
   (rule
    (target testfile-bitv023_ci_cdcl_no_minimal_bj.output)
    (deps (:input testfile-bitv023.ae))