diff --git a/src/main.rs b/src/main.rs
index 3a8a8291..b577a37b 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -207,9 +207,18 @@ fn main() {
     }
 
     let t = Instant::now();
-    pass::check::check(&mut diags, &mut combined_tu, "elab", true);
+    pass::normalize_casts::normalize_casts(&mut combined_tu);
     if cli.time_passes {
-        eprintln!("  check (post-elab): {:.3}s", t.elapsed().as_secs_f64());
+        eprintln!("  normalize_casts: {:.3}s", t.elapsed().as_secs_f64());
+    }
+
+    let t = Instant::now();
+    pass::check::check(&mut diags, &mut combined_tu, "normalize_casts", true);
+    if cli.time_passes {
+        eprintln!(
+            "  check (post-normalize_casts): {:.3}s",
+            t.elapsed().as_secs_f64()
+        );
     }
 
     let t = Instant::now();
diff --git a/src/pass/emit.rs b/src/pass/emit.rs
index c12737a4..8df18e1d 100644
--- a/src/pass/emit.rs
+++ b/src/pass/emit.rs
@@ -14,20 +14,9 @@ use crate::{
     mayberc::MaybeRc,
 };
 
-pub type SourceRangeMap = Vec<(Location, Range)>;
+use super::normalize_casts::normalize_unsigned;
 
-/// Normalize a possibly-negative integer literal into the unsigned range
-/// [0, 2^width).
-///
-/// clang hands us the signed interpretation of an N-bit bit pattern (see
-/// `toBigInt` in `cpp/impl.cpp`, which uses `toStringSigned`), so an unsigned
-/// literal with the high bit set arrives as a negative `BigInt` (e.g. the u32
-/// value 0xFFFFFFFF as -1). F* unsigned literals must be non-negative, so we
-/// reduce the value modulo 2^width before emitting it.
-fn normalize_unsigned(val: &BigInt, width: u32) -> BigInt {
-    let modulus = BigInt::from(1u32) << width;
-    ((val % &modulus) + &modulus) % &modulus
-}
+pub type SourceRangeMap = Vec<(Location, Range)>;
 
 /// The module holding a function's fnptr wrapper (`func_<g>__fp`), whose type
 /// carries the inlined pre/post spec. Kept separate from the function's own
@@ -316,6 +305,82 @@ fn annotated<T>(ast: &Ast<T>, doc: impl FnOnce() -> Doc) -> Doc {
     doc().annotate(ast.loc.clone())
 }
 
