diff --git a/Strata/DL/SMT/Encoder.lean b/Strata/DL/SMT/Encoder.lean
index 3db2c0634..296266f08 100644
--- a/Strata/DL/SMT/Encoder.lean
+++ b/Strata/DL/SMT/Encoder.lean
@@ -31,11 +31,11 @@ The encoding pipeline has two layers:
 2. **Encoder layer** (`EncoderM`): Sits on top of `SolverM` and manages
    A-normal form decomposition purely in the `Term` domain:
    - **Term → abbreviated Term cache** (`terms`): Maps each `Term` to its
-     abbreviated `Term.var` reference (e.g., a variable named `t0`, `t1`).
+     abbreviated `Term.var` reference (e.g., a variable named `$__t.0`, `$__t.1`).
      Large terms are broken into small `define-fun` definitions with short
      names, and the Solver handles all `Term → String` conversion.
    - **UF → abbreviated name cache** (`ufs`): Maps uninterpreted functions to
-     their abbreviated identifiers (e.g., `f0`, `f1`).
+     their abbreviated identifiers (e.g., `$__f.0`, `$__f.1`).
 
 The Encoder works purely with `Term` values. The `SolverM` layer handles all
 string conversion and caching when emitting commands.
@@ -72,10 +72,10 @@ open Solver
 public section
 
 structure EncoderState where
-  /-- Maps a `Term` to its abbreviated `Term` (a `Term.var` with name like `t0`).
+  /-- Maps a `Term` to its abbreviated `Term` (a `Term.var` with name like `$__t.0`).
       This is a cache after converting terms to A-Normal Form. -/
   terms : Std.HashMap Term Term
-  /-- Maps a `UF` to its abbreviated SMT identifier (e.g., `f0`, `f1`). -/
+  /-- Maps a `UF` to its abbreviated SMT identifier (e.g., `$__f.0`, `$__f.1`). -/
   ufs   : Std.HashMap UF String
 
 def EncoderState.init : EncoderState where
@@ -94,10 +94,23 @@ def smtReservedKeywords : List String :=
   -- SMT-LIB reserved words from the DDM parser
   let parserKeywords := _root_.Strata.reservedKeywords.map (·.2)
   -- Additional keywords not in the parser list
-  parserKeywords ++ ["select", "store", "and", "or", "not", "ite",
-   "true", "false", "Int", "Bool", "Real", "Array", "BitVec",
-   -- Theory function symbols that cvc5 disallows shadowing
-   "abs", "mod", "div", "to_real", "to_int", "is_int"]
+  parserKeywords ++
+   ["true", "false", "Int", "Bool", "Real", "Array", "BitVec",
+   -- Core theory symbols
+   "abs", "and", "distinct", "/", "=", ">", ">=", "ite", "=>",
+   "div", "is_int", "<", "<=", "-", "mod", "*", "not", "or", "+",
+   "to_int", "to_real", "xor",
+   -- String theory symbols
+   "str.at", "str.++", "str.contains", "str.from_code", "str.from_int",
+   "str.in_re", "str.indexof", "str.is_digit", "str.<=", "str.len",
+   "str.<", "str.prefixof", "str.replace", "str.substr", "str.suffixof",
+   "str.to_code", "str.to_int", "str.to_re",
+   -- Regex theory symbols
+   "re.*", "re.+", "re.opt", "re.++", "re.union", "re.inter", "re.diff",
+   "re.comp", "re.loop", "re.^", "re.range", "re.none", "re.all",
+   "re.allchar",
+   -- Array theory symbols
+   "select", "store"]
 
 /-- Generate a disambiguated name by appending @suffix -/
 def disambiguateName (baseName : String) (suffix : Nat) : String :=
