diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean
index aa088ca54f..6361a9fdeb 100644
--- a/Strata/Languages/Core/DDMTransform/Translate.lean
+++ b/Strata/Languages/Core/DDMTransform/Translate.lean
@@ -453,8 +453,8 @@ partial def dealiasTypeExpr (p : Program) (te : TypeExpr) : TypeExpr :=
   match te with
   | (.fvar _ idx #[]) =>
     match p.globalContext.kindOf! idx with
-    | .expr te => te
-    | .type [] (.some te) => te
+    | .expr te => dealiasTypeExpr p te
+    | .type [] (.some te) => dealiasTypeExpr p te
     | _ => te
   | _ => te
 
diff --git a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs
index 05e16b9b9f..2f921c041b 100644
--- a/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs
+++ b/Tools/BoogieToStrata/IntegrationTests/BoogieToStrataIntegrationTests.cs
@@ -51,7 +51,28 @@ public static IEnumerable<object[]> GetBoogieTestFiles() {
         }
     }
 
+    /// <summary>
+    /// Returns true if the first 5 lines of <paramref name="filePath"/> contain
+    /// the literal token "{:smack}". Files carrying this marker opt into the
+    /// --smack CLI flag, which gates the assert_.<type> synthetic-requires
+    /// injection and InferModifies=true.
+    /// </summary>
+    private static bool HasSmackMarker(string filePath) {
+        if (!File.Exists(filePath)) return false;
+        using var reader = new StreamReader(filePath);
+        for (var i = 0; i < 5; i++) {
+            var line = reader.ReadLine();
+            if (line == null) break;
+            if (line.Contains("{:smack}", StringComparison.Ordinal)) return true;
+        }
+        return false;
+    }
+
     private (int, string, string) RunTranslation(string filePath) {
+        return RunTranslation(filePath, HasSmackMarker(filePath));
+    }
+
+    private (int, string, string) RunTranslation(string filePath, bool smack) {
         // Capture console output
         using var consoleOutput = new StringWriter();
         using var consoleError = new StringWriter();
@@ -62,7 +83,8 @@ public static IEnumerable<object[]> GetBoogieTestFiles() {
         try {
             Console.SetOut(consoleOutput);
             Console.SetError(consoleError);
-            exitCode = BoogieToStrata.Main([filePath]);
+            var args = smack ? new[] { "--smack", filePath } : new[] { filePath };
+            exitCode = BoogieToStrata.Main(args);
         } catch (Exception) {
             exitCode = 1;
         } finally {
@@ -149,6 +171,182 @@ public void VerifyTestFile(string fileName, string filePath) {
         Assert.Equal(expectedExitCode, proc.ExitCode);
     }
 
+    /// <summary>
+    /// Regression test: assert_.<type> procedures must produce a single
+    /// merged spec block, not duplicates, regardless of whether the input
+    /// already has user-written specs. Two cases:
+    ///   1. existing ensures only — synthetic requires merges in.
+    ///   2. existing requires — synthetic requires is added alongside,
+    ///      not silently dropped.
+    /// </summary>
+    [Fact]
+    public void SmackAssertProducesSingleMergedSpecBlock() {
+        var filePath = Path.Combine(TestsDirectory, "SmackAssertDuplicateSpec.bpl");
+        Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}");
+
+        var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath);
+        Assert.Equal(0, exitCode);
+
+        // Three procedures (assert_.i32, assert_.i32_with_req, main); the two
+        // assert_.<type> ones each produce one spec block; main has none.
+        // Count occurrences of "spec {" in the output: must be exactly 2.
+        var specCount = 0;
+        var searchFrom = 0;
+        while (true) {
+            var idx = standardOutput.IndexOf("spec {", searchFrom, StringComparison.Ordinal);
+            if (idx < 0) break;
+            specCount++;
+            searchFrom = idx + 1;
+        }
+
+        output.WriteLine($"Output:\n{standardOutput}");
+        Assert.Equal(2, specCount);
+
+        // Overall sanity: the output contains at least one of each clause kind.
+        // (assert_.i32 has an `ensures`, both procedures have at least one
+        // `requires`.)
+        Assert.Contains("requires", standardOutput);
+        Assert.Contains("ensures", standardOutput);
+
+        // The critical regression check: BOTH clauses must appear in the
+        // SECOND procedure's spec block (assert_.i32_with_req) — i.e., the
+        // requires-already-present case must not silently drop the synthetic
+        // clause. Procedures emit in source order, so the second `spec {` is
+        // assert_.i32_with_req's.
+        var firstSpec = standardOutput.IndexOf("spec {", StringComparison.Ordinal);
+        Assert.True(firstSpec >= 0, "Expected at least one spec block");
+        var secondSpecStart = standardOutput.IndexOf("spec {", firstSpec + 1, StringComparison.Ordinal);
+        Assert.True(secondSpecStart >= 0, "Expected a second spec block for assert_.i32_with_req");
+        var secondSpecEnd = standardOutput.IndexOf("}", secondSpecStart, StringComparison.Ordinal);
+        Assert.True(secondSpecEnd > secondSpecStart, "Second spec block missing closing brace");
+        var secondSpec = standardOutput.Substring(secondSpecStart, secondSpecEnd - secondSpecStart);
+
+        // The user-written `requires (p.0 > -1)` (sanitized to `p_0 > -(1)`)
+        // and the synthetic `requires (p.0 != 0)` (sanitized to `p_0 != 0`)
+        // must both be present in this single spec block.
+        Assert.Contains("p_0 > -(1)", secondSpec);
+        Assert.Contains("p_0 != 0", secondSpec);
+    }
+
+    /// <summary>
+    /// Regression test: old() expressions must use the renamed name when a
+    /// variable has a name collision (e.g., global var `main` vs procedure `main`).
+    /// Previously, IdentifierExpr with Decl != null used NameOf() correctly, but
+    /// had a silent fallback to Name() when Decl was null — which would emit the
+    /// unrenamed (wrong) name in the collision case. Post-resolution, Decl should
+    /// always be non-null; the fallback masked potential bugs.
+    /// </summary>
+    [Fact]
+    public void OldExprUsesRenamedNameOnCollision() {
+        var filePath = Path.Combine(TestsDirectory, "OldExprRenameCollision.bpl");
+        Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}");
+
+        var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath);
+
+        output.WriteLine($"Output:\n{standardOutput}");
+        if (!string.IsNullOrEmpty(errorOutput)) {
+            output.WriteLine($"Error output: {errorOutput}");
+        }
+
+        Assert.Equal(0, exitCode);
+
+        // The output should contain an `old` expression referencing the *renamed*
+        // variable (e.g., __var_main), not the raw name `main` which is the procedure.
+        // Look for the pattern "old __var_main" or similar renamed form.
+        Assert.Contains("old __var_main", standardOutput);
+
+        // Also ensure the output does NOT contain "old main" (unrenamed fallback).
+        // This would indicate the fallback to Name() was used instead of NameOf().
+        Assert.DoesNotContain("old main", standardOutput);
+    }
+
+    /// <summary>
+    /// Regression test for InferModifies = true.
+    ///
+    /// SMACK-generated Boogie can omit explicit modifies clauses on procedures.
+    /// With InferModifies = true, Boogie's ModSetCollector infers them so that
+    /// the translator correctly emits globals as `inout` parameters (modified)
+    /// rather than read-only parameters.
+    ///
+    /// This test uses a .bpl file where procedure p() assigns to global g but
+    /// has no `modifies g;` clause.  If InferModifies is working, the output
+    /// should contain `inout g` for procedure p.
+    /// </summary>
+    [Fact]
+    public void InferModifiesEmitsInoutForMutatedGlobal() {
+        var filePath = Path.Combine(TestsDirectory, "InferModifiesGlobal.bpl");
+        Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}");
+
+        var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath);
+
+        output.WriteLine($"Output:\n{standardOutput}");
+        if (!string.IsNullOrEmpty(errorOutput)) {
+            output.WriteLine($"Error output: {errorOutput}");
+        }
+
+        // Translation must succeed — if InferModifies is broken, Boogie would
+        // reject the program because g is assigned without a modifies clause.
+        Assert.Equal(0, exitCode);
+
+        // The inferred modifies clause should cause the translator to emit
+        // `inout g` on procedure p's parameter list.
+        Assert.Contains("inout g", standardOutput);
+    }
+
+    /// <summary>
+    /// Pin down the --smack gate: without the flag, the assert_.<type>
+    /// pattern is treated as an opaque procedure (no synthetic requires
+    /// injected). Translation succeeds; the output does not contain a
+    /// requires clause for the assert_ procedure.
+    /// </summary>
+    [Fact]
+    public void SmackAssertWithoutFlagDoesNotInjectRequires() {
+        var filePath = Path.Combine(TestsDirectory, "SmackAssert.bpl");
+        Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}");
+
+        var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath, smack: false);
+
+        output.WriteLine($"Output:\n{standardOutput}");
+        if (!string.IsNullOrEmpty(errorOutput)) {
+            output.WriteLine($"Error output: {errorOutput}");
+        }
+
+        Assert.Equal(0, exitCode);
+
+        // Without --smack, no synthetic requires is added, so no `requires`
+        // clause should appear anywhere in the translation of this file
+        // (the .bpl has no user-written requires either).
+        Assert.DoesNotContain("requires", standardOutput);
+    }
+
+    /// <summary>
+    /// Pin down the --smack gate: without the flag, InferModifies is off.
+    /// A program that omits an explicit `modifies` clause on a procedure
+    /// that mutates a global is rejected at typecheck.
+    /// </summary>
+    [Fact]
+    public void InferModifiesOffWithoutSmackFlag() {
+        var filePath = Path.Combine(TestsDirectory, "InferModifiesGlobal.bpl");
+        Assert.True(File.Exists(filePath), $"Test file does not exist: {filePath}");
+
+        var (exitCode, standardOutput, errorOutput) = RunTranslation(filePath, smack: false);
+
+        output.WriteLine($"Exit code: {exitCode}");
+        output.WriteLine($"Output:\n{standardOutput}");
+        if (!string.IsNullOrEmpty(errorOutput)) {
+            output.WriteLine($"Error output: {errorOutput}");
+        }
+
+        // Without --smack, ResolveAndTypecheck rejects the program because
+        // procedure p mutates global g without an explicit `modifies g;`
+        // clause. BoogieToStrata.Main writes a "Failed to typecheck" line
+        // to stderr and returns exit code 1. Pin both signals so a future
+        // regression that fails for an unrelated reason (parse error,
+        // arg-handling change) doesn't silently pass this test.
+        Assert.Equal(1, exitCode);
+        Assert.Contains("Failed to typecheck", errorOutput);
+    }
+
     [Fact]
     public void ErrorCodeWithNoArguments() {
         var result = BoogieToStrata.Main(Array.Empty<string>());
diff --git a/Tools/BoogieToStrata/Source/BoogieToStrata.cs b/Tools/BoogieToStrata/Source/BoogieToStrata.cs
index 1816f6a1fc..de97643552 100644
--- a/Tools/BoogieToStrata/Source/BoogieToStrata.cs
+++ b/Tools/BoogieToStrata/Source/BoogieToStrata.cs
@@ -3,22 +3,59 @@
 namespace BoogieToStrata;
 
 public static class BoogieToStrata {
+    private const string Usage = "Usage: BoogieToStrata [--smack] <inputFile>";
+
+    private static bool _smack;
+
     private static void PrintResolvedProgram(ExecutionEngineOptions options, ProcessedProgram prog) {
         var writer = new TokenTextWriter(Console.Out, options);
-        StrataGenerator.EmitProgramAsStrata(options, prog.Program, writer);
+        StrataGenerator.EmitProgramAsStrata(options, prog.Program, writer, _smack);
+    }
+
+    /// <summary>
+    /// Parse args into (smack, filename). Returns false on any malformed
+    /// invocation (zero or two-plus positional args, unknown flags); the
+    /// caller should print Usage and return exit code 1.
+    /// </summary>
+    private static bool TryParseArgs(string[] args, out bool smack, out string filename) {
+        smack = false;
+        filename = "";
+        string? positional = null;
+        foreach (var arg in args) {
+            if (arg == "--smack") {
+                smack = true;
+            } else if (arg.StartsWith("--")) {
+                return false; // unknown flag
+            } else if (positional == null) {
+                positional = arg;
+            } else {
+                return false; // two positional args
+            }
+        }
+        if (positional == null) return false; // no positional arg
+        filename = positional;
+        return true;
     }
 
     public static int Main(string[] args) {
-        if (args.Length != 1) {
-            Console.Error.WriteLine("Usage: BoogieToStrata <inputFile>");
+        if (!TryParseArgs(args, out var smack, out var filename)) {
+            Console.Error.WriteLine(Usage);
             return 1;
         }
-
-        var filename = args[0];
+        _smack = smack;
 
         var options = new CommandLineOptions(Console.Out, new ConsolePrinter()) {
             Verify = false,
-            TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates
+            TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates,
+            // Under --smack, SMACK-generated Boogie often omits explicit
+            // `modifies` clauses on procedures that mutate globals.
+            // InferModifies runs ModSetCollector.CollectModifies to populate
+            // empty modifies clauses and suppresses modifies-clause
+            // typechecking (via CheckModifies), so that ResolveAndTypecheck
+            // does not reject SMACK programs missing modifies clauses.
+            // For strict Boogie input (no --smack), this stays false and
+            // missing modifies clauses are reported as typecheck errors.
+            InferModifies = smack
         };
 
         var boogieEngine = ExecutionEngine.CreateWithoutSharedCache(options);
@@ -44,4 +81,4 @@ public static int Main(string[] args) {
 
         return 0;
     }
-}
\ No newline at end of file
+}
diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs
index 368e6e7b5f..ad269fc77a 100644
--- a/Tools/BoogieToStrata/Source/StrataGenerator.cs
+++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs
@@ -52,15 +52,33 @@ public class StrataGenerator : ReadOnlyVisitor {
     // Global variables collected from the program, used to convert them
     // into inout/input parameters on procedure headers and call sites.
     private List<GlobalVariable> _globalVariables = [];
-
-    private StrataGenerator(VCGenOptions options, TokenTextWriter writer, Program program) {
+    // Renames for declarations whose sanitized name collides with another
+    // declaration. Keyed by Boogie Declaration object to avoid ambiguity
+    // when two entities share the same original name (e.g., const main and
+    // procedure main). First-seen wins; later entities get prefixed.
+    //
+    // Registration order determines who wins a collision:
+    //   1. Procedures  — registered first, always keep their name.
+    //   2. Implementations — claimed defensively (they share names with
+    //      their procedures, but claiming guards against edge cases).
+    //   3. Constants, Functions, Globals — registered last; in a
+    //      proc-vs-const collision the constant is always renamed.
+    private readonly Dictionary<Declaration, string> _renames = new();
+    // True when the input is SMACK-generated Boogie. Gates SMACK-specific
+    // accommodations (synthetic `requires (p != 0)` on assert_.<type> procedures).
+    // The companion `InferModifies = true` knob is set on the Boogie options
+    // by the BoogieToStrata.Main entrypoint, also gated on this flag.
+    private readonly bool _smack;
+
+    private StrataGenerator(VCGenOptions options, TokenTextWriter writer, Program program, bool smack) {
         _options = options;
         _writer = writer;
         _program = program;
+        _smack = smack;
     }
 
-    public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTextWriter writer) {
-        var generator = new StrataGenerator(options, writer, p);
+    public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTextWriter writer, bool smack) {
+        var generator = new StrataGenerator(options, writer, p, smack);
 
         var fieldTypeCollector = new FieldTypeCollector();
         fieldTypeCollector.Visit(p);
@@ -74,6 +92,31 @@ public static void EmitProgramAsStrata(VCGenOptions options, Program p, TokenTex
 
             generator.FindSpecialTypes();
 
+            // Build rename map for declarations with colliding sanitized names.
+            // Two kinds of collision are handled:
+            //   1. Cross-namespace: constant vs procedure sharing the same name
+            //   2. Sanitization: distinct names that map to the same string
+            //      (e.g., $add.i32 and $add_i32 both become _add_i32)
+            // First-seen wins; colliding entities get a suffix (_2, _3, ...).
+            var claimed = new HashSet<string>();
+
+            foreach (var proc in p.Procedures)
+                ClaimOrRename(proc, proc.Name, "__proc_", claimed, generator._renames);
+            // Defensive: implementations share names with their corresponding
+            // procedures, so they would normally never collide. Claiming them
+            // here guards against edge cases (e.g., an implementation whose
+            // procedure was pruned or renamed upstream).
+            foreach (var impl in p.Implementations) {
+                var sanitized = SanitizeNameForStrata(impl.Name);
+                claimed.Add(sanitized);
+            }
+            foreach (var c in liveDeclarations.OfType<Constant>())
+                ClaimOrRename(c, c.TypedIdent.Name, "__const_", claimed, generator._renames);
+            foreach (var f in liveDeclarations.OfType<Function>())
+                ClaimOrRename(f, f.Name, "__func_", claimed, generator._renames);
+            foreach (var g in p.GlobalVariables)
+                ClaimOrRename(g, g.Name, "__var_", claimed, generator._renames);
+
             var typeConstructors = p.TopLevelDeclarations.OfType<TypeCtorDecl>().ToList();
             if (typeConstructors.Count != 0) {
                 generator.WriteLine("// Type constructors");
@@ -205,6 +248,29 @@ private static string SanitizeNameForStrata(string name) {
             .Replace("$", "_");
     }
 
+    /// <summary>
+    /// Claim a sanitized name for <paramref name="decl"/>, or rename it if the
+    /// name is already taken. The first declaration to claim a name wins;
+    /// subsequent colliders get a prefixed (and possibly suffixed) name recorded
+    /// in <paramref name="renames"/>.
+    /// </summary>
+    private static void ClaimOrRename(
+        Declaration decl,
+        string originalName,
+        string prefix,
+        HashSet<string> claimed,
+        Dictionary<Declaration, string> renames) {
+        var sanitized = SanitizeNameForStrata(originalName);
+        if (claimed.Add(sanitized)) return;
+        var candidate = $"{prefix}{sanitized}";
+        if (!claimed.Add(candidate)) {
+            var i = 2;
+            while (!claimed.Add($"{candidate}_{i}")) i++;
+            candidate = $"{candidate}_{i}";
+        }
+        renames[decl] = candidate;
+    }
+
     private void AddUniqueConst(Type t, string name) {
         if (!_uniqueConstants.TryGetValue(t, out var value)) {
             value = new HashSet<string>();
@@ -299,6 +365,12 @@ private string Name(string name) {
         return SanitizeNameForStrata(name);
     }
 
+    private string NameOf(Declaration decl, string originalName) {
+        if (_renames.TryGetValue(decl, out var renamed))
+            return renamed;
+        return SanitizeNameForStrata(originalName);
+    }
+
     private void WriteLine(string text) {
         _writer.WriteLine(text);
     }
@@ -310,7 +382,10 @@ private void EmitOldExpr(Expr expr) {
         switch (expr) {
             case IdentifierExpr identExpr:
                 WriteText("old ");
-                WriteText(Name(identExpr.Name));
+                if (identExpr.Decl == null)
+                    throw new StrataConversionException(identExpr.tok,
+                        $"IdentifierExpr '{identExpr.Name}' has null Decl (expected non-null post-resolution)");
+                WriteText(NameOf(identExpr.Decl, identExpr.Name));
                 break;
             case NAryExpr { Fun: MapSelect } mapSelect:
                 WriteText("(");
@@ -546,7 +621,10 @@ public override Expr VisitExpr(Expr node) {
             case LiteralExpr literalExpr:
                 throw new StrataConversionException(node.tok, $"Unsupported literal type: {literalExpr}");
             case IdentifierExpr identifierExpr:
-                WriteText(Name(identifierExpr.Name));
+                if (identifierExpr.Decl == null)
+                    throw new StrataConversionException(identifierExpr.tok,
+                        $"IdentifierExpr '{identifierExpr.Name}' has null Decl (expected non-null post-resolution)");
+                WriteText(NameOf(identifierExpr.Decl, identifierExpr.Name));
                 break;
             case NAryExpr nAryExpr: {
                 var fun = nAryExpr.Fun;
@@ -634,7 +712,7 @@ public override Expr VisitExpr(Expr node) {
 
                         break;
                     case FunctionCall functionCall: {
-                        WriteText($"{Name(functionCall.FunctionName)}(");
+                        WriteText($"{NameOf(functionCall.Func, functionCall.FunctionName)}(");
                         EmitSeparated(args, e => VisitExpr(e), ", ");
                         WriteText(")");
                         break;
@@ -918,7 +996,7 @@ public override GotoCmd VisitGotoCmd(GotoCmd node) {
 
     private void EmitSimpleAssign(SimpleAssignLhs lhs, Expr rhs) {
         Indent();
-        WriteText($"{Name(lhs.AssignedVariable.Name)} := ");
+        WriteText($"{NameOf(lhs.AssignedVariable.Decl, lhs.AssignedVariable.Name)} := ");
         VisitExpr(rhs);
         WriteLine(";");
     }
@@ -953,17 +1031,17 @@ public override Cmd VisitCallCmd(CallCmd node) {
         var modifiesNames = new HashSet<string>(callee.Modifies.Select(m => m.Name));
 
         Indent("call ");
-        WriteText($"{Name(callee.Name)}(");
+        WriteText($"{NameOf(callee, callee.Name)}(");
         // Emit: inout globals, then read-only globals, then original args, then out outputs.
         var needComma = false;
         foreach (var g in _globalVariables.Where(g => modifiesNames.Contains(g.Name))) {
             if (needComma) WriteText(", ");
-            WriteText($"inout {Name(g.Name)}");
+            WriteText($"inout {NameOf(g, g.Name)}");
             needComma = true;
         }
         foreach (var g in _globalVariables.Where(g => !modifiesNames.Contains(g.Name))) {
             if (needComma) WriteText(", ");
-            WriteText(Name(g.Name));
+            WriteText(NameOf(g, g.Name));
             needComma = true;
         }
         foreach (var arg in node.Ins) {
@@ -983,7 +1061,7 @@ public override Cmd VisitCallCmd(CallCmd node) {
 
     public override Cmd VisitHavocCmd(HavocCmd node) {
         foreach (var x in node.Vars) {
-            IndentLine($"havoc {Name(x.Name)};");
+            IndentLine($"havoc {NameOf(x.Decl, x.Name)};");
         }
 
         // All assumptions come after all havocs! This allows where clauses
@@ -1510,7 +1588,7 @@ public override Block VisitBlock(Block node) {
 
     public override Constant VisitConstant(Constant node) {
         var ti = node.TypedIdent;
-        var name = Name(ti.Name);
+        var name = NameOf(node, ti.Name);
         WriteText($"const {name} : ");
         VisitType(ti.Type);
         if (node.Unique) {
@@ -1523,7 +1601,7 @@ public override Constant VisitConstant(Constant node) {
 
     public override GlobalVariable VisitGlobalVariable(GlobalVariable node) {
         var ti = node.TypedIdent;
-        WriteText($"var {Name(ti.Name)} : ");
+        WriteText($"var {NameOf(node, ti.Name)} : ");
         VisitType(ti.Type);
         WriteLine(";");
         return node;
@@ -1681,7 +1759,7 @@ private void MaybeEmitBuiltinBody(Function function) {
     }
 
     public override Function VisitFunction(Function node) {
-        WriteText($"function {Name(node.Name)}");
+        WriteText($"function {NameOf(node, node.Name)}");
         EmitTypeParameters(node.TypeParameters);
         WriteText("(");
         WriteFormals(node.InParams);
@@ -1723,7 +1801,7 @@ private void WriteProcedureHeader(Procedure proc) {
         var modifiesGlobals = _globalVariables.Where(g => modifiesNames.Contains(g.Name)).ToList();
         var readOnlyGlobals = _globalVariables.Where(g => !modifiesNames.Contains(g.Name)).ToList();
 
-        WriteText($"procedure {Name(proc.Name)}");
+        WriteText($"procedure {NameOf(proc, proc.Name)}");
         EmitTypeParameters(proc.TypeParameters);
         WriteText("(");
         // Emit: inout globals, then read-only globals, then original inputs, then out outputs.
@@ -1772,9 +1850,36 @@ private void WriteProcedureHeader(Procedure proc) {
 
     public override Procedure VisitProcedure(Procedure node) {
         if (!_program.Implementations.Any(i => i.Name.Equals(node.Name))) {
-            WriteProcedureHeader(node);
-            WriteLine(";");
-            WriteLine();
+            // Under --smack, SMACK encodes C assert(expr) as a call to
+            // assert_.*(cond). Inject a synthetic requires precondition so the
+            // call-elimination pass generates a VC checking the condition is
+            // non-zero. We add it to node.Requires so WriteProcedureHeader
+            // emits it inside a single spec block alongside any existing
+            // specs. The injection always fires when the name pattern matches
+            // (no Requires.Count == 0 guard) — if the procedure already has a
+            // hand-written requires, both clauses appear in the merged spec
+            // block, preserving the SMACK invariant unconditionally.
+            Requires? syntheticReq = null;
+            if (_smack && node.Name.StartsWith("assert_.") && node.InParams.Count > 0) {
+                var param = node.InParams[0];
+                var paramExpr = new IdentifierExpr(param.tok, param);
+                var zero = new LiteralExpr(param.tok, Microsoft.BaseTypes.BigNum.FromInt(0));
+                var neqExpr = Expr.Neq(paramExpr, zero);
+                syntheticReq = new Requires(false, neqExpr);
+                node.Requires.Add(syntheticReq);
+            }
+
+            try {
+                WriteProcedureHeader(node);
+                WriteLine(";");
+                WriteLine();
+            } finally {
+                // Remove the synthetic requires to avoid mutating the shared
+                // AST, even if WriteProcedureHeader threw.
+                if (syntheticReq != null) {
+                    node.Requires.Remove(syntheticReq);
+                }
+            }
         }
 
         return node;
@@ -1787,7 +1892,7 @@ private void WriteFormals(IEnumerable<Variable> variables, ref bool needComma,
             if (needComma) WriteText(", ");
             var name = v.TypedIdent.Name ?? "";
             if (name == "") name = $"x{n++}";
-            WriteText($"{prefix}{Name(name)} : ");
+            WriteText($"{prefix}{NameOf(v, name)} : ");
             VisitType(v.TypedIdent.Type);
             needComma = true;
         }
diff --git a/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl
new file mode 100644
index 0000000000..50bdf5579f
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.bpl
@@ -0,0 +1,12 @@
+// {:smack}
+// Regression test: procedures starting with "assert_" but NOT matching
+// SMACK's assert_.TYPE pattern should NOT get a synthetic requires.
+// Only assert_.<type> (literal dot) is the SMACK pattern.
+
+procedure assert_helper(p: int) returns (r: int);
+
+procedure main() returns (r: int)
+{
+  // assert_helper is a normal procedure, passing 0 should be fine
+  call r := assert_helper(0);
+}
diff --git a/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.expect b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.expect
new file mode 100644
index 0000000000..e9e8e85d9e
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/AssertPrefixFalsePositive.expect
@@ -0,0 +1,2 @@
+Successfully parsed.
+All 0 goals passed.
diff --git a/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.bpl b/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.bpl
new file mode 100644
index 0000000000..5a1275cbff
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.bpl
@@ -0,0 +1,9 @@
+const $a.b: int;   axiom $a.b > 0;
+var   $a_b: int;   // both sanitize to _a_b
+procedure main() returns (r: int)
+  modifies $a_b;
+{
+  $a_b := 1;
+  havoc $a_b;
+  r := $a.b + $a_b;
+}
diff --git a/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.expect b/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.expect
new file mode 100644
index 0000000000..e9e8e85d9e
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/GlobalVarRenameCollision.expect
@@ -0,0 +1,2 @@
+Successfully parsed.
+All 0 goals passed.
diff --git a/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl
new file mode 100644
index 0000000000..0767f22518
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.bpl
@@ -0,0 +1,17 @@
+// {:smack}
+// Regression test for InferModifies = true.
+//
+// This procedure mutates the global variable `g` but has NO explicit
+// `modifies g;` clause.  With InferModifies = true, Boogie's
+// ModSetCollector should infer the modifies clause so that the
+// BoogieToStrata translator emits `inout g` for procedure p.
+// If InferModifies is ever disabled or broken, this file will fail
+// to translate correctly (g would be treated as read-only instead
+// of inout).
+
+var g: int;
+
+procedure p()
+{
+  g := 1;
+}
diff --git a/Tools/BoogieToStrata/Tests/InferModifiesGlobal.expect b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.expect
new file mode 100644
index 0000000000..e9e8e85d9e
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/InferModifiesGlobal.expect
@@ -0,0 +1,2 @@
+Successfully parsed.
+All 0 goals passed.
diff --git a/Tools/BoogieToStrata/Tests/NamespaceCollision.bpl b/Tools/BoogieToStrata/Tests/NamespaceCollision.bpl
new file mode 100644
index 0000000000..caedc2c08a
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/NamespaceCollision.bpl
@@ -0,0 +1,25 @@
+// Minimal reproduction: namespace collision bug in BoogieToStrata.
+// Boogie allows a constant and procedure to share the same name
+// because they live in separate namespaces. BoogieToStrata emits
+// both into Strata Core's single namespace, causing:
+//   "a declaration of this name already exists"
+
+type ref = int;
+
+const main: ref;
+axiom (main == 1000);
+
+var x: int;
+
+procedure main()
+  modifies x;
+{
+  var y: int;
+  x := 42;
+  assert x == 42;
+  // Use the constant in an expression that doesn't require the axiom to verify
+  y := 0;
+  if (main == 1000) { y := 1; }
+  // This assertion is trivially true regardless of the axiom
+  assert y == 0 || y == 1;
+}
diff --git a/Tools/BoogieToStrata/Tests/NamespaceCollision.expect b/Tools/BoogieToStrata/Tests/NamespaceCollision.expect
new file mode 100644
index 0000000000..c2c458ba8c
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/NamespaceCollision.expect
@@ -0,0 +1,4 @@
+Successfully parsed.
+NamespaceCollision.core.st(23, 4) [assert_0]: ✅ pass
+NamespaceCollision.core.st(33, 4) [assert_1]: ✅ pass
+All 2 goals passed.
diff --git a/Tools/BoogieToStrata/Tests/OldExprRenameCollision.bpl b/Tools/BoogieToStrata/Tests/OldExprRenameCollision.bpl
new file mode 100644
index 0000000000..7494acd002
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/OldExprRenameCollision.bpl
@@ -0,0 +1,17 @@
+// Regression test: old() expression with a renamed (colliding) variable.
+//
+// The global variable `main` collides with procedure `main` after
+// sanitization (cross-namespace collision). The variable must be
+// renamed when emitted. An old() expression referencing that variable
+// must use the *renamed* name, not the raw sanitized name.
+// If the code silently falls back to Name() instead of NameOf(), the
+// old() expression will reference the wrong (procedure) name.
+
+var main: int;
+
+procedure main()
+  modifies main;
+  ensures main == old(main) + 1;
+{
+  main := main + 1;
+}
diff --git a/Tools/BoogieToStrata/Tests/OldExprRenameCollision.expect b/Tools/BoogieToStrata/Tests/OldExprRenameCollision.expect
new file mode 100644
index 0000000000..98a3632dbf
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/OldExprRenameCollision.expect
@@ -0,0 +1,3 @@
+Successfully parsed.
+OldExprRenameCollision.core.st(10, 2) [main_ensures_0]: ✅ pass
+All 1 goals passed.
diff --git a/Tools/BoogieToStrata/Tests/SanitizationCollision.bpl b/Tools/BoogieToStrata/Tests/SanitizationCollision.bpl
new file mode 100644
index 0000000000..7a4f339a01
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/SanitizationCollision.bpl
@@ -0,0 +1,25 @@
+// Test case: sanitization collision in BoogieToStrata.
+//
+// SanitizeNameForStrata replaces '.', '$', '@', '#', '^' with '_'.
+// This means distinct Boogie identifiers can map to the same Strata name:
+//   $add.i32  →  _add_i32
+//   $add_i32  →  _add_i32   (collision!)
+//
+// The rename mechanism should detect this and disambiguate.
+
+type i32 = int;
+
+function {:inline} $add.i32(i1: i32, i2: i32) returns (i32) { i1 + i2 }
+function {:inline} $add_i32(i1: i32, i2: i32) returns (i32) { i1 + i2 }
+
+procedure main() returns (r: i32)
+ensures r == 5;
+{
+  var a: i32;
+  var b: i32;
+  a := $add.i32(2, 3);
+  b := $add_i32(2, 3);
+  assert a == 5;
+  assert b == 5;
+  r := a;
+}
diff --git a/Tools/BoogieToStrata/Tests/SanitizationCollision.expect b/Tools/BoogieToStrata/Tests/SanitizationCollision.expect
new file mode 100644
index 0000000000..d7e99638ef
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/SanitizationCollision.expect
@@ -0,0 +1,5 @@
+Successfully parsed.
+SanitizationCollision.core.st(29, 4) [assert_0]: ✅ pass
+SanitizationCollision.core.st(30, 4) [assert_1]: ✅ pass
+SanitizationCollision.core.st(21, 2) [main_ensures_0]: ✅ pass
+All 3 goals passed.
diff --git a/Tools/BoogieToStrata/Tests/SmackAssert.bpl b/Tools/BoogieToStrata/Tests/SmackAssert.bpl
new file mode 100644
index 0000000000..5094a86704
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/SmackAssert.bpl
@@ -0,0 +1,18 @@
+// {:smack}
+// Minimal test case for SMACK assert_ pattern recognition.
+// SMACK encodes C assert(expr) as a call to assert_.i32(cond).
+// BoogieToStrata should recognize this pattern and emit:
+//   assert (cond != 0);
+// instead of an opaque procedure call.
+
+type i32 = int;
+
+procedure assert_.i32(p.0: i32) returns ($r: i32);
+
+procedure main() returns ($r: i32)
+{
+  // assert(false) — should fail verification
+  call $r := assert_.i32(0);
+  $r := 0;
+  return;
+}
diff --git a/Tools/BoogieToStrata/Tests/SmackAssert.expect b/Tools/BoogieToStrata/Tests/SmackAssert.expect
new file mode 100644
index 0000000000..8af84c0bbc
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/SmackAssert.expect
@@ -0,0 +1,3 @@
+Successfully parsed.
+SmackAssert.core.st(21, 6) [callElimAssert_assert__i32_requires_0_2]: ❌ fail
+Finished with 0 goals passed, 1 failed.
diff --git a/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl b/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl
new file mode 100644
index 0000000000..3f3d49bce3
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/SmackAssertDuplicateSpec.bpl
@@ -0,0 +1,30 @@
+// {:smack}
+// Regression test: assert_.<type> procedures must produce a single
+// merged spec block, not duplicates, regardless of whether the input
+// already has user-written specs.
+//
+// Two procedures exercise the two cases:
+//   1. assert_.i32 has only an existing `ensures` — output must merge
+//      the synthetic `requires (p.0 != 0)` with the existing ensures
+//      into one spec block.
+//   2. assert_.i32_with_req has an existing `requires (p.0 > -1)` —
+//      output must contain BOTH requires clauses (the synthetic one
+//      and the user-written one) in a single spec block, not drop the
+//      synthetic one.
+
+type i32 = int;
+
+procedure assert_.i32(p.0: i32) returns ($r: i32);
+  ensures ($r == 0);
+
+procedure assert_.i32_with_req(p.0: i32) returns ($r: i32);
+  requires (p.0 > -1);
+
+procedure main() returns ($r: i32)
+{
+  // assert(true) -- should pass because p.0 != 0 holds for 1
+  call $r := assert_.i32(1);
+  // call assert_.i32_with_req(1) — both `1 != 0` and `1 > -1` hold
+  call $r := assert_.i32_with_req(1);
+  return;
+}
diff --git a/Tools/BoogieToStrata/Tests/TypeSynonymChain.bpl b/Tools/BoogieToStrata/Tests/TypeSynonymChain.bpl
new file mode 100644
index 0000000000..cc5811b580
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/TypeSynonymChain.bpl
@@ -0,0 +1,20 @@
+// Regression test for multi-level type synonym resolution.
+// dealiasTypeExpr must recurse through: ref → i64 → int
+// Without recursive resolution, comparison and arithmetic on `ref`
+// trigger a panic because the type stays as a synonym instead of
+// resolving to the base `int` type.
+
+type i64 = int;
+type ref = i64;
+
+procedure main() returns (r: ref)
+ensures r >= 0;
+{
+  var a: ref;
+  var b: ref;
+  a := 3;
+  b := a + 4;
+  assert b == 7;
+  assert a <= b;
+  r := b;
+}
diff --git a/Tools/BoogieToStrata/Tests/TypeSynonymChain.expect b/Tools/BoogieToStrata/Tests/TypeSynonymChain.expect
new file mode 100644
index 0000000000..197fd783cb
--- /dev/null
+++ b/Tools/BoogieToStrata/Tests/TypeSynonymChain.expect
@@ -0,0 +1,5 @@
+Successfully parsed.
+TypeSynonymChain.core.st(22, 4) [assert_0]: ✅ pass
+TypeSynonymChain.core.st(23, 4) [assert_1]: ✅ pass
+TypeSynonymChain.core.st(14, 2) [main_ensures_0]: ✅ pass
+All 3 goals passed.