+/// Render an integer literal for use as a function argument. F* lexes a leading
+/// `-` as the infix subtraction operator, so `Int16.int_to_t -1` parses as
+/// `Int16.int_to_t - 1`; negative values must be parenthesized.
+fn paren_if_negative(val: &BigInt) -> String {
+    if val.sign() == num_bigint::Sign::Minus {
+        format!("({})", val)
+    } else {
+        format!("{}", val)
+    }
+}
+
+/// Render a suffixed literal such as `-1l`. A leading `-` also has to be
+/// parenthesized: F* lexes `=-` and `:=-` as single operators, so a negative
+/// literal in a record field or an assignment would otherwise not parse.
+/// The F* literal for a C machine-integer constant, if the type has a literal
+/// suffix. Emitting `62586880L` rather than `Int64.int_to_t 62586880` is not
+/// only shorter: the constructor's argument carries the refinement
+/// `FStar.Int.size 62586880 64`, which only the SMT solver discharges. That
+/// makes a constructor application ill-typed wherever the checker runs without
+/// SMT -- notably while Pulse searches for a witness to an existential, where
+/// a constant of this shape appears as a candidate.
+fn machine_int_literal(val: &BigInt, ty: &TypeT) -> Option<String> {
+    let (suffix, unsigned_width) = match ty {
+        TypeT::Int {
+            signed: true,
+            width: 8,
+        } => ("y", None),
+        TypeT::Int {
+            signed: false,
+            width: 8,
+        } => ("uy", Some(8)),
+        TypeT::Int {
+            signed: true,
+            width: 16,
+        } => ("s", None),
+        TypeT::Int {
+            signed: false,
+            width: 16,
+        } => ("us", Some(16)),
+        TypeT::Int {
+            signed: true,
+            width: 32,
+        } => ("l", None),
+        TypeT::Int {
+            signed: false,
+            width: 32,
+        } => ("ul", Some(32)),
+        TypeT::Int {
+            signed: true,
+            width: 64,
+        } => ("L", None),
+        TypeT::Int {
+            signed: false,
+            width: 64,
+        } => ("uL", Some(64)),
+        TypeT::SizeT => ("sz", None),
+        _ => return None,
+    };
+    match unsigned_width {
+        // clang hands us the signed interpretation of the bit pattern (see
+        // toBigInt in cpp/impl.cpp), so an unsigned literal with the high bit
+        // set arrives as a negative BigInt (e.g. 0xFFFFFFFF as -1). F*'s
+        // unsigned literals must lie in [0, 2^width), so normalize first.
+        Some(width) => Some(format!("{}{}", normalize_unsigned(val, width), suffix)),
+        None => Some(suffixed_literal(val, suffix)),
+    }
+}
+
+fn suffixed_literal(val: &BigInt, suffix: &str) -> String {
+    if val.sign() == num_bigint::Sign::Minus {
+        format!("({}{})", val, suffix)
+    } else {
+        format!("{}{}", val, suffix)
+    }
+}
+
 fn parens(doc: Doc) -> Doc {
     Doc::text("(")
         .append(doc)
@@ -2376,42 +2441,7 @@ impl<'a> Emitter<'a> {
     fn emit_pattern(&mut self, env: &Env, pattern: &Expr) -> Doc {
         if let ExprT::IntLit(val, ty) = &pattern.val {
             let resolved = env.vtype_whnf(ty.clone().into());
-            let literal = match resolved.val {
-                TypeT::Int {
-                    signed: true,
-                    width: 8,
-                } => Some(format!("{}y", val)),
-                TypeT::Int {
-                    signed: false,
-                    width: 8,
-                } => Some(format!("{}uy", normalize_unsigned(val, 8))),
-                TypeT::Int {
-                    signed: true,
-                    width: 16,
-                } => Some(format!("{}s", val)),
-                TypeT::Int {
-                    signed: false,
-                    width: 16,
-                } => Some(format!("{}us", normalize_unsigned(val, 16))),
-                TypeT::Int {
-                    signed: true,
-                    width: 32,
-                } => Some(format!("{}l", val)),
-                TypeT::Int {
-                    signed: false,
-                    width: 32,
-                } => Some(format!("{}ul", normalize_unsigned(val, 32))),
-                TypeT::Int {
-                    signed: true,
-                    width: 64,
-                } => Some(format!("{}L", val)),
-                TypeT::Int {
-                    signed: false,
-                    width: 64,
-                } => Some(format!("{}uL", normalize_unsigned(val, 64))),
-                TypeT::SizeT => Some(format!("{}sz", val)),
-                _ => None,
-            };
+            let literal = machine_int_literal(val, &resolved.val);
             if let Some(literal) = literal {
                 return Doc::text(literal);
             }
@@ -2425,26 +2455,22 @@ impl<'a> Emitter<'a> {
                 ExprT::BoolLit(v) => Doc::text(if *v { "true" } else { "false" }),
                 ExprT::IntLit(val, ty) => {
                     let resolved = env.vtype_whnf(ty.clone().into());
+                    if let Some(literal) = machine_int_literal(val, &resolved.val) {
+                        return Doc::text(literal);
+                    }
                     match resolved.val {
+                        // Widths without an F* literal suffix keep the
+                        // constructor form; they do not occur in practice.
                         TypeT::Int {
                             signed: true,
-                            width: 32,
-                        } => Doc::text(format!("{}l", val)),
-                        TypeT::Int {
-                            signed: false,
-                            width: 32,
-                        } => {
-                            // clang hands us the signed interpretation of the
-                            // bit pattern (see toBigInt in cpp/impl.cpp), so a
-                            // u32 literal with the high bit set arrives as a
-                            // negative BigInt (e.g. 0xFFFFFFFF as -1). F*'s `ul`
-                            // literals must lie in [0, 2^32), so normalize first.
-                            Doc::text(format!("{}ul", normalize_unsigned(val, 32)))
-                        }
-                        TypeT::Int {
-                            signed: true,
                             width,
-                        } => Doc::text(format!("(Int{}.int_to_t {})", width, val)),
+                        } => Doc::text(format!(
+                            // A bare negative argument would be parsed as
+                            // subtraction (`int_to_t - 1`), so parenthesize it.
+                            "(Int{}.int_to_t {})",
+                            width,
+                            paren_if_negative(val)
+                        )),
                         TypeT::Int {
                             signed: false,
                             width,
@@ -2453,8 +2479,7 @@ impl<'a> Emitter<'a> {
                             width,
                             normalize_unsigned(val, width)
                         )),
-                        TypeT::SizeT => Doc::text(format!("{}sz", val)),
-                        TypeT::SpecInt | TypeT::SpecNat => Doc::text(format!("{}", val)),
+                        TypeT::SpecInt | TypeT::SpecNat => Doc::text(suffixed_literal(val, "")),
                         TypeT::Pointer(_, PointerKind::Ref | PointerKind::Unknown)
                             if **val == BigInt::ZERO =>
                         {
@@ -2537,6 +2562,7 @@ impl<'a> Emitter<'a> {
                         // Same underlying type, no cast necessary.
                         return val_doc;
                     }
+
                     let default_msg = format!("unsupported cast from {} to {}", from_ty, to_ty);
                     match (&from_ty.val, &to_ty.val) {
                         (TypeT::Bool, TypeT::Int { signed, width }) => {
diff --git a/src/pass/mod.rs b/src/pass/mod.rs
index 683f9841..bafe9034 100644
--- a/src/pass/mod.rs
+++ b/src/pass/mod.rs
@@ -4,5 +4,6 @@ pub mod elab;
 pub mod elim_cis;
 pub mod emit;
 pub mod merge;
+pub mod normalize_casts;
 pub mod prune;
 pub mod restructure_goto;
diff --git a/src/pass/normalize_casts.rs b/src/pass/normalize_casts.rs
new file mode 100644
index 00000000..ae4699c1
--- /dev/null
+++ b/src/pass/normalize_casts.rs
@@ -0,0 +1,369 @@
+//! Normalize out-of-range casts of integer literals before emission.
+//!
+//! C defines conversion to unsigned integers modulo 2^N. Conversion to a
+//! signed type is implementation-defined when the value is not representable;
+//! PAL consistently models it using the target-width two's-complement value.
+
+use std::rc::Rc;
+
+use num_bigint::BigInt;
+
+use crate::{env::Env, ir::*};
+
+/// Recover the mathematical unsigned value of an N-bit clang integer literal.
+///
+/// `toBigInt` in `cpp/impl.cpp` uses clang's signed rendering, so a high-bit
+/// unsigned value can enter the IR as a negative `BigInt`.
+pub(super) fn normalize_unsigned(value: &BigInt, width: u32) -> BigInt {
+    let modulus = BigInt::from(1u32) << width;
+    ((value % &modulus) + &modulus) % &modulus
+}
+
+fn normalize_signed(value: &BigInt, width: u32) -> BigInt {
+    let modulus = BigInt::from(1u32) << width;
+    let sign_bit = BigInt::from(1u32) << (width - 1);
+    let unsigned = normalize_unsigned(value, width);
+    if unsigned >= sign_bit {
+        unsigned - modulus
+    } else {
+        unsigned
+    }
+}
+
+fn integer_fits(value: &BigInt, signed: bool, width: u32) -> bool {
+    if signed {
+        let upper_exclusive = BigInt::from(1u32) << (width - 1);
+        let lower_inclusive = -upper_exclusive.clone();
+        value >= &lower_inclusive && value < &upper_exclusive
+    } else {
+        value >= &BigInt::ZERO && value < &(BigInt::from(1u32) << width)
+    }
+}
+
+fn normalize_type(env: &Env, ty: &mut Rc<Type>) {
+    match &mut Rc::make_mut(ty).val {
+        TypeT::Pointer(inner, _)
+        | TypeT::FixedArray(inner, _)
+        | TypeT::FlexArray(inner)
+        | TypeT::Plain(inner)
+        | TypeT::Nullable(inner) => normalize_type(env, inner),
+        TypeT::FnPtr { args, ret } => {
+            for arg in args {
+                normalize_type(env, arg);
+            }
+            normalize_type(env, ret);
+        }
+        TypeT::Refine(inner, pred)
+        | TypeT::RefineAlways(inner, pred)
+        | TypeT::RefineUninit(inner, pred) => {
+            normalize_type(env, inner);
+            normalize_expr(env, Rc::make_mut(pred));
+        }
+        TypeT::RefineValue(inner, _, binding_ty, pred) => {
+            normalize_type(env, inner);
+            normalize_type(env, binding_ty);
+            normalize_expr(env, Rc::make_mut(pred));
+        }
+        TypeT::Void
+        | TypeT::Bool
+        | TypeT::Int { .. }
+        | TypeT::Float { .. }
+        | TypeT::SizeT
+        | TypeT::PtrdiffT
+        | TypeT::SpecInt
+        | TypeT::SpecNat
+        | TypeT::SLProp
+        | TypeT::TypeRef(_)
+        | TypeT::Unknown
+        | TypeT::Error => {}
+    }
+}
+
+fn normalize_inline_pulse(env: &Env, code: &mut InlinePulseCode) {
+    for token in &mut code.tokens {
+        match token {
+            InlinePulseToken::RValueAntiquot { expr, .. }
+            | InlinePulseToken::LValueAntiquot { expr, .. } => {
+                normalize_expr(env, Rc::make_mut(expr));
+            }
+            InlinePulseToken::TypeAntiquot { ty, .. }
+            | InlinePulseToken::FieldAntiquot { ty, .. }
+            | InlinePulseToken::AuxFnAntiquot { ty, .. }
+            | InlinePulseToken::Declare { ty, .. } => normalize_type(env, ty),
+            InlinePulseToken::Verbatim(_) => {}
+        }
+    }
+}
+
+fn normalize_exprs(env: &Env, exprs: &mut Exprs) {
+    for expr in exprs {
+        normalize_expr(env, Rc::make_mut(expr));
+    }
+}
+
+fn normalize_expr(env: &Env, expr: &mut Expr) {
+    match &mut expr.val {
+        ExprT::IntLit(_, ty)
+        | ExprT::FloatLit(_, ty)
+        | ExprT::Malloc(ty)
+        | ExprT::Calloc(ty)
+        | ExprT::SizeOf(ty)
+        | ExprT::AlignOf(ty)
+        | ExprT::Error(ty) => normalize_type(env, ty),
+        ExprT::InlinePulse(code, ty) => {
+            normalize_inline_pulse(env, Rc::make_mut(code));
+            normalize_type(env, ty);
+        }
+        ExprT::Cast(value, ty)
+        | ExprT::MallocArray(ty, value)
+        | ExprT::CallocArray(ty, value)
+        | ExprT::MallocFlex(ty, value)
+        | ExprT::CallocFlex(ty, value)
+        | ExprT::MemsetZero(ty, value) => {
+            normalize_expr(env, Rc::make_mut(value));
+            normalize_type(env, ty);
+        }
+        ExprT::ContainerOf(value, ty, _) => {
+            normalize_expr(env, Rc::make_mut(value));
+            normalize_type(env, ty);
+        }
+        ExprT::Forall(_, ty, body) | ExprT::Exists(_, ty, body) => {
+            normalize_type(env, ty);
+            normalize_expr(env, Rc::make_mut(body));
+        }
+        ExprT::ArrayInit { elem_ty, elems, .. } => {
+            normalize_type(env, elem_ty);
+            normalize_exprs(env, elems);
+        }
+        ExprT::Memset(ty, dest, value, count) => {
+            normalize_type(env, ty);
+            normalize_expr(env, Rc::make_mut(dest));
+            normalize_expr(env, Rc::make_mut(value));
+            normalize_expr(env, Rc::make_mut(count));
+        }
+        ExprT::Deref(value)
+        | ExprT::Member(value, _)
+        | ExprT::VAttr(_, value)
+        | ExprT::Ref(value)
+        | ExprT::UnOp(_, value)
+        | ExprT::Live(value)
+        | ExprT::Old(value)
+        | ExprT::Free(value)
+        | ExprT::PreIncr(value)
+        | ExprT::PostIncr(value)
+        | ExprT::PreDecr(value)
+        | ExprT::PostDecr(value)
+        | ExprT::UnionInit(_, _, value) => normalize_expr(env, Rc::make_mut(value)),
+        ExprT::Index(left, right)
+        | ExprT::BinOp(_, left, right)
+        | ExprT::AssignExpr(left, right) => {
+            normalize_expr(env, Rc::make_mut(left));
+            normalize_expr(env, Rc::make_mut(right));
+        }
+        ExprT::Cond(cond, then_expr, else_expr) => {
+            normalize_expr(env, Rc::make_mut(cond));
+            normalize_expr(env, Rc::make_mut(then_expr));
+            normalize_expr(env, Rc::make_mut(else_expr));
+        }
+        ExprT::FnCall(_, args) => normalize_exprs(env, args),
+        ExprT::FnPtrCall(function, args) => {
+            normalize_expr(env, Rc::make_mut(function));
+            normalize_exprs(env, args);
+        }
+        ExprT::StructInit(_, fields) => {
+            for (_, value) in fields {
+                normalize_expr(env, Rc::make_mut(value));
+            }
+        }
+        ExprT::Var(_) | ExprT::FnRef(_) | ExprT::BoolLit(_) => {}
+    }
+
+    let replacement = match &expr.val {
+        ExprT::Cast(value, target_ty) => {
+            let ExprT::IntLit(value, source_ty) = &value.val else {
+                return;
+            };
+            let TypeT::Int {
+                signed: target_signed,
+                width: target_width,
+            } = env.vtype_whnf(target_ty.clone().into()).val
+            else {
+                return;
+            };
+            let source_value = match env.vtype_whnf(source_ty.clone().into()).val {
+                TypeT::Int {
+                    signed: false,
+                    width,
+                } => normalize_unsigned(value, width),
+                TypeT::Int { signed: true, .. } => value.as_ref().clone(),
+                _ => return,
+            };
+            // Fold the cast away even when the value is representable. The
+            // result is the same constant at the target type, and dropping the
+            // conversion matters for more than readability: `Int.Cast` applied
+            // to a literal reduces to a machine-integer constructor whose
+            // argument carries a refinement only the SMT solver discharges, so
+            // such a term is ill-typed wherever the checker runs without SMT --
+            // notably while Pulse searches for a witness to an existential.
+            let target_value = if integer_fits(&source_value, target_signed, target_width) {
+                source_value
+            } else if target_signed {
+                normalize_signed(&source_value, target_width)
+            } else {
+                normalize_unsigned(&source_value, target_width)
+            };
+            Some(ExprT::IntLit(Rc::new(target_value), target_ty.clone()))
+        }
+        _ => None,
+    };
+    if let Some(replacement) = replacement {
+        expr.val = replacement;
+    }
+}
+
+fn normalize_stmt(env: &Env, stmt: &mut Stmt) {
+    match &mut stmt.val {
+        StmtT::Call(expr) | StmtT::Assert(expr) | StmtT::Return(Some(expr)) => {
+            normalize_expr(env, Rc::make_mut(expr));
+        }
+        StmtT::Decl(_, ty) => normalize_type(env, ty),
+        StmtT::Let(_, ty, value) => {
+            normalize_type(env, ty);
+            normalize_expr(env, Rc::make_mut(value));
+        }
+        StmtT::DeclStackArray {
+            elem_type, size, ..
+        } => {
+            normalize_type(env, elem_type);
+            normalize_expr(env, Rc::make_mut(size));
+        }
+        StmtT::Assign(left, right) => {
+            normalize_expr(env, Rc::make_mut(left));
+            normalize_expr(env, Rc::make_mut(right));
+        }
+        StmtT::If {
+            cond,
+            then_branch,
+            else_branch,
+            ensures,
+        } => {
+            normalize_expr(env, Rc::make_mut(cond));
+            normalize_stmts(env, Rc::make_mut(then_branch));
+            normalize_stmts(env, Rc::make_mut(else_branch));
+            normalize_exprs(env, Rc::make_mut(ensures));
+        }
+        StmtT::Match {
+            scrutinee,
+            branches,
+            default_branch,
+            ensures,
+        } => {
+            normalize_expr(env, Rc::make_mut(scrutinee));
+            for branch in Rc::make_mut(branches) {
+                let branch = Rc::make_mut(branch);
+                normalize_exprs(env, Rc::make_mut(&mut branch.patterns));
+                normalize_stmts(env, Rc::make_mut(&mut branch.body));
+            }
+            normalize_stmts(env, Rc::make_mut(default_branch));
+            normalize_exprs(env, Rc::make_mut(ensures));
+        }
+        StmtT::While {
+            cond,
+            inv,
+            requires,
+            ensures,
+            body,
+        } => {
+            normalize_expr(env, Rc::make_mut(cond));
+            normalize_exprs(env, Rc::make_mut(inv));
+            normalize_exprs(env, Rc::make_mut(requires));
+            normalize_exprs(env, Rc::make_mut(ensures));
+            normalize_stmts(env, Rc::make_mut(body));
+        }
+        StmtT::GhostStmt(code) => normalize_inline_pulse(env, Rc::make_mut(code)),
+        StmtT::Label { ensures, .. } => normalize_exprs(env, Rc::make_mut(ensures)),
+        StmtT::GotoBlock { body, ensures, .. } => {
+            normalize_stmts(env, Rc::make_mut(body));
+            normalize_exprs(env, Rc::make_mut(ensures));
+        }
+        StmtT::Break | StmtT::Continue | StmtT::Return(None) | StmtT::Goto(_) | StmtT::Error => {}
+    }
+}
+
+fn normalize_stmts(env: &Env, stmts: &mut Stmts) {
+    for stmt in stmts {
+        normalize_stmt(env, Rc::make_mut(stmt));
+    }
+}
+
+fn normalize_fn_decl(env: &Env, decl: &mut FnDecl) {
+    normalize_type(env, &mut decl.ret_type);
+    for arg in &mut decl.args {
+        normalize_type(env, &mut arg.ty);
+    }
+    for arg in &mut decl.ghost_args {
+        normalize_type(env, &mut arg.ty);
+    }
+    normalize_exprs(env, &mut decl.requires);
+    normalize_exprs(env, &mut decl.ensures);
+    if let Some(decreases) = &mut decl.decreases {
+        normalize_expr(env, Rc::make_mut(decreases));
+    }
+}
+
+fn normalize_decl(env: &Env, decl: &mut Decl) {
+    match &mut decl.val {
+        DeclT::FnDefn(definition) => {
+            normalize_fn_decl(env, &mut definition.decl);
+            normalize_stmts(env, &mut definition.body);
+        }
+        DeclT::FnDecl(decl) => normalize_fn_decl(env, decl),
+        DeclT::Typedef(definition) => normalize_type(env, &mut definition.body),
+        DeclT::StructDefn(definition) => {
+            for field in &mut definition.fields {
+                match &mut field.val {
+                    FieldT::Plain { ty, .. } | FieldT::BitField { ty, .. } => {
+                        normalize_type(env, ty);
+                    }
+                }
+            }
+        }
+        DeclT::UnionDefn(definition) => {
+            for field in &mut definition.fields {
+                match &mut field.val {
+                    FieldT::Plain { ty, .. } | FieldT::BitField { ty, .. } => {
+                        normalize_type(env, ty);
+                    }
+                }
+            }
+        }
+        DeclT::IncludeDecl(include) => normalize_inline_pulse(env, &mut include.code),
+        DeclT::LetDecl(decl) => {
+            normalize_type(env, &mut decl.ret_type);
+            for param in &mut decl.params {
+                normalize_type(env, &mut param.ty);
+            }
+            normalize_exprs(env, &mut decl.requires);
+            normalize_exprs(env, &mut decl.ensures);
+            normalize_expr(env, Rc::make_mut(&mut decl.body));
+        }
+        DeclT::OpaqueTypeDecl(decl) => normalize_inline_pulse(env, &mut decl.code),
+        DeclT::GlobalVar(global) => {
+            normalize_type(env, &mut global.ty);
+            if let Some(init) = &mut global.init {
+                normalize_expr(env, Rc::make_mut(init));
+            }
+        }
+        DeclT::StructDecl(_) => {}
+    }
+}
+
+pub fn normalize_casts(tu: &mut TranslationUnit) {
+    let mut env = Env::new();
+    for decl in &tu.decls {
+        env.push_decl(decl);
+    }
+    for decl in &mut tu.decls {
+        normalize_decl(&env, decl);
+    }
+}
diff --git a/test/integer_literal_casts/Makefile b/test/integer_literal_casts/Makefile
new file mode 120000
index 00000000..3febeb16
--- /dev/null
+++ b/test/integer_literal_casts/Makefile
@@ -0,0 +1 @@
+../_templates/Makefile
\ No newline at end of file
diff --git a/test/integer_literal_casts/fstar.fst.config.json b/test/integer_literal_casts/fstar.fst.config.json
new file mode 120000
index 00000000..4100b019
--- /dev/null
+++ b/test/integer_literal_casts/fstar.fst.config.json
@@ -0,0 +1 @@
+../_templates/fstar.fst.config.json
\ No newline at end of file
diff --git a/test/integer_literal_casts/integer_literal_casts.c b/test/integer_literal_casts/integer_literal_casts.c
new file mode 100644
index 00000000..344c464a
--- /dev/null
+++ b/test/integer_literal_casts/integer_literal_casts.c
@@ -0,0 +1,82 @@
+#include "pal.h"
+#include <stdint.h>
+
+int8_t cast_literal_to_int8(void)
+    _ensures(return == -1)
+{
+    return (int8_t)255;
+}
+
+uint8_t cast_literal_to_uint8(void)
+    _ensures(return == UINT8_MAX)
+{
+    return (uint8_t)511;
+}
+
+int16_t cast_literal_to_int16(void)
+    _ensures(return == -1)
+{
+    return (int16_t)65535;
+}
+
+uint16_t cast_literal_to_uint16(void)
+    _ensures(return == UINT16_MAX)
+{
+    return (uint16_t)131071;
+}
+
+#define GENERATED_CODE_FIRST ((int32_t)0x80010001L)
+#define GENERATED_CODE_SECOND ((int32_t)0x80010002L)
+#define GENERATED_CODE_LIST \
+    X(GENERATED_CODE_FIRST) \
+    X(GENERATED_CODE_SECOND)
+
+uint8_t is_direct_code(int32_t code)
+{
+    switch (code)
+    {
+    case (int32_t)0x80010001L:
+    case (int32_t)0x80010002L:
+        return 1;
+    default:
+        return 0;
+    }
+}
+
+uint8_t is_generated_code(int32_t code)
+{
+    switch (code)
+    {
+#define X(CODE) \
+    case CODE:
+        GENERATED_CODE_LIST
+#undef X
+        return 1;
+    default:
+        return 0;
+    }
+}
+
+uint32_t cast_literal_to_uint32(void)
+    _ensures(return == 1)
+{
+    return (uint32_t)4294967297ULL;
+}
+
+int64_t cast_literal_to_int64(void)
+    _ensures(return == -1)
+{
+    return (int64_t)UINT64_MAX;
+}
+
+uint64_t uint64_max_literal(void)
+    _ensures(return == UINT64_MAX)
+{
+    return UINT64_MAX;
+}
+
+uint64_t preserve_representable_uint64_cast(void)
+    _ensures(return == INT64_MAX)
+{
+    return (uint64_t)INT64_MAX;
+}
diff --git a/test/integer_literal_casts/pal.config.json b/test/integer_literal_casts/pal.config.json
new file mode 120000
index 00000000..d59f1cfa
--- /dev/null
+++ b/test/integer_literal_casts/pal.config.json
@@ -0,0 +1 @@
+../_templates/pal.config.json
\ No newline at end of file
diff --git a/test/integer_literal_casts/pal.h b/test/integer_literal_casts/pal.h
new file mode 120000
index 00000000..05ef83f9
--- /dev/null
+++ b/test/integer_literal_casts/pal.h
@@ -0,0 +1 @@
+../pal.h
\ No newline at end of file
diff --git a/test/negative_literals/negative_literals.c b/test/negative_literals/negative_literals.c
index 03222e1c..7e8aeb14 100644
--- a/test/negative_literals/negative_literals.c
+++ b/test/negative_literals/negative_literals.c
@@ -1,7 +1,23 @@
 #include "pal.h"
 
+#include <stdint.h>
+
+typedef struct _RECORD
+{
+    int32_t Code;
+    uint32_t Info;
+} RECORD;
+
 int test_negative_literal() {
     int x = -10;
     int y = -100;
     return x + y;
 }
+
+// A negative literal in a record field or an assignment must be parenthesized:
+// F* lexes `=-` and `:=-` as single operators.
+RECORD test_negative_literal_field(void) {
+    RECORD record = {.Code = -2084828230L, .Info = 0};
+    record.Code = -1;
+    return record;
+}