diff --git a/Blaster/Optimize/Opaque.lean b/Blaster/Optimize/Opaque.lean
index 8a1023b..cbea509 100644
--- a/Blaster/Optimize/Opaque.lean
+++ b/Blaster/Optimize/Opaque.lean
@@ -63,7 +63,8 @@ def opaqueFuns : NameHashSet :=
     -- String operators
     ``String.append,
     ``String.replace,
-    ``String.length
+    ``String.length,
+    ``String.take
   ]
 
 /-- list of types for which:
diff --git a/Blaster/Optimize/Rewriting/OptimizeString.lean b/Blaster/Optimize/Rewriting/OptimizeString.lean
index f8f1770..48ec885 100644
--- a/Blaster/Optimize/Rewriting/OptimizeString.lean
+++ b/Blaster/Optimize/Rewriting/OptimizeString.lean
@@ -128,6 +128,30 @@ def optimizeStrReplace (f : Expr) (args: Array Expr) : TranslateEnvT Expr := do
       Expr.lit (Literal.strVal s3) => mkStrLitExpr (String.replace s1 s2 s3)
     | _, _, _  => return none
 
+/-- Apply the following simplification/normalization rules on `String.take` :
+     - String.take S n ==> "String.take" S n
+   Assume that f = Expr.const ``String.take.
+   An error is triggered when args.size ≠ 2 (i.e., only fully applied `String.take` expected at this stage)
+-/
+def optimizeStrTake (f : Expr) (args: Array Expr) : TranslateEnvT Expr := do
+ if args.size != 2 then throwEnvError "optimizeStrTake: exactly two arguments expected"
+ -- args[0] string operand
+ -- args[1] nat operand (number of characters to take)
+ let op1 := args[0]!
+ let op2 := args[1]!
+ if let some r ← cstStrTake? op1 op2 then return r
+ return (mkApp2 f op1 op2)
+
+ where
+   /-- Given `op1` and `op2` corresponding to the operands for `String.take`
+       return `some ("String.take" S n)` when `op1 := S` (a string literal) and `op2 := n` (a nat value).
+       Otherwise `none`.
+   -/
+   cstStrTake? (op1 : Expr) (op2 : Expr) : TranslateEnvT (Option Expr) :=
+    match op1, isNatValue? op2 with
+    | Expr.lit (Literal.strVal s), some n => mkStrLitExpr (s.take n)
+    | _, _ => return none
+
 
 /-- Apply simplification/normalization rules on `String` operators. -/
 def optimizeString? (f : Expr) (args : Array Expr) : TranslateEnvT (Option Expr) := do
@@ -137,6 +161,7 @@ def optimizeString? (f : Expr) (args : Array Expr) : TranslateEnvT (Option Expr)
  | ``String.append => optimizeStrAppend f args
  | ``String.length => optimizeStrLength f args
  | ``String.replace => optimizeStrReplace f args
+ | ``String.take => optimizeStrTake f args
  | _ => return none
 
 end Blaster.Optimize
diff --git a/Blaster/Smt/Env.lean b/Blaster/Smt/Env.lean
index 000bc26..7f18ff8 100644
--- a/Blaster/Smt/Env.lean
+++ b/Blaster/Smt/Env.lean
@@ -171,7 +171,7 @@ partial def getErrorMsg (h : IO.FS.Handle) : IO String := h.getLine
 -/
 partial def getOutputEval (h : IO.FS.Handle) : IO String := do
   let line ← h.getLine
-  if line.get! 0 != '(' then return line
+  if String.Pos.Raw.get! line 0 != '(' then return line
   getIndValue line (tallyParenthesis line 0)
 
  where
diff --git a/Blaster/Smt/Syntax.lean b/Blaster/Smt/Syntax.lean
index 6306e05..8a6a943 100644
--- a/Blaster/Smt/Syntax.lean
+++ b/Blaster/Smt/Syntax.lean
@@ -148,7 +148,7 @@ opaque validSimpleChars : String :=
       -- characters in `validSimpleChars` that -- does not start with a digit.
       if str.isEmpty then "||"
       else
-        let fstChar := str.get 0
+        let fstChar := String.Pos.Raw.get str 0
         if (fstChar ≥ '0' && fstChar ≤ '9') || str.any (λ c => !(validSimpleChars.contains c))
         then s!"|{str}|" -- create quoted smt symbol
         else str
diff --git a/lean-toolchain b/lean-toolchain
index c00a535..e5ab73a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.25.0