diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 1edfedcef..b9bd5fc46 100644 --- 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 index ca695b352..37204e15b 100644 --- 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)