feat(Boole): SMT-LIB 2.7 cast operators (as_int, as_sint, as_bv{n})

Strata/DL/SMT/DDMTransform/Translate.lean

@@ -206,6 +206,10 @@ partial def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term Provenanc
       let iden := SMTIdentifier.iden_indexed smtProv (mkSymbol "zero_extend")
         (smtAnn #[.ind_numeral smtProv n])
       return mk_qual_identifier (.qi_ident smtProv iden)
+    | .bv (.int_to_bv n) =>
+      let iden := SMTIdentifier.iden_indexed smtProv (mkSymbol "int_to_bv")
+        (smtAnn #[.ind_numeral smtProv n])
+      return mk_qual_identifier (.qi_ident smtProv iden)
     | .str (.re_index n) =>
       let iden := SMTIdentifier.iden_indexed smtProv (mkSymbol "re.^")
         (smtAnn #[.ind_numeral smtProv n])

Strata/DL/SMT/Denote.lean

@@ -854,6 +854,15 @@ and semantics when successful.
   | .app (.zero_extend i) [x] _ =>
     let ⟨.prim (.bitvec n), _, x⟩ ← denoteTerm ctx x | none
     return ⟨.prim (.bitvec (n + i)), rfl, fun Γ => BitVec.zeroExtend (n + i) (x Γ)⟩
+  | .app .ubv_to_int [x] _ =>
+    let ⟨.prim (.bitvec _), _, x⟩ ← denoteTerm ctx x | none
+    return ⟨.prim .int, rfl, fun Γ => Int.ofNat (x Γ).toNat⟩
+  | .app .sbv_to_int [x] _ =>
+    let ⟨.prim (.bitvec _), _, x⟩ ← denoteTerm ctx x | none
+    return ⟨.prim .int, rfl, fun Γ => (x Γ).toInt⟩
+  | .app (.int_to_bv n) [x] _ =>
+    let ⟨.prim .int, _, x⟩ ← denoteTerm ctx x | none
+    return ⟨.prim (.bitvec n), rfl, fun Γ => BitVec.ofInt n (x Γ)⟩
   -- SMT-Lib theory of strings
   | .prim (.string s) =>
     return ⟨.prim .string, rfl, fun _ => s⟩

Strata/DL/SMT/Op.lean

@@ -122,6 +122,9 @@ inductive Op.BV : Type where
   | bvsmulo -- bit-vector signed multiplication overflow predicate
   | bvconcat
   | zero_extend : Nat → Op.BV
+  | ubv_to_int  -- unsigned bitvector → Int  (SMT-LIB 2.7: ubv_to_int)
+  | sbv_to_int  -- signed bitvector → Int    (SMT-LIB 2.7: sbv_to_int)
+  | int_to_bv : Nat → Op.BV -- Int → bitvector (SMT-LIB 2.7: (_ int_to_bv n))
 deriving Repr, DecidableEq, Inhabited, Hashable
 
 inductive Op.Strings : Type where
@@ -223,6 +226,9 @@ elab "#genOpAbbrevs" : command => do
       if ctorName == "zero_extend" then
         let abbrevCmd ← `(command| abbrev $(mkIdent name) (n : Nat) := Op.bv (Op.BV.zero_extend n))
         abbrevs := abbrevs.push (name, abbrevCmd)
+      else if ctorName == "int_to_bv" then
+        let abbrevCmd ← `(command| abbrev $(mkIdent name) (n : Nat) := Op.bv (Op.BV.int_to_bv n))
+        abbrevs := abbrevs.push (name, abbrevCmd)
       else
         let abbrevCmd ← `(command| abbrev $(mkIdent name) := Op.bv $(mkIdent ctor))
         abbrevs := abbrevs.push (name, abbrevCmd)
@@ -254,7 +260,7 @@ elab "#genOpAbbrevs" : command => do
 
 
 /--
-info: Generated abbrevs: #[Op.not, Op.and, Op.or, Op.eq, Op.ite, Op.implies, Op.distinct, Op.uf, Op.neg, Op.sub, Op.add, Op.mul, Op.div, Op.rdiv, Op.mod, Op.abs, Op.le, Op.lt, Op.ge, Op.gt, Op.bvneg, Op.bvadd, Op.bvsub, Op.bvmul, Op.bvnot, Op.bvand, Op.bvor, Op.bvxor, Op.bvshl, Op.bvlshr, Op.bvashr, Op.bvslt, Op.bvsle, Op.bvult, Op.bvsge, Op.bvsgt, Op.bvule, Op.bvugt, Op.bvuge, Op.bvudiv, Op.bvurem, Op.bvsdiv, Op.bvsrem, Op.bvnego, Op.bvsaddo, Op.bvssubo, Op.bvsmulo, Op.bvconcat, Op.zero_extend, Op.str_length, Op.str_concat, Op.str_lt, Op.str_le, Op.str_at, Op.str_substr, Op.str_prefixof, Op.str_suffixof, Op.str_contains, Op.str_indexof, Op.str_replace, Op.str_replace_all, Op.str_to_re, Op.str_in_re, Op.re_none, Op.re_all, Op.re_allchar, Op.re_concat, Op.re_union, Op.re_inter, Op.re_star, Op.str_replace_re, Op.str_replace_re_all, Op.re_comp, Op.re_diff, Op.re_plus, Op.re_opt, Op.re_range, Op.re_loop, Op.re_index, Op.select, Op.store]
+info: Generated abbrevs: #[Op.not, Op.and, Op.or, Op.eq, Op.ite, Op.implies, Op.distinct, Op.uf, Op.neg, Op.sub, Op.add, Op.mul, Op.div, Op.rdiv, Op.mod, Op.abs, Op.le, Op.lt, Op.ge, Op.gt, Op.bvneg, Op.bvadd, Op.bvsub, Op.bvmul, Op.bvnot, Op.bvand, Op.bvor, Op.bvxor, Op.bvshl, Op.bvlshr, Op.bvashr, Op.bvslt, Op.bvsle, Op.bvult, Op.bvsge, Op.bvsgt, Op.bvule, Op.bvugt, Op.bvuge, Op.bvudiv, Op.bvurem, Op.bvsdiv, Op.bvsrem, Op.bvnego, Op.bvsaddo, Op.bvssubo, Op.bvsmulo, Op.bvconcat, Op.zero_extend, Op.ubv_to_int, Op.sbv_to_int, Op.int_to_bv, Op.str_length, Op.str_concat, Op.str_lt, Op.str_le, Op.str_at, Op.str_substr, Op.str_prefixof, Op.str_suffixof, Op.str_contains, Op.str_indexof, Op.str_replace, Op.str_replace_all, Op.str_to_re, Op.str_in_re, Op.re_none, Op.re_all, Op.re_allchar, Op.re_concat, Op.re_union, Op.re_inter, Op.re_star, Op.str_replace_re, Op.str_replace_re_all, Op.re_comp, Op.re_diff, Op.re_plus, Op.re_opt, Op.re_range, Op.re_loop, Op.re_index, Op.select, Op.store]
 -/
 #guard_msgs in
 #genOpAbbrevs
@@ -309,6 +315,9 @@ def Op.mkName : Op → String
   | .bvsmulo       => "bvsmulo"
   | .bvconcat      => "concat"
   | .zero_extend _ => "zero_extend"
+  | .ubv_to_int    => "ubv_to_int"
+  | .sbv_to_int    => "sbv_to_int"
+  | .int_to_bv _   => "int_to_bv"
   | .triggers      => "triggers"
   | .option_get    => "option.get"
   | .datatype_op .tester name => s!"is-{name}"
@@ -349,6 +358,7 @@ def Op.mkName : Op → String
 def Op.LT : Op → Op → Bool
   | .uf f₁, .uf f₂                    => f₁ < f₂
   | .zero_extend n₁, .zero_extend n₂  => n₁ < n₂
+  | .int_to_bv n₁,   .int_to_bv n₂   => n₁ < n₂
   | .re_index n₁, .re_index n₂        => n₁ < n₂
   | .re_loop n₁ n₂, .re_loop m₁ m₂    => n₁ < n₂ && m₁ < m₂
   | ty₁, ty₂                          => ty₁.mkName < ty₂.mkName

Strata/DL/SMT/Translate.lean

@@ -520,6 +520,15 @@ def translateTerm (t : SMT.Term) : TranslateM (Expr × Expr) := do
     let (α, x) ← translateTerm x
     let w ← getBitVecWidth α
     return (mkBitVec (w + i), mkApp3 (.const ``BitVec.zeroExtend []) (toExpr w) (toExpr (w + i)) x)
+  | .app .ubv_to_int [x] _ =>
+    let (_, x) ← translateTerm x
+    return (mkInt, mkApp (.const ``Int.ofNat []) (mkApp (.const ``BitVec.toNat []) x))
+  | .app .sbv_to_int [x] _ =>
+    let (_, x) ← translateTerm x
+    return (mkInt, mkApp (.const ``BitVec.toInt []) x)
+  | .app (.int_to_bv n) [x] _ =>
+    let (_, x) ← translateTerm x
+    return (mkBitVec n, mkApp2 (.const ``BitVec.ofInt []) (toExpr n) x)
   -- SMT-Lib theory of strings
   | .prim (.string s) =>
     return (mkString, toExpr s)

Strata/Languages/Boole/Grammar.lean

@@ -134,6 +134,22 @@ fn seq_drop_first (A : Type, s : Sequence A) : Sequence A =>
 fn seq_subrange (A : Type, s : Sequence A, lo : int, hi : int) : Sequence A =>
   "Sequence.subrange" "(" s ", " lo ", " hi ")";
 
+// Unsigned widening cast: `e as_int` converts a bitvector to Int (unsigned).
+// Lowers to `Bv{n}.ToUInt` Core op → SMT-LIB 2.7 `ubv_to_int`.
+fn cast_to_int (T : Type, e : T) : int => @[prec(80)] e " as_int";
+
+// Signed widening cast: `e as_sint` converts a bitvector to Int (signed, two's complement).
+// Lowers to `Bv{n}.ToInt` Core op → SMT-LIB 2.7 `sbv_to_int`.
+fn cast_to_sint (T : Type, e : T) : int => @[prec(80)] e " as_sint";
+
+// Narrowing cast: `e as_bv{n}` converts an Int to a bitvector of width n (truncating mod 2^n).
+// Lowers to `Int.ToBv{n}` Core op → SMT-LIB 2.7 `(_ int_to_bv n)`.
+fn cast_to_bv1   (e : int) : bv1   => @[prec(80)] e " as_bv1";
+fn cast_to_bv8   (e : int) : bv8   => @[prec(80)] e " as_bv8";
+fn cast_to_bv16  (e : int) : bv16  => @[prec(80)] e " as_bv16";
+fn cast_to_bv32  (e : int) : bv32  => @[prec(80)] e " as_bv32";
+fn cast_to_bv64  (e : int) : bv64  => @[prec(80)] e " as_bv64";
+fn cast_to_bv128 (e : int) : bv128 => @[prec(80)] e " as_bv128";
 
 category Step;
 op step(e: Expr) : Step =>

Strata/Languages/Boole/Verify.lean

@@ -230,6 +230,7 @@ private def typeRange : Boole.Type → SourceRange
   | .bv16 m => m
   | .bv32 m => m
   | .bv64 m => m
+  | .bv128 m => m
   | .Map m _ _ => m
   | .Sequence m _ => m
 
@@ -247,6 +248,7 @@ def toCoreMonoType (t : Boole.Type) : TranslateM Lambda.LMonoTy := do
   | .bv16 _ => return .bitvec 16
   | .bv32 _ => return .bitvec 32
   | .bv64 _ => return .bitvec 64
+  | .bv128 _ => return .bitvec 128
   | .Map _ v k => return .tcons "Map" [← toCoreMonoType k, ← toCoreMonoType v]
   | .Sequence _ elem => return .tcons "Sequence" [← toCoreMonoType elem]
   | _ => throwAt (typeRange t) s!"Unsupported Boole type: {repr t}"
@@ -287,7 +289,8 @@ private def bvWidth (m : SourceRange) (ty : Boole.Type) : TranslateM Nat :=
   | .bv8 _  => return 8
   | .bv16 _ => return 16
   | .bv32 _ => return 32
-  | .bv64 _ => return 64
+  | .bv64 _  => return 64
+  | .bv128 _ => return 128
   | _ => throwAt m s!"Expected bitvector type, got: {repr ty}"
 
 private def toCoreBvUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do
@@ -487,6 +490,25 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do
       return tys.foldr (fun ty acc => .abs () "" (some ty) acc) body'
   -- Function application: `(f)(x)`  →  Core .app
   | .apply_expr _ _ _ f x => return .app () (← toCoreExpr f) (← toCoreExpr x)
+  | .cast_to_int m ty e =>
+    match ty with
+    | .bv1 _ | .bv8 _ | .bv16 _ | .bv32 _ | .bv64 _ | .bv128 _ => do
+      let n ← bvWidth m ty
+      return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToUInt") none) [← toCoreExpr e]
+    | .int _ => toCoreExpr e
+    | _ => throwAt m s!"'as int' requires a bitvector source type, got: {repr ty}"
+  | .cast_to_sint m ty e =>
+    match ty with
+    | .bv1 _ | .bv8 _ | .bv16 _ | .bv32 _ | .bv64 _ | .bv128 _ => do
+      let n ← bvWidth m ty
+      return mkCoreApp (.op () (mkIdent s!"Bv{n}.ToInt") none) [← toCoreExpr e]
+    | _ => throwAt m s!"'as sint' requires a bitvector source type, got: {repr ty}"
+  | .cast_to_bv1   _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv1")   none) [← toCoreExpr e]
+  | .cast_to_bv8   _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv8")   none) [← toCoreExpr e]
+  | .cast_to_bv16  _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv16")  none) [← toCoreExpr e]
+  | .cast_to_bv32  _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv32")  none) [← toCoreExpr e]
+  | .cast_to_bv64  _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv64")  none) [← toCoreExpr e]
+  | .cast_to_bv128 _ e => return mkCoreApp (.op () (mkIdent "Int.ToBv128") none) [← toCoreExpr e]
   | _ => throw (.fromMessage s!"Unsupported expression: {repr e}")
 
 end
@@ -1010,7 +1032,8 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec
       body := ← toCoreBlock b
     } .empty]
   | .command_datatypes _ ⟨_, decls⟩ =>
-    return [.type (.data (← decls.toList.mapM toCoreDatatypeDecl)) .empty]
+    let datatypes ← decls.toList.mapM toCoreDatatypeDecl
+    return [.type (.data datatypes) .empty]
 
 /-- Render a `Boole.Program` to a format object using the provided `GlobalContext` and
 `DialectMap`. These should come from the originating `Strata.Program` (i.e. `env.globalContext`
@@ -1030,7 +1053,7 @@ def formatProgram (prog : Boole.Program) (gctx : GlobalContext) (dialects : Dial
 def toCoreProgram (p : Boole.Program) (gctx : GlobalContext := {}) (fileName : String := "") : Except DiagnosticModel Core.Program := do
   match p with
   | .prog _ ⟨_, cmds⟩ =>
-    -- Pre-pass: collect global variable types and modifies info per procedure.
+    -- Pre-pass: collect global variable types and modifies info.
     let mut varTypes : Std.HashMap String Lambda.LMonoTy := {}
     let mut modMap : Std.HashMap String (List (Core.Expression.Ident × Lambda.LMonoTy)) := {}
     for cmd in cmds do

Strata/Languages/Core/CoreOp.lean

@@ -51,6 +51,9 @@ inductive BvOpKind where
   -- Overflow predicates
   | SAddOverflow | SSubOverflow | SMulOverflow | SNegOverflow | SDivOverflow
   | UAddOverflow | USubOverflow | UMulOverflow | UNegOverflow
+  -- Cross-sort conversion
+  | ToUInt -- unsigned bv → int (ubv_to_int)
+  | ToInt  -- signed bv → int  (sbv_to_int)
   deriving Repr, DecidableEq, Inhabited, BEq, Hashable
 
 structure BvOp where
@@ -69,7 +72,7 @@ def BvOpKind.isPredicate : BvOpKind → Bool
   | _ => false
 
 def BvOpKind.isUnary : BvOpKind → Bool
-  | .Neg | .Not => true
+  | .Neg | .Not | .ToUInt | .ToInt => true
   | _ => false
 
 def BvOpKind.names : List (BvOpKind × String) :=
@@ -89,7 +92,8 @@ def BvOpKind.names : List (BvOpKind × String) :=
    (.SMulOverflow, "SMulOverflow"), (.SNegOverflow, "SNegOverflow"),
    (.SDivOverflow, "SDivOverflow"),
    (.UAddOverflow, "UAddOverflow"), (.USubOverflow, "USubOverflow"),
-   (.UMulOverflow, "UMulOverflow"), (.UNegOverflow, "UNegOverflow")]
+   (.UMulOverflow, "UMulOverflow"), (.UNegOverflow, "UNegOverflow"),
+   (.ToUInt, "ToUInt"), (.ToInt, "ToInt")]
 
 def BvOpKind.toString (k : BvOpKind) : String := lookupName names k
 instance : ToString BvOpKind := ⟨BvOpKind.toString⟩
@@ -241,6 +245,7 @@ inductive CoreOp where
   | map (kind : MapOpKind)
   | seq (kind : SeqOpKind)
   | bvExtract (size hi lo : Nat)
+  | intToBv (n : Nat)  -- int → bv of width n (int_to_bv)
   | trigger (kind : TriggerOpKind)
   | other (name : String)
   deriving Repr, DecidableEq, Inhabited, BEq, Hashable
@@ -257,6 +262,7 @@ def CoreOp.toString : CoreOp → String
   | .map kind => kind.toString
   | .seq kind => s!"Sequence.{kind}"
   | .bvExtract size hi lo => s!"Bv{size}.Extract_{hi}_{lo}"
+  | .intToBv n => s!"Int.ToBv{n}"
   | .trigger kind => kind.toString
   | .other name => name
 
@@ -291,6 +297,12 @@ def CoreOp.ofString (name : String) : CoreOp :=
   match parseBvOp? name with
   | some op => op
   | none =>
+  -- Try "Int.ToBv{n}": int → bitvector of width n
+  if name.startsWith "Int.ToBv" then
+    match (name.drop 8).toString.toNat? with
+    | some n => .intToBv n
+    | none   => .other name
+  else
   -- Try numeric ops: "Int.{kind}" or "Real.{kind}"
   let numPrefixes := [("Int.", NumericType.int), ("Real.", NumericType.real)]
   let numResult := numPrefixes.findSome? fun (pfx, ty) =>

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -50,6 +50,7 @@ type bv8;
 type bv16;
 type bv32;
 type bv64;
+type bv128;
 type Map (dom : Type, range : Type);
 type Sequence (elem : Type);
 
@@ -92,6 +93,7 @@ fn bv8Lit (n : Num) : bv8 => "bv{8}" "(" n ")";
 fn bv16Lit (n : Num) : bv16 => "bv{16}" "(" n ")";
 fn bv32Lit (n : Num) : bv32 => "bv{32}" "(" n ")";
 fn bv64Lit (n : Num) : bv64 => "bv{64}" "(" n ")";
+fn bv128Lit (n : Num) : bv128 => "bv{128}" "(" n ")";
 fn strLit (s : Str) : string => s;
 fn realLit (d : Decimal) : real => d;
 

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -234,6 +234,7 @@ partial def translateLMonoTy (bindings : TransBindings) (arg : Arg) :
   | .ident _ q`Core.bv16 #[] => pure <| .bitvec 16
   | .ident _ q`Core.bv32 #[] => pure <| .bitvec 32
   | .ident _ q`Core.bv64 #[] => pure <| .bitvec 64
+  | .ident _ q`Core.bv128 #[] => pure <| .bitvec 128
   | .ident _ i argst =>
       let argst' ← translateLMonoTys bindings (argst.map ArgF.type)
       pure <| (.tcons i.name argst'.toList.reverse)

Strata/Languages/Core/Factory.lean

@@ -770,10 +770,40 @@ def bvExtractFunc (size hi lo : Nat) : WFLFunc CoreLParams :=
   unaryFuncUneval s!"Bv{size}.Extract_{hi}_{lo}"
     (.bitvec size) (.bitvec (hi + 1 - lo)) rfl rfl
 
+def bvToUIntFunc (size : Nat) : WFLFunc CoreLParams :=
+  unaryFuncUneval s!"Bv{size}.ToUInt" (.bitvec size) .int rfl rfl
+
+def bvToIntFunc (size : Nat) : WFLFunc CoreLParams :=
+  unaryFuncUneval s!"Bv{size}.ToInt" (.bitvec size) .int rfl rfl
+
+def intToBvFunc (size : Nat) : WFLFunc CoreLParams :=
+  unaryFuncUneval s!"Int.ToBv{size}" .int (.bitvec size) rfl rfl
+
 def bv8ConcatFunc  := bvConcatFunc 8
 def bv16ConcatFunc := bvConcatFunc 16
 def bv32ConcatFunc := bvConcatFunc 32
 
+def bv1ToUIntFunc   := bvToUIntFunc 1
+def bv8ToUIntFunc   := bvToUIntFunc 8
+def bv16ToUIntFunc  := bvToUIntFunc 16
+def bv32ToUIntFunc  := bvToUIntFunc 32
+def bv64ToUIntFunc  := bvToUIntFunc 64
+def bv128ToUIntFunc := bvToUIntFunc 128
+
+def bv1ToIntFunc   := bvToIntFunc 1
+def bv8ToIntFunc   := bvToIntFunc 8
+def bv16ToIntFunc  := bvToIntFunc 16
+def bv32ToIntFunc  := bvToIntFunc 32
+def bv64ToIntFunc  := bvToIntFunc 64
+def bv128ToIntFunc := bvToIntFunc 128
+
+def int1ToBvFunc   := intToBvFunc 1
+def int8ToBvFunc   := intToBvFunc 8
+def int16ToBvFunc  := intToBvFunc 16
+def int32ToBvFunc  := intToBvFunc 32
+def int64ToBvFunc  := intToBvFunc 64
+def int128ToBvFunc := intToBvFunc 128
+
 def bv8Extract_7_7_Func    := bvExtractFunc  8  7  7
 def bv16Extract_15_15_Func := bvExtractFunc 16 15 15
 def bv16Extract_7_0_Func   := bvExtractFunc 16  7  0
@@ -864,6 +894,24 @@ def WFFactory : Lambda.WFLFactory CoreLParams :=
   bv8ConcatFunc,
   bv16ConcatFunc,
   bv32ConcatFunc,
+  bv1ToUIntFunc,
+  bv8ToUIntFunc,
+  bv16ToUIntFunc,
+  bv32ToUIntFunc,
+  bv64ToUIntFunc,
+  bv128ToUIntFunc,
+  bv1ToIntFunc,
+  bv8ToIntFunc,
+  bv16ToIntFunc,
+  bv32ToIntFunc,
+  bv64ToIntFunc,
+  bv128ToIntFunc,
+  int1ToBvFunc,
+  int8ToBvFunc,
+  int16ToBvFunc,
+  int32ToBvFunc,
+  int64ToBvFunc,
+  int128ToBvFunc,
   bv8Extract_7_7_Func,
   bv16Extract_15_15_Func,
   bv16Extract_7_0_Func,

Strata/Languages/Core/SMTEncoder.lean

@@ -546,7 +546,10 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte
     | .bv ⟨_, .SLe⟩  => .ok (.app Op.bvsle,      .bool,   ctx)
     | .bv ⟨_, .SGt⟩  => .ok (.app Op.bvsgt,      .bool,   ctx)
     | .bv ⟨_, .SGe⟩  => .ok (.app Op.bvsge,      .bool,   ctx)
-    | .bv ⟨n, .Concat⟩ => .ok (.app Op.bvconcat, .bitvec (n * 2), ctx)
+    | .bv ⟨n, .Concat⟩ => .ok (.app Op.bvconcat,    .bitvec (n * 2), ctx)
+    | .bv ⟨_, .ToUInt⟩  => .ok (.app Op.ubv_to_int,  .int,            ctx)
+    | .bv ⟨_, .ToInt⟩   => .ok (.app Op.sbv_to_int,  .int,            ctx)
+    | .intToBv n        => .ok (.app (Op.int_to_bv n), .bitvec n,     ctx)
 
     | .str .Length   => .ok (.app Op.str_length,    .int,    ctx)
     | .str .Concat   => .ok (.app Op.str_concat,    .string, ctx)