Fix Boole tests after merge

Strata/Languages/Boole/Verify.lean

@@ -469,9 +469,11 @@ partial def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do
       let intSub : Core.Expression.Expr := .op () ⟨"Int.Sub", ()⟩ none
       return mkCoreApp Core.seqTakeOp
         [mkCoreApp Core.seqDropOp [s', lo'], mkCoreApp intSub [hi', lo']]
-  -- Typed empty-sequence constant (Sequence.empty for bv32; other types can be added when needed).
-  | .seq_empty_bv8 _ | .seq_empty_bv16 _ | .seq_empty_bv32 _
-  | .seq_empty_bv64 _ | .seq_empty_int _ => return Core.seqEmptyOp
+  | .seq_empty_bv8 _  => return Core.seqEmptyOp (some (.bitvec 8))
+  | .seq_empty_bv16 _ => return Core.seqEmptyOp (some (.bitvec 16))
+  | .seq_empty_bv32 _ => return Core.seqEmptyOp (some (.bitvec 32))
+  | .seq_empty_bv64 _ => return Core.seqEmptyOp (some (.bitvec 64))
+  | .seq_empty_int _  => return Core.seqEmptyOp (some .int)
   -- Sequence literals: Sequence.of_bv32[v0, v1, ..., vn]
   -- Lowers to a left-fold of seq_build over seq_empty.
   | .seq_of_bv8  _ ⟨_, vs⟩ | .seq_of_bv16 _ ⟨_, vs⟩ | .seq_of_bv32 _ ⟨_, vs⟩

Strata/Languages/Core/Factory.lean

@@ -1050,7 +1050,10 @@ def mapConstOp : Expression.Expr := mapConstFunc.opExpr
 def mapSelectOp : Expression.Expr := mapSelectFunc.opExpr
 def mapUpdateOp : Expression.Expr := mapUpdateFunc.opExpr
 def seqLengthOp : Expression.Expr := seqLengthFunc.opExpr
-def seqEmptyOp : Expression.Expr := seqEmptyFunc.opExpr
+def seqEmptyOp (elemTy : Option LMonoTy := none) : Expression.Expr :=
+  match elemTy with
+  | none => seqEmptyFunc.opExpr
+  | some ty => .op default "Sequence.empty" (some (seqTy ty))
 def seqAppendOp : Expression.Expr := seqAppendFunc.opExpr
 def seqSelectOp : Expression.Expr := seqSelectFunc.opExpr
 def seqBuildOp : Expression.Expr := seqBuildFunc.opExpr

StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean

@@ -183,7 +183,11 @@ spec {
 #end
 
 /-- info:
-Obligation: seq_oob_seed_ensures_0_3481
+Obligation: set_v_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ❓ unknown
+
+Obligation: seq_oob_seed_ensures_0_4964
 Property: assert
 Result: ❓ unknown-/
 #guard_msgs in