Address review

bclement-ocp · Aug 19, 2024 · 3a80705 · 3a80705
1 parent 47dd42e
commit 3a80705
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
@@ -3098,7 +3098,8 @@ module BV = struct
 
   (* Other operations *)
   let repeat i t =
-    assert (i >= 1);
+    if i < 1 then
+      Fmt.invalid_arg "repeat: count must be positive (got %d)" i;
     mk_term (Op (Repeat i)) [t] (Tbitv (i * size t))
 
   let zero_extend i t =

diff --git a/tests/bitv/testfile-sign-extend-003.smt2 b/tests/bitv/testfile-sign-extend-003.smt2
@@ -1,4 +1,4 @@
 (set-logic ALL)
 (declare-const x (_ BitVec 4))
-(assert (distinct ((_ extract 3 2) ((_ sign_extend 4) x)) ((_ extract 3 2) x)))
+(assert (distinct ((_ extract 5 4) ((_ sign_extend 4) x)) ((_ repeat 2) ((_ extract 3 3) x))))
 (check-sat)