Add high-level binding for string length

Signed-off-by: Yage Hu <me@huyage.dev>
prove-rs · Oct 18, 2024 · 397b32b · 397b32b
1 parent 7b00b99
commit 397b32b
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/z3/src/ast.rs b/z3/src/ast.rs
@@ -1177,6 +1177,11 @@ impl<'ctx> String<'ctx> {
         concat(Z3_mk_seq_concat, String<'ctx>);
     }
 
+    unop! {
+        /// Gets the length of `Self`.
+        length(Z3_mk_seq_length, Int<'ctx>);
+    }
+
     binop! {
         /// Checks whether `Self` contains a substring
         contains(Z3_mk_seq_contains, Bool<'ctx>);