@@ -133,8 +146,12 @@ def findUniqueName (baseName : String) (startSuffix : Nat) (isUsed : String →
     omega
   loop (if startSuffix == 1 then baseName else disambiguateName baseName (startSuffix - 1)) startSuffix limit
 
-def termId (n : Nat)                    : String := s!"t{n}"
-def ufId (n : Nat)                      : String := s!"f{n}"
+/-- The `$__` prefix is reserved for internal use and cannot appear in user
+    identifiers (see `Strata.DL.Lambda.LState.EvalConfig.varPrefix`).
+    The `.` after `t`/`f` prevents collision with Lambda-generated names
+    like `$__t0` (variable `t`, index 0). -/
+def termId (n : Nat)                    : String := s!"$__t.{n}"
+def ufId (n : Nat)                      : String := s!"$__f.{n}"
 
 def termNum : EncoderM Nat := do return (← get).terms.size
 def ufNum   : EncoderM Nat := do return (← get).ufs.size
@@ -325,11 +342,8 @@ Then you can run any `SolverM` action `act` with `act |>.run solver`, where
 `solver` is a `Solver` instance you can construct using functions in
 Solver.lean.
 
-Note that `encode` itself first resets the solver in order to define datatypes
-etc.
 -/
 def encode (ts : List Term) : SolverM Unit := do
-  Solver.reset
   Solver.setLogic "ALL"
   Solver.declareDatatype "Option" ["X"]
     [⟨"none", []⟩, ⟨"some", [("val", .constr "X" [])]⟩]
diff --git a/Strata/Languages/B3/Verifier/Program.lean b/Strata/Languages/B3/Verifier/Program.lean
index 037f21584..31f48f091 100644
--- a/Strata/Languages/B3/Verifier/Program.lean
+++ b/Strata/Languages/B3/Verifier/Program.lean
@@ -176,11 +176,8 @@ Workflow:
    - If failed, automatically diagnose to find root cause
 3. Report all results with diagnosis
 
-The solver is reset at the beginning to ensure clean state.
 -/
 def programToSMT (prog : Strata.B3AST.Program SourceRange) (solver : Solver) : IO (List ProcedureReport) := do
-  -- Reset solver to clean state
-  let _ ← (Solver.reset).run solver
   let state ← buildProgramState prog solver
   let mut reportsRev := []
 
diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean
index 1815abd8d..05217482f 100644
--- a/Strata/Languages/Core/SMTEncoder.lean
+++ b/Strata/Languages/Core/SMTEncoder.lean
@@ -43,6 +43,8 @@ structure SMT.Context where
   typeFactory : @Lambda.TypeFactory CoreLParams.IDMeta := #[]
   seenDatatypes : Std.HashSet String := {}
   datatypeFuns : Map String (Op.DatatypeFuncs × LConstr CoreLParams.IDMeta) := Map.empty
+  /-- Global counter for generating unique bound variable names across all terms. -/
+  bvCounter : Nat := 0
 deriving Repr, Inhabited
 
 def SMT.Context.default : SMT.Context := {}
@@ -269,12 +271,15 @@ partial def toSMTTerm (E : Env) (bvs : BoundVars) (e : LExpr CoreLParams.mono) (
   | .quant _ _ _ .none _ _ => .error f!"Cannot encode untyped quantifier {e}"
   | .quant _ qk name (.some ty) tr e =>
     let fvarNames := (e.collectFvarNames.map (·.name)).toArray
-    -- Generate base name and extract any existing suffix
+    -- Generate base name using global counter to ensure uniqueness across terms.
+    -- The `$__` prefix is reserved for internal use and cannot appear in user
+    -- identifiers (see `Strata.DL.Lambda.LState.EvalConfig.varPrefix`).
     let (baseName, startSuffix) :=
       if name.isEmpty then
-        (s!"$__bv{bvs.length}", 1)
+        (s!"$__bv{ctx.bvCounter}", 1)
       else
         Encoder.breakDisambiguatedName name
+    let ctx := { ctx with bvCounter := ctx.bvCounter + 1 }
     -- Check for clashes with existing bvars, fvars in ctx, and fvars in body
     let isUsed := fun candidate =>
       bvs.any (fun (n, _) => n == candidate) ||
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 9cb06f803..71273b053 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -47,7 +47,6 @@ def encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit)
     (md : Imperative.MetaData Core.Expression)
     (satisfiabilityCheck validityCheck : Bool) :
     SolverM (List String × EncoderState) := do
-  Solver.reset
   Solver.setLogic "ALL"
   prelude
   let _ ← ctx.sorts.mapM (fun s => Solver.declareSort s.name s.arity)
diff --git a/StrataTest/DL/Imperative/SMTEncoder.lean b/StrataTest/DL/Imperative/SMTEncoder.lean
index 601991e5e..968912c27 100644
--- a/StrataTest/DL/Imperative/SMTEncoder.lean
+++ b/StrataTest/DL/Imperative/SMTEncoder.lean
@@ -71,7 +71,6 @@ def ProofObligation.toSMTTerms (E : Env) (d : Imperative.ProofObligation Arith.P
   .ok (assumptions_terms ++ [obligation_term])
 
 def encodeArithToSMTTerms (ts : List Term) : SolverM (List String × EncoderState) := do
-  Solver.reset
   Solver.setLogic "ALL"
   let estate := EncoderState.init
   let (termEncs, estate) ← ts.mapM (Strata.SMT.Encoder.encodeTerm False) |>.run estate
diff --git a/StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean b/StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean
index 1f852aaf4..506bc6484 100644
--- a/StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean
+++ b/StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean
@@ -114,7 +114,7 @@ info: (declare-datatype TestOption (par (α) (
   (Some (TestOption..val |α|)))))
 ; x
 (declare-const x (TestOption Int))
-(define-fun t0 () (TestOption Int) x)
+(define-fun $__t.0 () (TestOption Int) x)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -128,7 +128,7 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; xs
 (declare-const xs (TestList Int))
-(define-fun t0 () (TestList Int) xs)
+(define-fun $__t.0 () (TestList Int) xs)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -142,7 +142,7 @@ info: (declare-datatype TestTree (par (α) (
   (Node (TestTree..value |α|) (TestTree..left (TestTree |α|)) (TestTree..right (TestTree |α|))))))
 ; tree
 (declare-const tree (TestTree Bool))
-(define-fun t0 () (TestTree Bool) tree)
+(define-fun $__t.0 () (TestTree Bool) tree)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -156,7 +156,7 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; intList
 (declare-const intList (TestList Int))
-(define-fun t0 () (TestList Int) intList)
+(define-fun $__t.0 () (TestList Int) intList)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -170,7 +170,7 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; boolList
 (declare-const boolList (TestList Bool))
-(define-fun t0 () (TestList Bool) boolList)
+(define-fun $__t.0 () (TestList Bool) boolList)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -184,7 +184,7 @@ info: (declare-datatype TestTree (par (α) (
   (Node (TestTree..value |α|) (TestTree..left (TestTree |α|)) (TestTree..right (TestTree |α|))))))
 ; intTree
 (declare-const intTree (TestTree Int))
-(define-fun t0 () (TestTree Int) intTree)
+(define-fun $__t.0 () (TestTree Int) intTree)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -201,7 +201,7 @@ info: (declare-datatype TestOption (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; listOfOption
 (declare-const listOfOption (TestList (TestOption Int)))
-(define-fun t0 () (TestList (TestOption Int)) listOfOption)
+(define-fun $__t.0 () (TestList (TestOption Int)) listOfOption)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -215,7 +215,7 @@ info: (declare-datatype TestOption (par (α) (
 info: (declare-datatype TestOption (par (α) (
   (None)
   (Some (TestOption..val |α|)))))
-(define-fun t0 () (TestOption Int) (as None (TestOption Int)))
+(define-fun $__t.0 () (TestOption Int) (as None (TestOption Int)))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -227,7 +227,7 @@ info: (declare-datatype TestOption (par (α) (
 info: (declare-datatype TestOption (par (α) (
   (None)
   (Some (TestOption..val |α|)))))
-(define-fun t0 () (TestOption Int) ((as Some (TestOption Int)) 42))
+(define-fun $__t.0 () (TestOption Int) ((as Some (TestOption Int)) 42))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -239,8 +239,8 @@ info: (declare-datatype TestOption (par (α) (
 info: (declare-datatype TestList (par (α) (
   (Nil)
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
-(define-fun t0 () (TestList Int) (as Nil (TestList Int)))
-(define-fun t1 () (TestList Int) ((as Cons (TestList Int)) 1 t0))
+(define-fun $__t.0 () (TestList Int) (as Nil (TestList Int)))
+(define-fun $__t.1 () (TestList Int) ((as Cons (TestList Int)) 1 $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -259,8 +259,8 @@ info: (declare-datatype TestOption (par (α) (
   (Some (TestOption..val |α|)))))
 ; x
 (declare-const x (TestOption Int))
-(define-fun t0 () (TestOption Int) x)
-(define-fun t1 () Bool (|is-None| t0))
+(define-fun $__t.0 () (TestOption Int) x)
+(define-fun $__t.1 () Bool (|is-None| $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -275,8 +275,8 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; xs
 (declare-const xs (TestList Int))
-(define-fun t0 () (TestList Int) xs)
-(define-fun t1 () Bool (|is-Cons| t0))
+(define-fun $__t.0 () (TestList Int) xs)
+(define-fun $__t.1 () Bool (|is-Cons| $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -293,8 +293,8 @@ info: (declare-datatype TestOption (par (α) (
   (Some (TestOption..val |α|)))))
 ; x
 (declare-const x (TestOption Int))
-(define-fun t0 () (TestOption Int) x)
-(define-fun t1 () Int (TestOption..val t0))
+(define-fun $__t.0 () (TestOption Int) x)
+(define-fun $__t.1 () Int (TestOption..val $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -309,8 +309,8 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; xs
 (declare-const xs (TestList Int))
-(define-fun t0 () (TestList Int) xs)
-(define-fun t1 () Int (TestList..head t0))
+(define-fun $__t.0 () (TestList Int) xs)
+(define-fun $__t.1 () Int (TestList..head $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -325,8 +325,8 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; xs
 (declare-const xs (TestList Int))
-(define-fun t0 () (TestList Int) xs)
-(define-fun t1 () (TestList Int) (TestList..tail t0))
+(define-fun $__t.0 () (TestList Int) xs)
+(define-fun $__t.1 () (TestList Int) (TestList..tail $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -391,7 +391,7 @@ info: (declare-datatype Root (
   (DiamondValue (Diamond..left Left) (Diamond..right Right))))
 ; diamondVar
 (declare-const diamondVar Diamond)
-(define-fun t0 () Diamond diamondVar)
+(define-fun $__t.0 () Diamond diamondVar)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -432,7 +432,7 @@ info: (declare-datatypes ((RoseTree 1) (Forest 1))
   (par (α) ((FNil) (FCons (Forest..hd (RoseTree |α|)) (Forest..tl (Forest |α|)))))))
 ; tree
 (declare-const tree (RoseTree Int))
-(define-fun t0 () (RoseTree Int) tree)
+(define-fun $__t.0 () (RoseTree Int) tree)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypeBlocks
@@ -450,7 +450,7 @@ info: (declare-datatype TestOption (par (α) (
   (par (α) ((FNil) (FCons (Forest..hd (RoseTree |α|)) (Forest..tl (Forest |α|)))))))
 ; optionTree
 (declare-const optionTree (TestOption (RoseTree Int)))
-(define-fun t0 () (TestOption (RoseTree Int)) optionTree)
+(define-fun $__t.0 () (TestOption (RoseTree Int)) optionTree)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypeBlocks
@@ -525,12 +525,12 @@ info: (declare-datatype IntList (
   (Cons (IntList..hd Int) (IntList..tl IntList))))
 ; listLen
 (declare-fun listLen (IntList) Int)
-(define-fun t0 () IntList (as Nil IntList))
-(define-fun t1 () Int (listLen t0))
-(define-fun t2 () Bool (= t1 0))
-(define-fun t3 () Bool (forall (($__bv0 Int) ($__bv1 IntList)) (! (= (listLen ((as Cons IntList) $__bv0 $__bv1)) (+ 1 (listLen $__bv1))) :pattern ((listLen ((as Cons IntList) $__bv0 $__bv1))))))
-(assert t2)
-(assert t3)
+(define-fun $__t.0 () IntList (as Nil IntList))
+(define-fun $__t.1 () Int (listLen $__t.0))
+(define-fun $__t.2 () Bool (= $__t.1 0))
+(define-fun $__t.3 () Bool (forall (($__bv0 Int) ($__bv1 IntList)) (! (= (listLen ((as Cons IntList) $__bv0 $__bv1)) (+ 1 (listLen $__bv1))) :pattern ((listLen ((as Cons IntList) $__bv0 $__bv1))))))
+(assert $__t.2)
+(assert $__t.3)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithRecFunc
diff --git a/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean b/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean
index b847fab4d..2241b9152 100644
--- a/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean
+++ b/StrataTest/Languages/Core/Tests/SMTEncoderTests.lean
@@ -13,7 +13,7 @@ namespace Core
 open Lambda
 open Strata.SMT
 
-/-- info: "(define-fun t0 () Bool (forall ((n Int)) (exists ((m Int)) (= n m))))\n" -/
+/-- info: "(define-fun $__t.0 () Bool (forall ((n Int)) (exists ((m Int)) (= n m))))\n" -/
 #guard_msgs in
 #eval toSMTTermString
   (.quant () .all "n" (.some .int) (LExpr.noTrigger ())
@@ -21,7 +21,7 @@ open Strata.SMT
    (.eq () (.bvar () 1) (.bvar () 0))))
 
 /--
-info: "; x\n(declare-const x Int)\n(define-fun t0 () Bool (exists ((i Int)) (= i x)))\n"
+info: "; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists ((i Int)) (= i x)))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -29,7 +29,7 @@ info: "; x\n(declare-const x Int)\n(define-fun t0 () Bool (exists ((i Int)) (= i
    (.eq () (.bvar () 0) (.fvar () "x" (.some .int))))
 
 /--
-info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun t0 () Bool (exists ((i Int)) (! (= i x) :pattern ((f i)))))\n"
+info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists ((i Int)) (! (= i x) :pattern ((f i)))))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -38,7 +38,7 @@ info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun t
 
 
 /--
-info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun t0 () Bool (exists ((i Int)) (! (= (f i) x) :pattern ((f i)))))\n"
+info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists ((i Int)) (! (= (f i) x) :pattern ((f i)))))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -52,7 +52,7 @@ info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun t
    (.eq () (.app () (.fvar () "f" (.some (.arrow .int .int))) (.bvar () 0)) (.fvar () "x" (.some .int))))
 
 /--
-info: "; f\n(declare-const f (arrow Int Int))\n; f\n(declare-fun f@1 (Int) Int)\n; x\n(declare-const x Int)\n(define-fun t0 () Bool (exists ((i Int)) (! (= (f@1 i) x) :pattern (f))))\n"
+info: "; f\n(declare-const f (arrow Int Int))\n; f\n(declare-fun f@1 (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists ((i Int)) (! (= (f@1 i) x) :pattern (f))))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -68,13 +68,13 @@ info: "; f\n(declare-const f (arrow Int Int))\n; f\n(declare-fun f@1 (Int) Int)\
    }})
 
 /--
-info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-fun t0 () Bool (forall ((m Int) (n Int)) (! (= (f n m) x) :pattern ((f n m)))))\n"
+info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall ((m Int) (n Int)) (! (= (f n m) x) :pattern ((f n m)))))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
    (.quant () .all "m" (.some .int) (.bvar () 0) (.quant () .all "n" (.some .int) (.app () (.app () (.op () "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar () 0)) (.bvar () 1))
    (.eq () (.app () (.app () (.op () "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar () 0)) (.bvar () 1)) (.fvar () "x" (.some .int)))))
-   (ctx := SMT.Context.mk #[] #[UF.mk "f" ((TermVar.mk "m" TermType.int) ::(TermVar.mk "n" TermType.int) :: []) TermType.int] #[] #[] [] #[] {} [])
+   (ctx := SMT.Context.mk #[] #[UF.mk "f" ((TermVar.mk "m" TermType.int) ::(TermVar.mk "n" TermType.int) :: []) TermType.int] #[] #[] [] #[] {} [] 0)
    (E := {Env.init with exprEnv := {
     Env.init.exprEnv with
       config := { Env.init.exprEnv.config with
@@ -86,13 +86,13 @@ info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-f
 
 
 /--
-info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-fun t0 () Bool (forall ((m Int) (n Int)) (= (f n m) x)))\n"
+info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall ((m Int) (n Int)) (= (f n m) x)))\n"
 -/
 #guard_msgs in -- No valid trigger
 #eval toSMTTermString
    (.quant () .all "m" (.some .int) (.bvar () 0) (.quant () .all "n" (.some .int) (.bvar () 0)
    (.eq () (.app () (.app () (.op () "f" (.some (.arrow .int (.arrow .int .int)))) (.bvar () 0)) (.bvar () 1)) (.fvar () "x" (.some .int)))))
-   (ctx := SMT.Context.mk #[] #[UF.mk "f" ((TermVar.mk "m" TermType.int) ::(TermVar.mk "n" TermType.int) :: []) TermType.int] #[] #[] [] #[] {} [])
+   (ctx := SMT.Context.mk #[] #[UF.mk "f" ((TermVar.mk "m" TermType.int) ::(TermVar.mk "n" TermType.int) :: []) TermType.int] #[] #[] [] #[] {} [] 0)
    (E := {Env.init with exprEnv := {
     Env.init.exprEnv with
       config := { Env.init.exprEnv.config with
@@ -108,7 +108,7 @@ section ArrayTheory
 
 -- Test map select with Array theory enabled
 /--
-info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int) m)\n; i\n(declare-const i Int)\n(define-fun t1 () Int i)\n(define-fun t2 () Int (select t0 t1))\n"
+info: "; m\n(declare-const m (Array Int Int))\n(define-fun $__t.0 () (Array Int Int) m)\n; i\n(declare-const i Int)\n(define-fun $__t.1 () Int i)\n(define-fun $__t.2 () Int (select $__t.0 $__t.1))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -125,7 +125,7 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int)
 
 -- Test map update with Array theory enabled
 /--
-info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int) m)\n; i\n(declare-const i Int)\n(define-fun t1 () Int i)\n; v\n(declare-const v Int)\n(define-fun t2 () Int v)\n(define-fun t3 () (Array Int Int) (store t0 t1 t2))\n"
+info: "; m\n(declare-const m (Array Int Int))\n(define-fun $__t.0 () (Array Int Int) m)\n; i\n(declare-const i Int)\n(define-fun $__t.1 () Int i)\n; v\n(declare-const v Int)\n(define-fun $__t.2 () Int v)\n(define-fun $__t.3 () (Array Int Int) (store $__t.0 $__t.1 $__t.2))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -143,7 +143,7 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int)
 
 -- Test nested map operations with Array theory
 /--
-info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int) m)\n; i\n(declare-const i Int)\n(define-fun t1 () Int i)\n; v\n(declare-const v Int)\n(define-fun t2 () Int v)\n(define-fun t3 () (Array Int Int) (store t0 t1 t2))\n; j\n(declare-const j Int)\n(define-fun t4 () Int j)\n(define-fun t5 () Int (select t3 t4))\n"
+info: "; m\n(declare-const m (Array Int Int))\n(define-fun $__t.0 () (Array Int Int) m)\n; i\n(declare-const i Int)\n(define-fun $__t.1 () Int i)\n; v\n(declare-const v Int)\n(define-fun $__t.2 () Int v)\n(define-fun $__t.3 () (Array Int Int) (store $__t.0 $__t.1 $__t.2))\n; j\n(declare-const j Int)\n(define-fun $__t.4 () Int j)\n(define-fun $__t.5 () Int (select $__t.3 $__t.4))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -163,7 +163,7 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int)
 
 -- Test that UF input types use Array when useArrayTheory=true (regression for Map/Array mismatch)
 /--
-info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int) m)\n; getFirst\n(declare-fun getFirst ((Array Int Int)) Int)\n(define-fun t1 () Int (getFirst t0))\n"
+info: "; m\n(declare-const m (Array Int Int))\n(define-fun $__t.0 () (Array Int Int) m)\n; getFirst\n(declare-fun getFirst ((Array Int Int)) Int)\n(define-fun $__t.1 () Int (getFirst $__t.0))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -181,7 +181,7 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int)
    }})
 
 -- Test empty string falls back to generated names
-/-- info: "(define-fun t0 () Bool (forall (($__bv0 Int)) (exists (($__bv1 Int)) (= $__bv0 $__bv1))))\n" -/
+/-- info: "(define-fun $__t.0 () Bool (forall (($__bv0 Int)) (exists (($__bv1 Int)) (= $__bv0 $__bv1))))\n" -/
 #guard_msgs in
 #eval toSMTTermString
   (.quant () .all "" (.some .int) (LExpr.noTrigger ())
@@ -190,7 +190,7 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int)
 
 -- Test name clash between two nested quantifiers with same name
 -- Expected: Inner x should be disambiguated to x@1
-/-- info: "(define-fun t0 () Bool (forall ((x Int)) (exists ((x@1 Int)) (= x x@1))))\n" -/
+/-- info: "(define-fun $__t.0 () Bool (forall ((x Int)) (exists ((x@1 Int)) (= x x@1))))\n" -/
 #guard_msgs in
 #eval toSMTTermString
   (.quant () .all "x" (.some .int) (LExpr.noTrigger ())
@@ -199,7 +199,7 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int)
 
 -- Test x, x, x@1 scenario: nested quantifiers both named "x", then bvar named "x@1"
 -- Expected: outer x stays x, inner x becomes x@1, bvar "x@1" becomes x@2
-/-- info: "(define-fun t0 () Bool (forall ((x Int) (x@1 Int) (x@2 Int)) (= x@2 x)))\n" -/
+/-- info: "(define-fun $__t.0 () Bool (forall ((x Int) (x@1 Int) (x@2 Int)) (= x@2 x)))\n" -/
 #guard_msgs in
 #eval toSMTTermString
   (.quant () .all "x" (.some .int) (LExpr.noTrigger ())
@@ -208,16 +208,36 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun t0 () (Array Int Int)
      (.eq () (.bvar () 0) (.bvar () 2)))))
 
 
-/-- info: "; x\n(declare-const x Int)\n(define-fun t0 () Bool (forall ((x@1 Int)) (= x@1 x)))\n" -/
+/-- info: "; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall ((x@1 Int)) (= x@1 x)))\n" -/
 #guard_msgs in
 #eval toSMTTermString
   (.quant () .all "x" (.some .int) (LExpr.noTrigger ())
    (.eq () (.bvar () 0) (.fvar () "x" (.some .int))))
 
+-- Test that bound variable names are globally unique across multiple terms.
+-- Two independent forall terms encoded via toSMTTerms should get distinct $__bv names.
+-- Before the fix, both terms would use $__bv0; now they get $__bv0 and $__bv1.
+#guard
+  match toSMTTerms Env.init [
+    -- Term 1: ∀ x:Int. x = x
+    (.quant () .all "" (.some .int) (LExpr.noTrigger ())
+     (.eq () (.bvar () 0) (.bvar () 0))),
+    -- Term 2: ∀ y:Bool. y
+    (.quant () .all "" (.some .bool) (LExpr.noTrigger ())
+     (.bvar () 0))
+  ] SMT.Context.default with
+  | .ok ([t1, t2], _) =>
+    match Strata.SMTDDM.termToString t1, Strata.SMTDDM.termToString t2 with
+    | .ok s1, .ok s2 =>
+      s1 == "(forall (($__bv0 Int)) true)" &&
+      s2 == "(forall (($__bv1 Bool)) $__bv1)"
+    | _, _ => false
+  | _ => false
+
 -- Test string literal containing double quotes is properly escaped for SMT-LIB 2.7
 -- In SMT-LIB 2.7, double quotes inside strings are escaped by doubling: "a""b" represents a"b
 /--
-info: "; x\n(declare-const x String)\n(define-fun t0 () String x)\n(define-fun t1 () Bool (= t0 \"{\"\"key\"\":\"\"val\"\"}\"))\n"
+info: "; x\n(declare-const x String)\n(define-fun $__t.0 () String x)\n(define-fun $__t.1 () Bool (= $__t.0 \"{\"\"key\"\":\"\"val\"\"}\"))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString
@@ -230,7 +250,7 @@ info: "; x\n(declare-const x String)\n(define-fun t0 () String x)\n(define-fun t
 
 -- Test that Real.Div encodes to `/` (real division) not `div` (integer division).
 /--
-info: "; x\n(declare-const x Real)\n(define-fun t0 () Real x)\n; y\n(declare-const y Real)\n(define-fun t1 () Real y)\n(define-fun t2 () Real (|/| t0 t1))\n"
+info: "; x\n(declare-const x Real)\n(define-fun $__t.0 () Real x)\n; y\n(declare-const y Real)\n(define-fun $__t.1 () Real y)\n(define-fun $__t.2 () Real (|/| $__t.0 $__t.1))\n"
 -/
 #guard_msgs in
 #eval toSMTTermString