diff --git a/Examples/NondetCond.core.st b/Examples/NondetCond.core.st
new file mode 100644
index 000000000..ee138ac03
--- /dev/null
+++ b/Examples/NondetCond.core.st
@@ -0,0 +1,14 @@
+// Test non-deterministic conditions in if and while statements
+procedure nondet_if()
+  modifies x;
+  ensures x >= 0;
+{
+  var x : int;
+  x := 0;
+  if (*) {
+    x := 1;
+  } else {
+    x := 2;
+  }
+  assert x >= 0;
+}
diff --git a/Strata/Backends/CBMC/CollectSymbols.lean b/Strata/Backends/CBMC/CollectSymbols.lean
index 6ee785215..b00e46754 100644
--- a/Strata/Backends/CBMC/CollectSymbols.lean
+++ b/Strata/Backends/CBMC/CollectSymbols.lean
@@ -125,11 +125,11 @@ private def collectGlobalSymbols (pgm : Core.Program) :
       let gty ← Lambda.LMonoTy.toGotoType ty.toMonoTypeUnsafe
       let tyJson := CProverGOTO.tyToJson gty
       let valueJson ← match e with
-        | some expr =>
+        | .det expr =>
           let gotoExpr ← Lambda.LExpr.toGotoExprCtx
             (TBase := ⟨Core.ExpressionMetadata, Unit⟩) [] expr
           (CProverGOTO.exprToJson gotoExpr).mapError (fun e => f!"{e}")
-        | none => pure (Lean.Json.mkObj [("id", "nil")])
+        | .nondet => pure (Lean.Json.mkObj [("id", "nil")])
       syms := syms ++ [(gname, {
         baseName := gname
         isLvalue := true
diff --git a/Strata/Backends/CBMC/CoreToCBMC.lean b/Strata/Backends/CBMC/CoreToCBMC.lean
index 987c190b7..721fa6384 100644
--- a/Strata/Backends/CBMC/CoreToCBMC.lean
+++ b/Strata/Backends/CBMC/CoreToCBMC.lean
@@ -99,7 +99,7 @@ def cmdToJson (e : Core.Command) (loc: SourceLoc) : Except String Json :=
       ])
     | .set ("ret") _ _ =>
       returnStmt loc.functionName
-    | .set name expr _ => do
+    | .set name (.det expr) _ => do
       let exprLoc : SourceLoc := { functionName := loc.functionName, lineNum := "6" }
       return (mkCodeBlock "expression" "6" loc.functionName #[
         mkSideEffect "assign" "6" loc.functionName mkIntType #[
@@ -165,7 +165,7 @@ def cmdToJson (e : Core.Command) (loc: SourceLoc) : Except String Json :=
     | .cover _ _ md =>
        throw s!"{Imperative.MetaData.formatFileRangeD md}\
                   cover unimplemented"
-    | .havoc _ md =>
+    | .set _ .nondet md =>
        throw s!"{Imperative.MetaData.formatFileRangeD md}\
                   havoc unimplemented"
 
@@ -188,7 +188,7 @@ def stmtToJson {P : Imperative.PureExpr} (I : Lambda.LExprParams) [IdentToStr (L
   (e : Imperative.Stmt P Command) (loc: SourceLoc) : Except String Json :=
   match e with
   | .cmd cmd => cmdToJson cmd loc
-  | .ite cond thenb elseb _ => do
+  | .ite (.det cond) thenb elseb _ => do
     let converted_cond : Lambda.LExpr I.mono := @HasLExpr.expr_eq P (I:=I) _ ▸ cond
     return Json.mkObj [
       ("id", "code"),
diff --git a/Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean b/Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean
index 500397e0d..26d0a86ff 100644
--- a/Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean
+++ b/Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean
@@ -117,14 +117,10 @@ def Core.Cmd.renameVars (frto : Map String String) (c : Imperative.Cmd Core.Expr
     let new := name_alt.getD (Core.CoreIdent.toPretty name)
     .init new ty e' (convertMetaData md)
   | .set name e md =>
-    let e' := substVarNames e frto
+    let e' := e.map (substVarNames · frto)
     let name_alt := frto.find? (Core.CoreIdent.toPretty name)
     let new := name_alt.getD (Core.CoreIdent.toPretty name)
     .set new e' (convertMetaData md)
-  | .havoc name md =>
-    let name_alt := frto.find? (Core.CoreIdent.toPretty name)
-    let new := name_alt.getD (Core.CoreIdent.toPretty name)
-    .havoc new (convertMetaData md)
   | .assume label e md =>
     let e' := substVarNames e frto
     .assume label e' (convertMetaData md)
diff --git a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean
index 4baf59ef6..0c4236070 100644
--- a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean
+++ b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean
@@ -61,8 +61,7 @@ private def renameCmd
     (rn : Std.HashMap String String)
     : Imperative.Cmd Core.Expression → Imperative.Cmd Core.Expression
   | .init name ty e md => .init (renameIdent rn name) ty (e.map (renameExpr rn)) md
-  | .set name e md => .set (renameIdent rn name) (renameExpr rn e) md
-  | .havoc name md => .havoc (renameIdent rn name) md
+  | .set name e md => .set (renameIdent rn name) (e.map (renameExpr rn)) md
   | .assert l e md => .assert l (renameExpr rn e) md
   | .assume l e md => .assume l (renameExpr rn e) md
   | .cover l e md => .cover l (renameExpr rn e) md
@@ -79,10 +78,16 @@ private partial def unwrapCmdExt
   | .ite c t e md => do
     let t' ← t.mapM (unwrapCmdExt rn)
     let e' ← e.mapM (unwrapCmdExt rn)
-    .ok (.ite (renameExpr rn c) t' e' md)
+    let c' := match c with
+      | .det expr => Imperative.ExprOrNondet.det (renameExpr rn expr)
+      | .nondet => .nondet
+    .ok (.ite c' t' e' md)
   | .loop g m i body md => do
     let body' ← body.mapM (unwrapCmdExt rn)
-    .ok (.loop (renameExpr rn g) (m.map (renameExpr rn)) (i.map (renameExpr rn)) body' md)
+    let g' := match g with
+      | .det expr => Imperative.ExprOrNondet.det (renameExpr rn expr)
+      | .nondet => .nondet
+    .ok (.loop g' (m.map (renameExpr rn)) (i.map (renameExpr rn)) body' md)
   | .exit l md => .ok (.exit l md)
   | .funcDecl _d _md =>
     .error f!"[unwrapCmdExt] Unexpected funcDecl; should have been lifted by collectFuncDecls."
@@ -186,7 +191,9 @@ private partial def coreStmtsToGoto
       | .ite cond thenb elseb md =>
         if hasCallStmt thenb || hasCallStmt elseb then
           let srcLoc := Imperative.metadataToSourceLoc md pname trans.sourceText
-          let cond_expr ← toExpr (renameExpr rn cond)
+          let cond_expr ← match cond with
+            | .det e => toExpr (renameExpr rn e)
+            | .nondet => pure { id := .side_effect .Nondet, type := .Boolean, operands := [] : CProverGOTO.Expr }
           let (trans, goto_else_idx) :=
             Imperative.emitCondGoto (CProverGOTO.Expr.not cond_expr) srcLoc trans
           let trans ← coreStmtsToGoto Env pname rn thenb trans
@@ -206,7 +213,9 @@ private partial def coreStmtsToGoto
           let srcLoc := Imperative.metadataToSourceLoc md pname trans.sourceText
           let loop_head := trans.nextLoc
           let trans := Imperative.emitLabel s!"loop_{loop_head}" srcLoc trans
-          let guard_expr ← toExpr (renameExpr rn guard)
+          let guard_expr ← match guard with
+            | .det e => toExpr (renameExpr rn e)
+            | .nondet => pure { id := .side_effect .Nondet, type := .Boolean, operands := [] : CProverGOTO.Expr }
           let (trans, goto_end_idx) :=
             Imperative.emitCondGoto (CProverGOTO.Expr.not guard_expr) srcLoc trans
           let trans ← coreStmtsToGoto Env pname rn body trans
diff --git a/Strata/Backends/CBMC/StrataToCBMC.lean b/Strata/Backends/CBMC/StrataToCBMC.lean
index 2e31266f9..247b06d4e 100644
--- a/Strata/Backends/CBMC/StrataToCBMC.lean
+++ b/Strata/Backends/CBMC/StrataToCBMC.lean
@@ -224,7 +224,7 @@ def cmdToJson (e : Strata.C_Simp.Command) (loc: SourceLoc) : Except String Json
       ]
     ])
   | .set ("return") _ _ => returnStmt loc.functionName
-  | .set name expr _ =>
+  | .set name (.det expr) _ =>
     let exprLoc : SourceLoc := { functionName := loc.functionName, lineNum := "6" }
     return (mkCodeBlock "expression" "6" loc.functionName (config := cfg) #[
       mkSideEffect "assign" "6" loc.functionName (mkIntType cfg) (config := cfg) #[
@@ -287,7 +287,7 @@ def cmdToJson (e : Strata.C_Simp.Command) (loc: SourceLoc) : Except String Json
         ]
       ]
     ])
-  | .havoc _ _ | .cover _ _ _ => throw "cmdToJson: Unimplemented"
+  | .set _ .nondet _ | .cover _ _ _ => throw "cmdToJson: Unimplemented"
 
 mutual
 def blockToJson (b: Imperative.Block Strata.C_Simp.Expression Strata.C_Simp.Command) (loc: SourceLoc) : Except String Json := do
@@ -307,7 +307,7 @@ def blockToJson (b: Imperative.Block Strata.C_Simp.Expression Strata.C_Simp.Comm
  def stmtToJson (e : Strata.C_Simp.Statement) (loc: SourceLoc) : Except String Json :=
   match e with
   | .cmd cmd => cmdToJson cmd loc
-  | .ite cond thenb elseb _ => do
+  | .ite (.det cond) thenb elseb _ => do
     return Json.mkObj [
       ("id", "code"),
       ("namedSub", Json.mkObj [
diff --git a/Strata/DL/Imperative/Cmd.lean b/Strata/DL/Imperative/Cmd.lean
index 59a75755e..df62a0b4c 100644
--- a/Strata/DL/Imperative/Cmd.lean
+++ b/Strata/DL/Imperative/Cmd.lean
@@ -24,6 +24,21 @@ programs. These constructs are parameterized by `PureExpr`, which can be
 instantiated with any language construct that does not have side-effects.
 -/
 
+/-! ## Deterministic or Non-deterministic Expressions
+
+`ExprOrNondet` represents a value that is either a deterministic expression or
+a non-deterministic (arbitrary) choice. This is used in commands where the
+right-hand side can be either a concrete expression or a havoc.
+-/
+
+/-- A value that is either a deterministic expression or a non-deterministic choice. -/
+inductive ExprOrNondet (P : PureExpr) where
+  /-- A deterministic expression. -/
+  | det (e : P.Expr)
+  /-- A non-deterministic (arbitrary) value. -/
+  | nondet
+  deriving Inhabited
+
 /-! ## Commands
 
 Commands form the core of the Imperative dialect. They include constructs for
@@ -37,13 +52,12 @@ Commands don't create local control flow, and are typically used as a parameter
 to `Imperative.Stmt` or other similar types.
 -/
 inductive Cmd (P : PureExpr) : Type where
-  /-- Define a variable called `name` with type `ty` and optional initial value `e`.
-      When `e` is `none`, the variable is initialized with an arbitrary value. -/
-  | init     (name : P.Ident) (ty : P.Ty) (e : Option P.Expr) (md : (MetaData P))
-  /-- Assign `e` to a pre-existing variable `name`. -/
-  | set      (name : P.Ident) (e : P.Expr) (md : (MetaData P))
-  /-- Assigns an arbitrary value to an existing variable `name`. -/
-  | havoc    (name : P.Ident) (md : (MetaData P))
+  /-- Define a variable called `name` with type `ty` and value `e`.
+      When `e` is `.nondet`, the variable is initialized with an arbitrary value. -/
+  | init     (name : P.Ident) (ty : P.Ty) (e : ExprOrNondet P) (md : (MetaData P))
+  /-- Assign `e` to a pre-existing variable `name`.
+      When `e` is `.nondet`, assigns an arbitrary value (havoc semantics). -/
+  | set      (name : P.Ident) (e : ExprOrNondet P) (md : (MetaData P))
   /-- Checks if condition `b` is true on _all_ paths on which this command is
     encountered. Reports an error if `b` does not hold on _any_ of these paths.
   -/
@@ -60,13 +74,13 @@ inductive Cmd (P : PureExpr) : Type where
 @[expose] abbrev Cmds (P : PureExpr) := List (Cmd P)
 
 instance [Inhabited P.Ident]: Inhabited (Cmd P) where
-  default := .havoc default default
+  default := .set default .nondet default
 
 ---------------------------------------------------------------------
 
 def Cmd.getMetaData (c : Cmd P) : MetaData P :=
   match c with
-  | .init _ _ _ md | .set _ _ md | .havoc _ md
+  | .init _ _ _ md | .set _ _ md
   | .assert _ _ md | .assume _ _ md | .cover _ _ md =>
    md
 
@@ -84,26 +98,34 @@ class HasHavoc (P : PureExpr) (CmdT : Type) where
   havoc : P.Ident → MetaData P → CmdT
 
 instance : HasHavoc P (Cmd P) where
-  havoc x md := .havoc x md
+  havoc x md := .set x .nondet md
 
-/-- Declare a variable with a given type and optional initial value. -/
+/-- Declare a variable with a given type and value (deterministic or non-deterministic). -/
 class HasInit (P : PureExpr) (CmdT : Type) where
-  init : P.Ident → P.Ty → Option P.Expr → MetaData P → CmdT
+  init : P.Ident → P.Ty → ExprOrNondet P → MetaData P → CmdT
 
 instance : HasInit P (Cmd P) where
   init x ty e md := .init x ty e md
 
 ---------------------------------------------------------------------
 
+/-- Get all variables accessed by an `ExprOrNondet`. -/
+def ExprOrNondet.getVars [HasVarsPure P P.Expr] (e : ExprOrNondet P) : List P.Ident :=
+  match e with
+  | .det e => HasVarsPure.getVars e
+  | .nondet => []
+
+/-- Map a function over the expression in an `ExprOrNondet`. -/
+def ExprOrNondet.map {P Q : PureExpr} (f : P.Expr → Q.Expr) : ExprOrNondet P → ExprOrNondet Q
+  | .det e => .det (f e)
+  | .nondet => .nondet
+
 mutual
 /-- Get all variables accessed by `c`. -/
 def Cmd.getVars [HasVarsPure P P.Expr] (c : Cmd P) : List P.Ident :=
   match c with
-  | .init _ _ eOpt _ => match eOpt with
-    | some e => HasVarsPure.getVars e
-    | none => []
-  | .set _ e _ => HasVarsPure.getVars e
-  | .havoc _ _ => []
+  | .init _ _ e _ => e.getVars
+  | .set _ e _ => e.getVars
   | .assert _ e _ => HasVarsPure.getVars e
   | .assume _ e _ => HasVarsPure.getVars e
   | .cover _ e _ => HasVarsPure.getVars e
@@ -142,7 +164,6 @@ def Cmd.modifiedVars (c : Cmd P) : List P.Ident :=
   match c with
   | .init _ _ _ _ => []
   | .set name _ _ => [name]
-  | .havoc name _ => [name]
   | .assert _ _ _ => []
   | .assume _ _ _ => []
   | .cover _ _ _ => []
@@ -168,13 +189,22 @@ instance (P : PureExpr) : HasVarsImp P (Cmds P) where
 
 open Std (ToFormat Format format)
 
+def formatExprOrNondet (P : PureExpr) (e : ExprOrNondet P)
+    [ToFormat P.Expr] : Format :=
+  match e with
+  | .det e => format e
+  | .nondet => f!"*"
+
+instance [ToFormat P.Expr] : ToFormat (ExprOrNondet P) where
+  format e := formatExprOrNondet P e
+
 def formatCmd (P : PureExpr) (c : Cmd P)
     [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty] : Format :=
   match c with
-  | .init name ty (some e) _md => f!"init ({name} : {ty}) := {e}"
-  | .init name ty none _md => f!"init ({name} : {ty})"
-  | .set name e _md => f!"{name} := {e}"
-  | .havoc name _md => f!"havoc {name}"
+  | .init name ty (.det e) _md => f!"init ({name} : {ty}) := {e}"
+  | .init name ty .nondet _md => f!"init ({name} : {ty})"
+  | .set name (.det e) _md => f!"{name} := {e}"
+  | .set name .nondet _md => f!"havoc {name}"
   | .assert label b _md => f!"assert [{label}] {b}"
   | .assume label b _md => f!"assume [{label}] {b}"
   | .cover label b _md => f!"cover [{label}] {b}"
diff --git a/Strata/DL/Imperative/CmdEval.lean b/Strata/DL/Imperative/CmdEval.lean
index 29b255a5e..5c4495f78 100644
--- a/Strata/DL/Imperative/CmdEval.lean
+++ b/Strata/DL/Imperative/CmdEval.lean
@@ -23,42 +23,43 @@ def Cmd.eval [BEq P.Ident] [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P 
   | some _ => (c, σ)
   | none =>
     match c with
-    | .init x ty eOpt md =>
+    | .init x ty e md =>
       match EC.lookup σ x with
       | none =>
-        match eOpt with
-        | some e =>
-          let (e, σ) := EC.preprocess σ c e
-          let e := EC.eval σ e
-          let σ := EC.update σ x ty e
-          let c' := .init x ty (some e) md
+        match e with
+        | .det expr =>
+          let (expr, σ) := EC.preprocess σ c expr
+          let expr := EC.eval σ expr
+          let σ := EC.update σ x ty expr
+          let c' := .init x ty (.det expr) md
           (c', σ)
-        | none =>
+        | .nondet =>
           -- Unconstrained initialization - generate a fresh value
-          let (e, σ) := EC.genFreeVar σ x ty
-          let σ := EC.update σ x ty e
-          let c' := .init x ty none md
+          let (expr, σ) := EC.genFreeVar σ x ty
+          let σ := EC.update σ x ty expr
+          let c' := .init x ty .nondet md
           (c', σ)
       | some (xv, xty) => (c, EC.updateError σ (.InitVarExists (x, xty) xv))
 
     | .set x e md =>
       match EC.lookup σ x with
-      | none => (c, EC.updateError σ (.AssignVarNotExists x e))
+      | none =>
+        match e with
+        | .det expr => (c, EC.updateError σ (.AssignVarNotExists x expr))
+        | .nondet => (c, EC.updateError σ (.HavocVarNotExists x))
       | some (_xv, xty) =>
-        let (e, σ) := EC.preprocess σ c e
-        let e := EC.eval σ e
-        let σ := EC.update σ x xty e
-        let c' := .set x e md
-        (c', σ)
-
-    | .havoc x md =>
-      match EC.lookup σ x with
-      | none => (c, EC.updateError σ (.HavocVarNotExists x))
-      | some (_, xty) =>
-        let (e, σ) := EC.genFreeVar σ x xty
-        let σ := EC.update σ x xty e
-        let c' := .havoc x (md.pushElem (.var x) (.expr e))
-        (c', σ)
+        match e with
+        | .det expr =>
+          let (expr, σ) := EC.preprocess σ c expr
+          let expr := EC.eval σ expr
+          let σ := EC.update σ x xty expr
+          let c' := .set x (.det expr) md
+          (c', σ)
+        | .nondet =>
+          let (expr, σ) := EC.genFreeVar σ x xty
+          let σ := EC.update σ x xty expr
+          let c' := .set x .nondet (md.pushElem (.var x) (.expr expr))
+          (c', σ)
 
     | .assert label e md =>
       let (e, σ) := EC.preprocess σ c e
diff --git a/Strata/DL/Imperative/CmdSemantics.lean b/Strata/DL/Imperative/CmdSemantics.lean
index 9afe463c1..ed6a4911c 100644
--- a/Strata/DL/Imperative/CmdSemantics.lean
+++ b/Strata/DL/Imperative/CmdSemantics.lean
@@ -282,14 +282,14 @@ inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
     InitState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ---
-    EvalCmd δ σ (.init x _ (some e) _) σ'
+    EvalCmd δ σ (.init x _ (.det e) _) σ'
 
   /-- Initialize `x` with an unconstrained value (havoc semantics). -/
   | eval_init_unconstrained :
     InitState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ---
-    EvalCmd δ σ (.init x _ none _) σ'
+    EvalCmd δ σ (.init x _ .nondet _) σ'
 
   /-- If `e` evaluates to a value `v`, assign `x` according to `UpdateState`. -/
   | eval_set :
@@ -297,14 +297,14 @@ inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
     UpdateState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ----
-    EvalCmd δ σ (.set x e _) σ'
+    EvalCmd δ σ (.set x (.det e) _) σ'
 
   /-- Assign `x` an arbitrary value `v` according to `UpdateState`. -/
-  | eval_havoc :
+  | eval_set_nondet :
     UpdateState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ----
-    EvalCmd δ σ (.havoc x _) σ'
+    EvalCmd δ σ (.set x .nondet _) σ'
 
   /-- If `e` evaluates to true in `σ`, evaluate to the same `σ`. This semantics
   does not have a concept of an erroneous execution. -/
diff --git a/Strata/DL/Imperative/CmdType.lean b/Strata/DL/Imperative/CmdType.lean
index 834d876d4..9ea4b7d37 100644
--- a/Strata/DL/Imperative/CmdType.lean
+++ b/Strata/DL/Imperative/CmdType.lean
@@ -31,7 +31,7 @@ def Cmd.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)]
     match TC.lookup τ x with
     | none =>
       match e with
-      | some expr =>
+      | .det expr =>
         if x ∈ TC.freeVars expr then
           .error <| md.toDiagnosticF f!"Variable {x} cannot appear in its own initialization expression!"
         else
@@ -40,13 +40,13 @@ def Cmd.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)]
           let τ ← TC.unifyTypes τ [(xty, ety)]
           let (xty, τ) ← TC.postprocess ctx τ xty
           let τ := TC.update τ x xty
-          let c := Cmd.init x xty (some expr) md
+          let c := Cmd.init x xty (.det expr) md
           .ok (c, τ)
-      | none =>
+      | .nondet =>
         let (xty, τ) ← TC.preprocess ctx τ xty
         let (xty, τ) ← TC.postprocess ctx τ xty
         let τ := TC.update τ x xty
-        let c := Cmd.init x xty none md
+        let c := Cmd.init x xty .nondet md
         .ok (c, τ)
     | some xty =>
       .error <| md.toDiagnosticF f!"Variable {x} of type {xty} already in context."
@@ -55,15 +55,14 @@ def Cmd.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)]
     match TC.lookup τ x with
     | none => .error <| md.toDiagnosticF f!"Cannot set undeclared variable {x}."
     | some xty =>
-      let (e, ety, τ) ← TC.inferType ctx τ c e
-      let τ ← TC.unifyTypes τ [(xty, ety)]
-      let c := Cmd.set x e md
-      .ok (c, τ)
-
-  | .havoc x md =>
-    match TC.lookup τ x with
-    | some _ => .ok (c, τ)
-    | none => .error <| md.toDiagnosticF f!"Cannot havoc undeclared variable {x}."
+      match e with
+      | .det expr =>
+        let (expr, ety, τ) ← TC.inferType ctx τ c expr
+        let τ ← TC.unifyTypes τ [(xty, ety)]
+        let c := Cmd.set x (.det expr) md
+        .ok (c, τ)
+      | .nondet =>
+        .ok (c, τ)
 
   | .assert label e md =>
     let (e, ety, τ) ← TC.inferType ctx τ c e
diff --git a/Strata/DL/Imperative/NondetStmt.lean b/Strata/DL/Imperative/NondetStmt.lean
index f95175e81..a507a22e0 100644
--- a/Strata/DL/Imperative/NondetStmt.lean
+++ b/Strata/DL/Imperative/NondetStmt.lean
@@ -44,11 +44,11 @@ inductive NondetStmt (P : PureExpr) (Cmd : Type) : Type where
   deriving Inhabited
 
 abbrev NondetStmt.init {P : PureExpr} (name : P.Ident) (ty : P.Ty) (expr : P.Expr) (md : MetaData P) :=
-  NondetStmt.cmd (P:=P) (Cmd.init name ty expr md)
+  NondetStmt.cmd (P:=P) (Cmd.init name ty (.det expr) md)
 abbrev NondetStmt.set {P : PureExpr} (name : P.Ident) (expr : P.Expr) (md : MetaData P) :=
-  NondetStmt.cmd (P:=P) (Cmd.set name expr md)
+  NondetStmt.cmd (P:=P) (Cmd.set name (.det expr) md)
 abbrev NondetStmt.havoc {P : PureExpr} (name : P.Ident) (md : MetaData P) :=
-  NondetStmt.cmd (P:=P) (Cmd.havoc name md)
+  NondetStmt.cmd (P:=P) (Cmd.set name .nondet md)
 abbrev NondetStmt.assert {P : PureExpr} (label : String) (b : P.Expr) (md : MetaData P) :=
   NondetStmt.cmd (P:=P) (Cmd.assert label b md)
 abbrev NondetStmt.assume {P : PureExpr} (label : String) (b : P.Expr) (md : MetaData P) :=
diff --git a/Strata/DL/Imperative/SemanticsProps.lean b/Strata/DL/Imperative/SemanticsProps.lean
index e48d9a7f1..d3ebaa5ef 100644
--- a/Strata/DL/Imperative/SemanticsProps.lean
+++ b/Strata/DL/Imperative/SemanticsProps.lean
@@ -145,7 +145,7 @@ theorem semantic_eval_eq_of_eval_cmd_set_unrelated_var
   [HasFvar P] [HasVal P] [HasBool P] [HasNot P]:
   WellFormedSemanticEvalExprCongr δ →
   ¬ v ∈ HasVarsPure.getVars e →
-  EvalCmd P δ σ (Cmd.set v e' md) σ' →
+  EvalCmd P δ σ (Cmd.set v (.det e') md) σ' →
   δ σ e = δ σ' e := by
   intro Hwf Hnin Heval
   unfold WellFormedSemanticEvalExprCongr at Hwf
@@ -169,10 +169,10 @@ theorem eval_cmd_set_comm'
   ¬ x1 = x2 →
   δ σ v1 = δ σ2 v1 →
   δ σ v2 = δ σ1 v2 →
-  EvalCmd P δ σ (Cmd.set x1 v1 md1) σ1 →
-  EvalCmd P δ σ1 (Cmd.set x2 v2 md2) σ' →
-  EvalCmd P δ σ (Cmd.set x2 v2 md2') σ2 →
-  EvalCmd P δ σ2 (Cmd.set x1 v1 md1') σ'' →
+  EvalCmd P δ σ (Cmd.set x1 (.det v1) md1) σ1 →
+  EvalCmd P δ σ1 (Cmd.set x2 (.det v2) md2) σ' →
+  EvalCmd P δ σ (Cmd.set x2 (.det v2) md2') σ2 →
+  EvalCmd P δ σ2 (Cmd.set x1 (.det v1) md1') σ'' →
   σ' = σ'' := by
   intro Hneq Heq1 Heq2 Hs1 Hs2 Hs3 Hs4
   cases Hs1 with | eval_set _ Hu1 _ =>
@@ -189,10 +189,10 @@ theorem eval_cmd_set_comm
   ¬ x1 = x2 →
   ¬ x1 ∈ HasVarsPure.getVars v2 →
   ¬ x2 ∈ HasVarsPure.getVars v1 →
-  EvalCmd P δ σ (Cmd.set x1 v1 md1) σ1 →
-  EvalCmd P δ σ1 (Cmd.set x2 v2 md2) σ' →
-  EvalCmd P δ σ (Cmd.set x2 v2 md2') σ2 →
-  EvalCmd P δ σ2 (Cmd.set x1 v1 md1') σ'' →
+  EvalCmd P δ σ (Cmd.set x1 (.det v1) md1) σ1 →
+  EvalCmd P δ σ1 (Cmd.set x2 (.det v2) md2) σ' →
+  EvalCmd P δ σ (Cmd.set x2 (.det v2) md2') σ2 →
+  EvalCmd P δ σ2 (Cmd.set x1 (.det v1) md1') σ'' →
   σ' = σ'' := by
   intro Hwf Hneq Hnin1 Hnin2 Hs1 Hs2 Hs3 Hs4
   have Heval2:= semantic_eval_eq_of_eval_cmd_set_unrelated_var Hwf Hnin1 Hs1
@@ -206,10 +206,10 @@ theorem eval_stmt_set_comm
   ¬ x1 = x2 →
   ¬ x1 ∈ HasVarsPure.getVars v2 →
   ¬ x2 ∈ HasVarsPure.getVars v1 →
-  EvalStmt P (Cmd P) (EvalCmd P) evalFun δ σ (.cmd (Cmd.set x1 v1 md1)) σ1 δ1 →
-  EvalStmt P (Cmd P) (EvalCmd P) evalFun δ σ1 (.cmd (Cmd.set x2 v2 md2)) σ' δ2 →
-  EvalStmt P (Cmd P) (EvalCmd P) evalFun δ σ (.cmd (Cmd.set x2 v2 md2')) σ2 δ3 →
-  EvalStmt P (Cmd P) (EvalCmd P) evalFun δ σ2 (.cmd (Cmd.set x1 v1 md1')) σ'' δ4 →
+  EvalStmt P (Cmd P) (EvalCmd P) evalFun δ σ (.cmd (Cmd.set x1 (.det v1) md1)) σ1 δ1 →
+  EvalStmt P (Cmd P) (EvalCmd P) evalFun δ σ1 (.cmd (Cmd.set x2 (.det v2) md2)) σ' δ2 →
+  EvalStmt P (Cmd P) (EvalCmd P) evalFun δ σ (.cmd (Cmd.set x2 (.det v2) md2')) σ2 δ3 →
+  EvalStmt P (Cmd P) (EvalCmd P) evalFun δ σ2 (.cmd (Cmd.set x1 (.det v1) md1')) σ'' δ4 →
   σ' = σ'' := by
   intro Hwf Hneq Hnin1 Hnin2 Hs1 Hs2 Hs3 Hs4
   cases Hs1; cases Hs2; cases Hs3; cases Hs4
@@ -223,8 +223,8 @@ theorem eval_stmts_set_comm
   ¬ x1 = x2 →
   ¬ x1 ∈ HasVarsPure.getVars v2 →
   ¬ x2 ∈ HasVarsPure.getVars v1 →
-  EvalBlock P (Cmd P) (EvalCmd P) evalFun δ σ [(.cmd (Cmd.set x1 v1 md1)), (.cmd (Cmd.set x2 v2 md2))] σ' δ' →
-  EvalBlock P (Cmd P) (EvalCmd P) evalFun δ σ [(.cmd (Cmd.set x2 v2 md2')), (.cmd (Cmd.set x1 v1 md1'))] σ'' δ'' →
+  EvalBlock P (Cmd P) (EvalCmd P) evalFun δ σ [(.cmd (Cmd.set x1 (.det v1) md1)), (.cmd (Cmd.set x2 (.det v2) md2))] σ' δ' →
+  EvalBlock P (Cmd P) (EvalCmd P) evalFun δ σ [(.cmd (Cmd.set x2 (.det v2) md2')), (.cmd (Cmd.set x1 (.det v1) md1'))] σ'' δ'' →
   σ' = σ'' := by
   intro Hwf Hneq Hnin1 Hnin2 Heval1 Heval2
   -- Decompose first evaluation: [set x1 v1, set x2 v2]
diff --git a/Strata/DL/Imperative/Stmt.lean b/Strata/DL/Imperative/Stmt.lean
index 3244f544e..6630b8d0e 100644
--- a/Strata/DL/Imperative/Stmt.lean
+++ b/Strata/DL/Imperative/Stmt.lean
@@ -33,11 +33,13 @@ inductive Stmt (P : PureExpr) (Cmd : Type) : Type where
   | cmd      (cmd : Cmd)
   /-- An block containing a `List` of `Stmt`. -/
   | block    (label : String) (b : List (Stmt P Cmd)) (md : MetaData P)
-  /-- A conditional execution statement. -/
-  | ite      (cond : P.Expr)  (thenb : List (Stmt P Cmd)) (elseb : List (Stmt P Cmd)) (md : MetaData P)
+  /-- A conditional execution statement. When `cond` is `.nondet`, the branch
+  is chosen non-deterministically. -/
+  | ite      (cond : ExprOrNondet P)  (thenb : List (Stmt P Cmd)) (elseb : List (Stmt P Cmd)) (md : MetaData P)
   /-- An iterated execution statement. Includes an optional measure (for
-  termination) and invariants. -/
-  | loop     (guard : P.Expr) (measure : Option P.Expr) (invariants : List P.Expr)
+  termination) and invariants. When `guard` is `.nondet`, the loop iterates
+  a non-deterministic number of times. -/
+  | loop     (guard : ExprOrNondet P) (measure : Option P.Expr) (invariants : List P.Expr)
              (body : List (Stmt P Cmd)) (md : MetaData P)
   /-- An exit statement that transfers control out of the nearest enclosing
   block with the given label. If no label is provided, exits the nearest
@@ -68,11 +70,11 @@ def Stmt.inductionOn {P : PureExpr} {Cmd : Type}
     (block_case : ∀ (label : String) (b : List (Stmt P Cmd)) (md : MetaData P),
       (∀ s, s ∈ b → motive s) →
       motive (Stmt.block label b md))
-    (ite_case : ∀ (cond : P.Expr) (thenb elseb : List (Stmt P Cmd)) (md : MetaData P),
+    (ite_case : ∀ (cond : ExprOrNondet P) (thenb elseb : List (Stmt P Cmd)) (md : MetaData P),
       (∀ s, s ∈ thenb → motive s) →
       (∀ s, s ∈ elseb → motive s) →
       motive (Stmt.ite cond thenb elseb md))
-    (loop_case : ∀ (guard : P.Expr) (measure : Option P.Expr) (invariant : List P.Expr)
+    (loop_case : ∀ (guard : ExprOrNondet P) (measure : Option P.Expr) (invariant : List P.Expr)
       (body : List (Stmt P Cmd)) (md : MetaData P),
       (∀ s, s ∈ body → motive s) →
       motive (Stmt.loop guard measure invariant body md))
@@ -109,8 +111,8 @@ def Stmt.sizeOf (s : Imperative.Stmt P C) : Nat :=
   match s with
   | .cmd c => 1 + SizeOf.sizeOf c
   | .block _ bss _ => 1 + Block.sizeOf bss
-  | .ite c tss ess _ => 3 + sizeOf c + Block.sizeOf tss + Block.sizeOf ess
-  | .loop g _ _ bss _ => 3 + sizeOf g + Block.sizeOf bss
+  | .ite _ tss ess _ => 3 + Block.sizeOf tss + Block.sizeOf ess
+  | .loop _ _ _ bss _ => 3 + Block.sizeOf bss
   | .exit _ _ => 1
   | .funcDecl _ _ => 1
   | .typeDecl _ _ => 1
@@ -193,8 +195,8 @@ def Stmt.getVars [HasVarsPure P P.Expr] [HasVarsPure P C] (s : Stmt P C) : List
   match s with
   | .cmd cmd => HasVarsPure.getVars cmd
   | .block _ bss _ => Block.getVars bss
-  | .ite _ tbss ebss _ => Block.getVars tbss ++ Block.getVars ebss
-  | .loop _ _ _ bss _ => Block.getVars bss
+  | .ite cond tbss ebss _ => cond.getVars ++ Block.getVars tbss ++ Block.getVars ebss
+  | .loop guard _ _ bss _ => guard.getVars ++ Block.getVars bss
   | .exit _ _  => []
   | .funcDecl decl _ =>
     -- Get free variables from function body, excluding formal parameters
diff --git a/Strata/DL/Imperative/StmtSemantics.lean b/Strata/DL/Imperative/StmtSemantics.lean
index fcaef4cbd..cb74845e6 100644
--- a/Strata/DL/Imperative/StmtSemantics.lean
+++ b/Strata/DL/Imperative/StmtSemantics.lean
@@ -56,14 +56,24 @@ inductive EvalStmt (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
     WellFormedSemanticEvalBool δ →
     EvalBlock P Cmd EvalCmd extendEval δ σ t σ' δ' →
     ----
-    EvalStmt P Cmd EvalCmd extendEval δ σ (.ite c t e md) σ' δ'
+    EvalStmt P Cmd EvalCmd extendEval δ σ (.ite (.det c) t e md) σ' δ'
 
   | ite_false_sem :
     δ σ c = .some HasBool.ff →
     WellFormedSemanticEvalBool δ →
     EvalBlock P Cmd EvalCmd extendEval δ σ e σ' δ' →
     ----
-    EvalStmt P Cmd EvalCmd extendEval δ σ (.ite c t e md) σ' δ'
+    EvalStmt P Cmd EvalCmd extendEval δ σ (.ite (.det c) t e md) σ' δ'
+
+  | ite_nondet_true_sem :
+    EvalBlock P Cmd EvalCmd extendEval δ σ t σ' δ' →
+    ----
+    EvalStmt P Cmd EvalCmd extendEval δ σ (.ite .nondet t e md) σ' δ'
+
+  | ite_nondet_false_sem :
+    EvalBlock P Cmd EvalCmd extendEval δ σ e σ' δ' →
+    ----
+    EvalStmt P Cmd EvalCmd extendEval δ σ (.ite .nondet t e md) σ' δ'
 
   | funcDecl_sem [HasSubstFvar P] [HasVarsPure P P.Expr] :
     EvalStmt P Cmd EvalCmd extendEval δ σ (.funcDecl decl md) σ
@@ -153,6 +163,10 @@ theorem EvalStmtDefMonotone
       apply EvalBlockDefMonotone <;> assumption
     | ite_false_sem Hsome Hwf Heval =>
       apply EvalBlockDefMonotone <;> assumption
+    | ite_nondet_true_sem Heval =>
+      apply EvalBlockDefMonotone <;> assumption
+    | ite_nondet_false_sem Heval =>
+      apply EvalBlockDefMonotone <;> assumption
   | .exit _ _ => cases Heval
   | .loop _ _ _ _ _ => cases Heval
   | .funcDecl _ _ => cases Heval; assumption
diff --git a/Strata/DL/Imperative/StmtSemanticsSmallStep.lean b/Strata/DL/Imperative/StmtSemanticsSmallStep.lean
index daeee8e1a..fa9d06b36 100644
--- a/Strata/DL/Imperative/StmtSemanticsSmallStep.lean
+++ b/Strata/DL/Imperative/StmtSemanticsSmallStep.lean
@@ -82,7 +82,7 @@ inductive StepStmt
     WellFormedSemanticEvalBool δ →
     ----
     StepStmt P EvalCmd extendEval
-      (.stmt (.ite c tss ess _) σ δ)
+      (.stmt (.ite (.det c) tss ess _) σ δ)
       (.stmts tss σ δ)
 
   /-- If the condition of an `ite` statement evaluates to false, step to the else
@@ -92,7 +92,19 @@ inductive StepStmt
     WellFormedSemanticEvalBool δ →
     ----
     StepStmt P EvalCmd extendEval
-      (.stmt (.ite c tss ess _) σ δ)
+      (.stmt (.ite (.det c) tss ess _) σ δ)
+      (.stmts ess σ δ)
+
+  /-- Non-deterministic ite: step to the then branch. -/
+  | step_ite_nondet_true :
+    StepStmt P EvalCmd extendEval
+      (.stmt (.ite .nondet tss ess _) σ δ)
+      (.stmts tss σ δ)
+
+  /-- Non-deterministic ite: step to the else branch. -/
+  | step_ite_nondet_false :
+    StepStmt P EvalCmd extendEval
+      (.stmt (.ite .nondet tss ess _) σ δ)
       (.stmts ess σ δ)
 
   /-- If a loop guard is true, execute the body and then loop again. -/
@@ -101,8 +113,8 @@ inductive StepStmt
     WellFormedSemanticEvalBool δ →
     ----
     StepStmt P EvalCmd extendEval
-      (.stmt (.loop g m inv body md) σ δ)
-      (.stmts (body ++ [.loop g m inv body md]) σ δ)
+      (.stmt (.loop (.det g) m inv body md) σ δ)
+      (.stmts (body ++ [.loop (.det g) m inv body md]) σ δ)
 
   /-- If a loop guard is false, terminate the loop. -/
   | step_loop_exit :
@@ -110,7 +122,19 @@ inductive StepStmt
     WellFormedSemanticEvalBool δ →
     ----
     StepStmt P EvalCmd extendEval
-      (.stmt (.loop g m inv body _) σ δ)
+      (.stmt (.loop (.det g) m inv body _) σ δ)
+      (.terminal σ δ)
+
+  /-- Non-deterministic loop: enter the body. -/
+  | step_loop_nondet_enter :
+    StepStmt P EvalCmd extendEval
+      (.stmt (.loop .nondet m inv body md) σ δ)
+      (.stmts (body ++ [.loop .nondet m inv body md]) σ δ)
+
+  /-- Non-deterministic loop: exit the loop. -/
+  | step_loop_nondet_exit :
+    StepStmt P EvalCmd extendEval
+      (.stmt (.loop .nondet m inv body _) σ δ)
       (.terminal σ δ)
 
   /-- An exit statement produces an exiting configuration. -/
diff --git a/Strata/DL/Imperative/ToCProverGOTO.lean b/Strata/DL/Imperative/ToCProverGOTO.lean
index 2200f2f9f..3599e3a95 100644
--- a/Strata/DL/Imperative/ToCProverGOTO.lean
+++ b/Strata/DL/Imperative/ToCProverGOTO.lean
@@ -108,7 +108,7 @@ def Cmd.toGotoInstructions {P} [G: ToGoto P] [BEq P.Ident]
         sourceLoc := srcLoc,
         code := Code.decl v_expr }
     match e with
-    | some expr =>
+    | .det expr =>
       let e_expr ← G.toGotoExpr expr
       let assign_inst :=
         { type := .ASSIGN, locationNum := (trans.nextLoc + 1),
@@ -118,12 +118,12 @@ def Cmd.toGotoInstructions {P} [G: ToGoto P] [BEq P.Ident]
                 instructions := trans.instructions.append #[decl_inst, assign_inst],
                 nextLoc := trans.nextLoc + 2,
                 T := T }
-    | none =>
+    | .nondet =>
       return { trans with
                 instructions := trans.instructions.push decl_inst,
                 nextLoc := trans.nextLoc + 1,
                 T := T }
-  | .set v e md =>
+  | .set v (.det e) md =>
     let gty ← G.lookupType T v
     let v_expr := Expr.symbol (G.identToString v) gty
     let e_expr ← G.toGotoExpr e
@@ -159,7 +159,7 @@ def Cmd.toGotoInstructions {P} [G: ToGoto P] [BEq P.Ident]
               instructions := trans.instructions.push assume_inst,
               nextLoc := trans.nextLoc + 1,
               T := T }
-  | .havoc v md =>
+  | .set v .nondet md =>
     let gty ← G.lookupType T v
     let v_expr := Expr.symbol (G.identToString v) gty
     let srcLoc := metadataToSourceLoc md functionName trans.sourceText
@@ -167,8 +167,6 @@ def Cmd.toGotoInstructions {P} [G: ToGoto P] [BEq P.Ident]
       { id := .side_effect .Nondet,
         sourceLoc := srcLoc,
         type := gty,
-        /- (TODO) Do we want havoc'd variables to be null too? -/
-        -- namedFields := [("is_nondet_nullable", Expr.constant "1" Ty.Integer)]
       }
     let assign_inst :=
       { type := .ASSIGN, locationNum := trans.nextLoc,
@@ -301,7 +299,9 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] [BEq P.Ident]
       LOCATION end_label         ; after conditional
     -/
     let srcLoc := metadataToSourceLoc md functionName trans.sourceText
-    let cond_expr ← G.toGotoExpr cond
+    let cond_expr ← match cond with
+      | .det e => G.toGotoExpr e
+      | .nondet => pure { id := .side_effect .Nondet, type := .Boolean, operands := [] : Expr }
     let (trans, goto_else_idx) := emitCondGoto (Expr.not cond_expr) srcLoc trans
     let trans ← Block.toGotoInstructions trans.T functionName thenb trans
     let (trans, goto_end_idx) := emitUncondGoto srcLoc trans
@@ -326,7 +326,9 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] [BEq P.Ident]
     let srcLoc := metadataToSourceLoc md functionName trans.sourceText
     let loop_start_loc := trans.nextLoc
     let trans := emitLabel s!"loop_start_{loop_start_loc}" srcLoc trans
-    let guard_expr ← G.toGotoExpr guard
+    let guard_expr ← match guard with
+      | .det e => G.toGotoExpr e
+      | .nondet => pure { id := .side_effect .Nondet, type := .Boolean, operands := [] : Expr }
     let (trans, goto_end_idx) := emitCondGoto (Expr.not guard_expr) srcLoc trans
     let trans ← Block.toGotoInstructions trans.T functionName body trans
     -- Back edge: attach loop invariants and/or decreases clause
diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean
index 6496ed30b..4725d8369 100644
--- a/Strata/Languages/Boole/Verify.lean
+++ b/Strata/Languages/Boole/Verify.lean
@@ -334,10 +334,10 @@ def lowerFor
     (initExpr guardExpr stepExpr : Core.Expression.Expr)
     (invs : List Core.Expression.Expr)
     (body : List Core.Statement) : TranslateM Core.Statement := do
-  let initStmt : Core.Statement := Core.Statement.init id (.forAll [] ty) (some initExpr) (← toCoreMetaData m)
+  let initStmt : Core.Statement := Core.Statement.init id (.forAll [] ty) (.det initExpr) (← toCoreMetaData m)
   let stepStmt : Core.Statement := Core.Statement.set id stepExpr (← toCoreMetaData m)
   let loopBody := body ++ [stepStmt]
-  return .block "for" [initStmt, .loop guardExpr none invs loopBody (← toCoreMetaData m)] (← toCoreMetaData m)
+  return .block "for" [initStmt, .loop (.det guardExpr) none invs loopBody (← toCoreMetaData m)] (← toCoreMetaData m)
 
 private def lowerVarStatement (m : SourceRange) (ds : BooleDDM.DeclList SourceRange) : TranslateM (List Core.Statement) := do
   let mut outRev : List Core.Statement := []
@@ -348,7 +348,7 @@ private def lowerVarStatement (m : SourceRange) (ds : BooleDDM.DeclList SourceRa
     modify fun st => { st with globalVarCounter := n + 1 }
     let initName := mkIdent s!"init_{id.name}_{n}"
     newBVarsRev := (.fvar () id none : Core.Expression.Expr) :: newBVarsRev
-    outRev := Core.Statement.init id ty (some (.fvar () initName none)) (← toCoreMetaData m) :: outRev
+    outRev := Core.Statement.init id ty (.det (.fvar () initName none)) (← toCoreMetaData m) :: outRev
   modify fun st => { st with bvars := st.bvars ++ newBVarsRev.reverse.toArray }
   return outRev.reverse
 
@@ -377,7 +377,7 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement
   | .initStatement m ty ⟨_, n⟩ e =>
     let rhs ← toCoreExpr e
     modify fun st => { st with bvars := st.bvars.push (.fvar () (mkIdent n) none) }
-    return Core.Statement.init (mkIdent n) (← toCoreType ty) (some rhs) (← toCoreMetaData m)
+    return Core.Statement.init (mkIdent n) (← toCoreType ty) (.det rhs) (← toCoreMetaData m)
   | .assign m _ lhs rhs =>
     let rec lhsParts (lhs : BooleDDM.Lhs SourceRange) : TranslateM (String × List Core.Expression.Expr) := do
       match lhs with
@@ -404,11 +404,11 @@ def toCoreStmt (s : BooleDDM.Statement SourceRange) : TranslateM Core.Statement
     let elseb ← withBVars [] <| match e with
       | .else0 _ => return []
       | .else1 _ b => toCoreBlock b
-    return .ite (← toCoreExpr c) thenb elseb (← toCoreMetaData m)
+    return .ite (.det (← toCoreExpr c)) thenb elseb (← toCoreMetaData m)
   | .havoc_statement m ⟨_, n⟩ =>
     return Core.Statement.havoc (mkIdent n) (← toCoreMetaData m)
   | .while_statement m g _ invs b =>
-    return .loop (← toCoreExpr g) none (← toCoreInvariants invs) (← withBVars [] (toCoreBlock b)) (← toCoreMetaData m)
+    return .loop (.det (← toCoreExpr g)) none (← toCoreInvariants invs) (← withBVars [] (toCoreBlock b)) (← toCoreMetaData m)
   | .call_statement m ⟨_, lhs⟩ ⟨_, n⟩ ⟨_, args⟩ =>
     return Core.Statement.call (lhs.toList.map (mkIdent ·.val)) n (← args.toList.mapM toCoreExpr) (← toCoreMetaData m)
   | .call_unit_statement m ⟨_, n⟩ ⟨_, args⟩ =>
@@ -677,7 +677,7 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec
     let (id, ty) ← toCoreBind b
     let i := (← get).globalVarCounter
     modify fun s => { s with globalVarCounter := i + 1 }
-    return [.var id ty (some (.fvar () (mkIdent s!"init_{id.name}_{i}") none))]
+    return [.var id ty (.det (.fvar () (mkIdent s!"init_{id.name}_{i}") none))]
   | .command_axiom m ⟨_, l?⟩ e =>
     return [.ax { name := ← defaultLabel m "axiom" l?, e := ← toCoreExpr e }]
   | .command_distinct m ⟨_, l?⟩ ⟨_, es⟩ =>
diff --git a/Strata/Languages/C_Simp/DDMTransform/Translate.lean b/Strata/Languages/C_Simp/DDMTransform/Translate.lean
index ee5d55ef3..512563e94 100644
--- a/Strata/Languages/C_Simp/DDMTransform/Translate.lean
+++ b/Strata/Languages/C_Simp/DDMTransform/Translate.lean
@@ -383,7 +383,7 @@ partial def translateStmt (bindings : TransBindings) (arg : Arg) :
     let newBindings := { bindings with
                          boundVars := bbindings,
                          freeVars := bindings.freeVars.push id }
-    return ([(.cmd (.init id ty none md))], newBindings)
+    return ([(.cmd (.init id ty .nondet md))], newBindings)
   | q`C_Simp.init_def, #[ida, tpa, ea] =>
     let id ← translateIdent ida
     let tp ← translateLMonoTy bindings tpa
@@ -394,21 +394,21 @@ partial def translateStmt (bindings : TransBindings) (arg : Arg) :
     let newBindings := { bindings with
                          boundVars := bbindings,
                          freeVars := bindings.freeVars.push id }
-    return ([(.cmd (.init id ty val md))], newBindings)
+    return ([(.cmd (.init id ty (.det val) md))], newBindings)
   | q`C_Simp.assign, #[_tpa, ida, ea] =>
     let id ← translateIdent ida
     let val ← translateExpr bindings ea
-    return ([(.cmd (.set id val md))], bindings)
+    return ([(.cmd (.set id (.det val) md))], bindings)
   | q`C_Simp.if_command, #[ca, ta, fa] =>
     let c ← translateExpr bindings ca
-    return ([(.ite c (← translateBlock bindings ta) (← translateElse bindings fa) md)], bindings)
+    return ([(.ite (.det c) (← translateBlock bindings ta) (← translateElse bindings fa) md)], bindings)
   | q`C_Simp.while_command, #[ga, measurea, invarianta, ba] =>
-    return ([.loop (← translateExpr bindings ga) (← translateMeasure bindings measurea) (← translateInvariant bindings invarianta) (← translateBlock bindings ba) md], bindings)
+    return ([.loop (.det (← translateExpr bindings ga)) (← translateMeasure bindings measurea) (← translateInvariant bindings invarianta) (← translateBlock bindings ba) md], bindings)
   | q`C_Simp.return, #[_tpa, ea] =>
     -- Return statements are assignments to the global `return` variable
     -- TODO: I don't think this works if we have functions with different return types
     let val ← translateExpr bindings ea
-    return ([(.cmd (.set "return" val md))], bindings)
+    return ([(.cmd (.set "return" (.det val) md))], bindings)
   | q`C_Simp.annotation, #[a] =>
     let .op a_op := a
       | TransM.error s!"Annotation expected op {repr a}"
diff --git a/Strata/Languages/C_Simp/StrataToCBMC.lean b/Strata/Languages/C_Simp/StrataToCBMC.lean
index 19a3db053..bbb8e4e06 100644
--- a/Strata/Languages/C_Simp/StrataToCBMC.lean
+++ b/Strata/Languages/C_Simp/StrataToCBMC.lean
@@ -316,7 +316,7 @@ def cmdToJson (e : Strata.C_Simp.Command) (loc: SourceLoc) : Except String Json
         ]
       ]
     ])
-  | .havoc _ _ => throw "cmdToJson: Unimplemented"
+  | .set _ .nondet _ => throw "cmdToJson: Unimplemented"
 
 mutual
 partial def blockToJson (b: Imperative.Block Strata.C_Simp.Expression Strata.C_Simp.Command) (loc: SourceLoc) : Except String Json := do
diff --git a/Strata/Languages/C_Simp/Verify.lean b/Strata/Languages/C_Simp/Verify.lean
index da3cd6886..57a6c93e4 100644
--- a/Strata/Languages/C_Simp/Verify.lean
+++ b/Strata/Languages/C_Simp/Verify.lean
@@ -38,9 +38,12 @@ def translate_opt_expr (e : Option C_Simp.Expression.Expr) : Option (Lambda.LExp
 
 def translate_cmd (c: C_Simp.Command) : Core.Command :=
   match c with
-  | .init name ty e _md => .cmd (.init ⟨name.name, ()⟩ ty (translate_opt_expr e) {})
-  | .set name e _md => .cmd (.set ⟨name.name, ()⟩ (translate_expr e) {})
-  | .havoc name _md => .cmd (.havoc ⟨name.name, ()⟩ {})
+  | .init name ty e _md =>
+    let e' := e.map translate_expr
+    .cmd (.init ⟨name.name, ()⟩ ty e' {})
+  | .set name e _md =>
+    let e' := e.map translate_expr
+    .cmd (.set ⟨name.name, ()⟩ e' {})
   | .assert label b _md => .cmd (.assert label (translate_expr b) {})
   | .assume label b _md =>  .cmd (.assume label (translate_expr b) {})
   | .cover label b _md =>  .cmd (.cover label (translate_expr b) {})
@@ -49,8 +52,16 @@ def translate_stmt (s: Imperative.Stmt C_Simp.Expression C_Simp.Command) : Core.
   match s with
   | .cmd c => .cmd (translate_cmd c)
   | .block l b _md => .block l (b.map translate_stmt) {}
-  | .ite cond thenb elseb _md => .ite (translate_expr cond) (thenb.map translate_stmt) (elseb.map translate_stmt) {}
-  | .loop guard measure invariant body _md => .loop (translate_expr guard) (translate_opt_expr measure) (invariant.map translate_expr) (body.map translate_stmt) {}
+  | .ite cond thenb elseb _md =>
+    let cond' := match cond with
+      | .det e => Imperative.ExprOrNondet.det (translate_expr e)
+      | .nondet => .nondet
+    .ite cond' (thenb.map translate_stmt) (elseb.map translate_stmt) {}
+  | .loop guard measure invariant body _md =>
+    let guard' := match guard with
+      | .det e => Imperative.ExprOrNondet.det (translate_expr e)
+      | .nondet => .nondet
+    .loop guard' (translate_opt_expr measure) (invariant.map translate_expr) (body.map translate_stmt) {}
   | .funcDecl _ _ => panic! "C_Simp does not support function declarations"
   | .typeDecl _ _ => panic! "C_Simp does not support type declarations"
   | .exit label _md => .exit label {}
@@ -78,9 +89,8 @@ other analyses.
 def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement :=
   match s with
   | .loop guard measure invList body _ =>
-    match measure, invList with
-    | .some measure, _ =>
-      -- let bodyss : := body.ss
+    match guard, measure, invList with
+    | .det guard_expr, .some measure, _ =>
       let assigned_vars := (Imperative.Block.modifiedVars body).map (λ s => ⟨s.name, ()⟩)
       let havocd : Core.Statement := .block "loop havoc" (assigned_vars.map (λ n => Core.Statement.havoc n {})) {}
 
@@ -94,11 +104,11 @@ def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement :=
       let inv_assumes : List Core.Statement := invList.mapIdx fun i inv =>
         Core.Statement.assume s!"assume_invariant_{i}" (translate_expr inv) {}
       let arbitrary_iter_assumes := .block "arbitrary_iter_assumes"
-        ([Core.Statement.assume "assume_guard" (translate_expr guard) {}] ++ inv_assumes ++
+        ([Core.Statement.assume "assume_guard" (translate_expr guard_expr) {}] ++ inv_assumes ++
          [Core.Statement.assume "assume_measure_pos" measure_pos {}]) {}
-      let measure_old_value_assign : Core.Statement := .init "special-name-for-old-measure-value" (.forAll [] (.tcons "int" [])) (some (translate_expr measure)) {}
+      let measure_old_value_assign : Core.Statement := .init "special-name-for-old-measure-value" (.forAll [] (.tcons "int" [])) (.det (translate_expr measure)) {}
       let measure_decreases : Core.Statement := .assert "measure_decreases" (.app () (.app () (.op () "Int.Lt" none) (translate_expr measure)) (.fvar () "special-name-for-old-measure-value" none)) {}
-      let measure_imp_not_guard : Core.Statement := .assert "measure_imp_not_guard" (.ite () (.app () (.app () (.op () "Int.Le" none) (translate_expr measure)) (.intConst () 0)) (.app () (.op () "Bool.Not" none) (translate_expr guard)) (.true ())) {}
+      let measure_imp_not_guard : Core.Statement := .assert "measure_imp_not_guard" (.ite () (.app () (.app () (.op () "Int.Le" none) (translate_expr measure)) (.intConst () 0)) (.app () (.op () "Bool.Not" none) (translate_expr guard_expr)) (.true ())) {}
       let maintain_invariants : List Core.Statement := invList.mapIdx fun i inv =>
         .assert s!"arbitrary_iter_maintain_invariant_{i}" (translate_expr inv) {}
       let body_statements : List Core.Statement := body.map translate_stmt
@@ -106,12 +116,12 @@ def loop_elimination_statement(s : C_Simp.Statement) : Core.Statement :=
         ([havocd, arbitrary_iter_assumes, measure_old_value_assign] ++ body_statements ++
          [measure_decreases, measure_imp_not_guard] ++ maintain_invariants) {}
 
-      let not_guard : Core.Statement := .assume "not_guard" (.app () (.op () "Bool.Not" none) (translate_expr guard)) {}
+      let not_guard : Core.Statement := .assume "not_guard" (.app () (.op () "Bool.Not" none) (translate_expr guard_expr)) {}
       let invariant_assumes : List Core.Statement := invList.mapIdx fun i inv =>
         .assume s!"invariant_{i}" (translate_expr inv) {}
 
-      .ite (translate_expr guard) ([first_iter_facts, arbitrary_iter_facts, havocd, not_guard] ++ invariant_assumes) [] {}
-    | _, _ => panic! "Loop elimination require measure and invariant"
+      .ite (.det (translate_expr guard_expr)) ([first_iter_facts, arbitrary_iter_facts, havocd, not_guard] ++ invariant_assumes) [] {}
+    | _, _, _ => panic! "Loop elimination require measure and invariant"
   | _ => translate_stmt s
 
 -- C_Simp functions are Strata Core procedures
diff --git a/Strata/Languages/Core/CmdEval.lean b/Strata/Languages/Core/CmdEval.lean
index d48f73c5e..540488cfd 100644
--- a/Strata/Languages/Core/CmdEval.lean
+++ b/Strata/Languages/Core/CmdEval.lean
@@ -57,11 +57,11 @@ def preprocess (E : Env) (c : Cmd Expression) (e : Expression.Expr) : Expression
     -- command.
     -- See `CmdType.lean` for details.
     match eOpt with
-    | some _ =>
+    | .det _ =>
       let freeVars := e.freeVars
       let E' := E.insertFreeVarsInOldestScope freeVars
       (e, E')
-    | none => (e, E)
+    | .nondet => (e, E)
   | _ => (e, E)
 
 def genFreeVar (E : Env) (x : Expression.Ident) (ty : Expression.Ty) : Expression.Expr × Env :=
diff --git a/Strata/Languages/Core/DDMTransform/ASTtoCST.lean b/Strata/Languages/Core/DDMTransform/ASTtoCST.lean
index 6875a1903..bd137a818 100644
--- a/Strata/Languages/Core/DDMTransform/ASTtoCST.lean
+++ b/Strata/Languages/Core/DDMTransform/ASTtoCST.lean
@@ -782,12 +782,12 @@ partial def stmtToCST {M} [Inhabited M] (s : Core.Statement)
     let nameAnn : Ann String M := ⟨default, name.toPretty⟩
     let tyCST ← lTyToCoreType ty
     let result ← match expr with
-    | none => do
+    | Imperative.ExprOrNondet.nondet => do
       let bind := Bind.bind_mk default nameAnn
                   ⟨default, none⟩ tyCST
       let dl := DeclList.declAtom default bind
       pure (.varStatement default dl)
-    | some e =>
+    | Imperative.ExprOrNondet.det e =>
       let exprCST ← lexprToExpr e 0
       pure (.initStatement default tyCST nameAnn exprCST)
     -- Push the newly declared variable to the *end of the bound variables
@@ -837,16 +837,24 @@ partial def stmtToCST {M} [Inhabited M] (s : Core.Statement)
     let blockCST ← blockToCST stmts
     pure (.block_statement default labelAnn blockCST)
   | .ite cond thenb elseb _md => do
-    let condCST ← lexprToExpr cond 0
     let thenCST ← blockToCST thenb
     let elseCST ← elseToCST elseb
-    pure (.if_statement default condCST thenCST elseCST)
+    match cond with
+    | .det e =>
+      let condCST ← lexprToExpr e 0
+      pure (.if_statement default condCST thenCST elseCST)
+    | .nondet =>
+      pure (.if_statement default (.bstar default) thenCST elseCST)
   | .loop guard measure invariant body _md => do
-    let guardCST ← lexprToExpr guard 0
     let measureCST ← measureToCST measure
     let invs ← invariantsToCST invariant
     let bodyCST ← blockToCST body
-    pure (.while_statement default guardCST measureCST invs bodyCST)
+    match guard with
+    | .det e =>
+      let guardCST ← lexprToExpr e 0
+      pure (.while_statement default guardCST measureCST invs bodyCST)
+    | .nondet =>
+      pure (.while_statement default (.bstar default) measureCST invs bodyCST)
   | .exit label _md => do
     match label with
     | some l =>
@@ -1028,7 +1036,7 @@ def distinctToCST {M} [Inhabited M] (name : CoreIdent) (es : List (Lambda.LExpr
 
 /-- Convert a variable declaration to CST -/
 def varToCST {M} [Inhabited M]
-    (name : CoreIdent) (ty : Lambda.LTy) (_e : Option (Lambda.LExpr CoreLParams.mono))
+    (name : CoreIdent) (ty : Lambda.LTy) (_e : Imperative.ExprOrNondet Expression)
     (_md : Imperative.MetaData Expression) : ToCSTM M (Command M) := do
   -- Register name as free variable
   modify (·.addGlobalFreeVars #[name.toPretty])
diff --git a/Strata/Languages/Core/DDMTransform/Grammar.lean b/Strata/Languages/Core/DDMTransform/Grammar.lean
index 9b900b49d..a4286e570 100644
--- a/Strata/Languages/Core/DDMTransform/Grammar.lean
+++ b/Strata/Languages/Core/DDMTransform/Grammar.lean
@@ -111,6 +111,7 @@ fn re_none () : regex => "re.none" "(" ")";
 
 fn btrue : bool => "true";
 fn bfalse : bool => "false";
+fn bstar : bool => "*";
 fn equiv (a : bool, b : bool) : bool => @[prec(4)] a " <==> " b;
 fn implies (a : bool, b : bool) : bool => @[prec(5), rightassoc] a " ==> " b;
 fn and (a : bool, b : bool) : bool => @[prec(10), leftassoc] a " && " b;
diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean
index cd259d1c3..372aeed00 100644
--- a/Strata/Languages/Core/DDMTransform/Translate.lean
+++ b/Strata/Languages/Core/DDMTransform/Translate.lean
@@ -184,13 +184,13 @@ instance : Inhabited (List Core.Statement × TransBindings) where
   default := ([], {})
 
 instance : Inhabited Core.Decl where
-  default := .var "badguy" (.forAll [] (.tcons "bool" [])) none
+  default := .var "badguy" (.forAll [] (.tcons "bool" [])) .nondet
 
 instance : Inhabited (Core.Procedure.CheckAttr) where
   default := .Default
 
 instance : Inhabited (Core.Decl × TransBindings) where
-  default := (.var "badguy" (.forAll [] (.tcons "bool" [])) none, {})
+  default := (.var "badguy" (.forAll [] (.tcons "bool" [])) .nondet, {})
 
 instance : Inhabited (Core.Decls × TransBindings) where
   default := ([], {})
@@ -1005,7 +1005,7 @@ def initVarStmts (tpids : ListMap Core.Expression.Ident LTy) (bindings : TransBi
   match tpids with
   | [] => return ([], bindings)
   | (id, tp) :: rest =>
-    let s := Core.Statement.init id tp none md
+    let s := Core.Statement.init id tp .nondet md
     let (stmts, bindings) ← initVarStmts rest bindings md
     return ((s :: stmts), bindings)
 
@@ -1037,7 +1037,7 @@ def translateInitStatement (p : Program) (bindings : TransBindings) (args : Arra
     let ty := (.forAll [] mty)
     let newBinding: LExpr Core.CoreLParams.mono := LExpr.fvar () lhs mty
     let bbindings := bindings.boundVars ++ [newBinding]
-    return ([.init lhs ty val md], { bindings with boundVars := bbindings })
+    return ([.init lhs ty (.det val) md], { bindings with boundVars := bbindings })
 
 def translateOptionReachCheck (arg : Arg) : TransM Bool := do
   let .option _ rc := arg
@@ -1110,18 +1110,32 @@ partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) :
     let md ← getOpMetaData op
     return ([.assume l c md], bindings)
   | q`Core.if_statement, #[ca, ta, fa] =>
-    let c ← translateExpr p bindings ca
     let (tss, thenBindings) ← translateBlock p bindings ta
     let (fss, elseBindings) ← translateElse p { bindings with gen := thenBindings.gen } fa
     let md ← getOpMetaData op
-    return ([.ite c tss fss md], { bindings with gen := elseBindings.gen })
+    -- Check if condition is the nondet star expression
+    let isNondet := match ca with
+      | .expr (ExprF.fn _ ⟨_, "bstar"⟩) => true
+      | _ => false
+    let cond : Imperative.ExprOrNondet Core.Expression ← if isNondet then
+      pure .nondet
+    else
+      pure (.det (← translateExpr p bindings ca))
+    return ([.ite cond tss fss md], { bindings with gen := elseBindings.gen })
   | q`Core.while_statement, #[ca, ma, ia, ba] =>
-    let c ← translateExpr p bindings ca
     let measure ← translateMeasure p bindings ma
     let invs ← translateInvariants p bindings ia
     let (bodyss, bindings) ← translateBlock p bindings ba
     let md ← getOpMetaData op
-    return ([.loop c measure invs bodyss md], bindings)
+    -- Check if guard is the nondet star expression
+    let isNondet := match ca with
+      | .expr (ExprF.fn _ ⟨_, "bstar"⟩) => true
+      | _ => false
+    let guard : Imperative.ExprOrNondet Core.Expression ← if isNondet then
+      pure .nondet
+    else
+      pure (.det (← translateExpr p bindings ca))
+    return ([.loop guard measure invs bodyss md], bindings)
   | q`Core.call_statement, #[lsa, fa, esa] =>
     let ls  ← translateCommaSep (translateIdent Core.CoreIdent) lsa
     let f   ← translateIdent String fa
@@ -1722,7 +1736,7 @@ def translateGlobalVar (bindings : TransBindings) (op : Operation) :
   let (id, targs, mty) ← translateBindMk bindings op.args[0]!
   let ty := LTy.forAll targs mty
   let md ← getOpMetaData op
-  let decl := (.var id ty none md)
+  let decl := (.var id ty .nondet md)
   let bindings := incrNum .var_def bindings
   return (decl, { bindings with freeVars := bindings.freeVars.push decl})
 
diff --git a/Strata/Languages/Core/Program.lean b/Strata/Languages/Core/Program.lean
index 082a52805..8076b105b 100644
--- a/Strata/Languages/Core/Program.lean
+++ b/Strata/Languages/Core/Program.lean
@@ -46,7 +46,7 @@ Note: constants are 0-ary functions.
 inductive Decl where
   /-- Global variable declaration. The optional RHS is not currently used in verification
       but could serve as a starting value for future execution-based analyses. -/
-  | var (name : Expression.Ident) (ty : Expression.Ty) (e : Option Expression.Expr) (md : MetaData Core.Expression := .empty)
+  | var (name : Expression.Ident) (ty : Expression.Ty) (e : Imperative.ExprOrNondet Core.Expression) (md : MetaData Core.Expression := .empty)
   | type (t : TypeDecl) (md : MetaData Core.Expression := .empty)
   | ax   (a : Axiom) (md : MetaData Core.Expression := .empty)
   -- The following is temporary, until we have lists and can encode `distinct` in Lambda.
@@ -89,13 +89,13 @@ def Decl.name (d : Decl) : Expression.Ident :=
   | _ => [d.name]
 
 def Decl.getVar? (d : Decl) :
-  Option (Expression.Ident × Expression.Ty × Option Expression.Expr) :=
+  Option (Expression.Ident × Expression.Ty × Imperative.ExprOrNondet Expression) :=
   match d with
   | .var name ty e _ => some (name, ty, e)
   | _ => none
 
 def Decl.getVar (d : Decl) (H: d.kind = .var):
-  Expression.Ident × Expression.Ty × Option Expression.Expr :=
+  Expression.Ident × Expression.Ty × Imperative.ExprOrNondet Expression :=
   match d with | .var name ty e _ => (name, ty, e)
 
 def Decl.getTypeDecl? (d : Decl) : Option TypeDecl :=
@@ -147,8 +147,8 @@ def Decl.stripMetaData (d : Decl) : Decl :=
 -- Metadata not included.
 instance : ToFormat Decl where
   format d := match d with
-    | .var name ty (some e) _md => f!"var ({name} : {ty}) := {e}"
-    | .var name ty none _md => f!"var ({name} : {ty})"
+    | .var name ty (.det e) _md => f!"var ({name} : {ty}) := {e}"
+    | .var name ty .nondet _md => f!"var ({name} : {ty})"
     | .type t _md => f!"{t}"
     | .ax a _md  => f!"{a}"
     | .distinct l es _md  => f!"distinct [{l}] {es}"
@@ -208,7 +208,7 @@ theorem Program.find?_kind : ∀ {p : Program}, (p.find? k x) = some d → d.kin
     apply ih (by rfl)
 
 def Program.getVar? (P: Program) (x : Expression.Ident)
-  : Option (Expression.Ident × Expression.Ty × Option Expression.Expr) := do
+  : Option (Expression.Ident × Expression.Ty × Imperative.ExprOrNondet Expression) := do
   let decl ← P.find? .var x
   let var ← decl.getVar?
   return var
@@ -225,8 +225,9 @@ def Program.getAxiom? (P: Program) (n : Expression.Ident) : Option Axiom := do
 
 def Program.getInit? (P: Program) (x : Expression.Ident) : Option Expression.Expr := do
   let var ← P.getVar? x
-  let init ← var.snd.snd
-  return init
+  match var.snd.snd with
+  | .det e => return e
+  | .nondet => none
 
 @[expose]
 def Program.getNames (P: Program) : List Expression.Ident :=
@@ -255,9 +256,10 @@ def Program.getVarTy? (P: Program) (x : Expression.Ident) : Option Expression.Ty
   | some decl => some $ (decl.getVar $ Program.find?_kind H).2.1
 
 def Program.getVarInit? (P: Program) (x : Expression.Ident) : Option Expression.Expr := do
-  match H: (P.find? .var x) with
-  | none => none
-  | some decl => (decl.getVar $ Program.find?_kind H).2.2
+  let var ← P.getVar? x
+  match var.snd.snd with
+  | .det e => return e
+  | .nondet => none
 
 theorem Program.findproc_some : (P.find? .proc x).isSome = (Procedure.find? P x).isSome := by
   simp [Procedure.find?, Option.isSome, Program.find?]
@@ -310,7 +312,7 @@ def Program.Function.find (P: Program) (x : Expression.Ident) (H : (P.find? .fun
   (P.find .func x H).getFunc (find_kind P)
 
 def Program.getVar (P: Program) (x : Expression.Ident) (H : (P.find? .var x).isSome = true)
-  : Expression.Ident × Expression.Ty × Option Expression.Expr :=
+  : Expression.Ident × Expression.Ty × Imperative.ExprOrNondet Expression :=
   (P.find .var x H).getVar (find_kind P)
 
 def Program.getVarTy (P: Program) (x : Expression.Ident) (H : (P.find? .var x).isSome = true)
@@ -318,7 +320,7 @@ def Program.getVarTy (P: Program) (x : Expression.Ident) (H : (P.find? .var x).i
   ((P.find .var x H).getVar (find_kind P)).2.1
 
 def Program.getVarInit (P: Program) (x : Expression.Ident) (H : (P.find? .var x).isSome = true)
-  : Option Expression.Expr :=
+  : Imperative.ExprOrNondet Expression :=
   ((P.find .var x H).getVar (find_kind P)).2.2
 def Program.Procedure.findP? (P : Program) (x : Expression.Ident)
   : Option (Procedure ×' (find? P x).isSome = true) :=
diff --git a/Strata/Languages/Core/ProgramWF.lean b/Strata/Languages/Core/ProgramWF.lean
index 75d70a5bb..265fba131 100644
--- a/Strata/Languages/Core/ProgramWF.lean
+++ b/Strata/Languages/Core/ProgramWF.lean
@@ -278,7 +278,7 @@ private theorem Except_bind_is_ok_rhs {E α β}
   Except_bind_is_ok m h r |>.mp
 
 @[local grind .]
-private theorem WFVarProp_trivial (p : Program) (name : Expression.Ident) (ty : Expression.Ty) (e : Option Expression.Expr) :
+private theorem WFVarProp_trivial (p : Program) (name : Expression.Ident) (ty : Expression.Ty) (e : Imperative.ExprOrNondet Expression) :
   WFVarProp p name ty e := by
   constructor
 
diff --git a/Strata/Languages/Core/Statement.lean b/Strata/Languages/Core/Statement.lean
index 8b679beac..4bbbd87c2 100644
--- a/Strata/Languages/Core/Statement.lean
+++ b/Strata/Languages/Core/Statement.lean
@@ -49,7 +49,7 @@ instance : HasPassiveCmds Expression Command where
   assume l e md := .cmd (.assume l e md)
 
 instance : HasHavoc Expression Command where
-  havoc x md := .cmd (.havoc x md)
+  havoc x md := .cmd (.set x .nondet md)
 
 instance : HasInit Expression Command where
   init x ty e md := .cmd (.init x ty e md)
@@ -71,16 +71,16 @@ abbrev Statement := Imperative.Stmt Core.Expression Core.Command
 abbrev Statements := List Statement
 
 @[expose, match_pattern]
-abbrev Statement.init (name : Expression.Ident) (ty : Expression.Ty) (expr : Option Expression.Expr)
+abbrev Statement.init (name : Expression.Ident) (ty : Expression.Ty) (expr : ExprOrNondet Expression)
     (md : MetaData Expression) :=
   @Stmt.cmd Expression Command (CmdExt.cmd (Cmd.init name ty expr md))
 @[expose, match_pattern]
 abbrev Statement.set (name : Expression.Ident) (expr : Expression.Expr)
     (md : MetaData Expression) :=
-  @Stmt.cmd Expression Command (CmdExt.cmd (Cmd.set name expr md))
+  @Stmt.cmd Expression Command (CmdExt.cmd (Cmd.set name (.det expr) md))
 @[expose, match_pattern]
 abbrev Statement.havoc (name : Expression.Ident) (md : MetaData Expression) :=
-  @Stmt.cmd Expression Command (CmdExt.cmd (Cmd.havoc name md))
+  @Stmt.cmd Expression Command (CmdExt.cmd (Cmd.set name .nondet md))
 @[expose, match_pattern]
 abbrev Statement.assert (label : String) (b : Expression.Expr) (md : MetaData Expression) :=
   @Stmt.cmd Expression Command (CmdExt.cmd (Cmd.assert label b md))
@@ -110,8 +110,7 @@ def Command.eraseTypes (c : Command) : Command :=
   | .cmd c =>
     match c with
     | .init name ty e md => .cmd $ .init name ty (e.map Lambda.LExpr.eraseTypes) md
-    | .set name e md => .cmd $ .set name e.eraseTypes md
-    | .havoc name md => .cmd $ .havoc name md
+    | .set name e md => .cmd $ .set name (e.map Lambda.LExpr.eraseTypes) md
     | .assert label b md => .cmd $ .assert label b.eraseTypes md
     | .assume label b md => .cmd $ .assume label b.eraseTypes md
     | .cover label b md => .cmd $ .cover label b.eraseTypes md
@@ -335,8 +334,8 @@ def Statement.substFvar (s : Core.Statement)
       (fr:Expression.Ident)
       (to:Expression.Expr) : Statement :=
   match s with
-  | .init lhs ty rhs metadata =>
-    .init lhs ty (rhs.map (Lambda.LExpr.substFvar · fr to)) metadata
+  | .init lhs ty e metadata =>
+    .init lhs ty (e.map (Lambda.LExpr.substFvar · fr to)) metadata
   | .set lhs rhs metadata =>
     .set lhs (Lambda.LExpr.substFvar rhs fr to) metadata
   | .havoc _ _ => s
@@ -352,10 +351,10 @@ def Statement.substFvar (s : Core.Statement)
   | .block lbl b metadata =>
     .block lbl (Block.substFvar b fr to) metadata
   | .ite cond thenb elseb metadata =>
-    .ite (Lambda.LExpr.substFvar cond fr to) (Block.substFvar thenb fr to)
+    .ite (cond.map (Lambda.LExpr.substFvar · fr to)) (Block.substFvar thenb fr to)
           (Block.substFvar elseb fr to) metadata
   | .loop guard measure invariant body metadata =>
-    .loop (Lambda.LExpr.substFvar guard fr to)
+    .loop (guard.map (Lambda.LExpr.substFvar · fr to))
           (Option.map (Lambda.LExpr.substFvar · fr to) measure)
           (invariant.map (Lambda.LExpr.substFvar · fr to))
           (Block.substFvar body fr to)
diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 396469979..7e96cc527 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -474,15 +474,21 @@ def evalAuxGo (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (ss :
           | .ite cond then_ss else_ss md =>
             let orig_stk := Ewn.stk
             let Ewn := { Ewn with stk := orig_stk.push [] }
-            let cond' := Ewn.env.exprEval cond
+            match cond with
+            | .nondet =>
+              -- Non-deterministic condition: process both branches
+              processIteBranchesNondet steps' old_var_subst
+                Ewn then_ss else_ss md orig_stk
+            | .det c =>
+            let cond' := Ewn.env.exprEval c
             match cond' with
             | .true _ | .false _ =>
               let (ss_live, ss_dead) :=
                 if cond'.isTrue then (then_ss, else_ss) else (else_ss, then_ss)
-              let deadDeferred := collectDeadBranchDeferred ss_dead cond Ewn.env.pathConditions
+              let deadDeferred := collectDeadBranchDeferred ss_dead c Ewn.env.pathConditions
               let Ewns :=
                 (go' Ewn ss_live .none).map fun (ewn : EnvWithNext) =>
-                  { ewn with stk := orig_stk.appendToTop [.ite cond' ewn.stk.top [] md] }
+                  { ewn with stk := orig_stk.appendToTop [.ite (.det cond') ewn.stk.top [] md] }
               -- Prepend dead-branch obligations to the first result only.
               -- Pre-ITE obligations flow through the live branch naturally;
               -- processIteBranches keeps them in the first (true-path) result,
@@ -495,7 +501,7 @@ def evalAuxGo (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (ss :
             | _ =>
               -- Process both branches.
               processIteBranches steps' old_var_subst
-                Ewn cond cond' then_ss else_ss md orig_stk
+                Ewn c cond' then_ss else_ss md orig_stk
 
           | .loop _ _ _ _ _ =>
             panic! "Cannot evaluate `loop` statement. \
@@ -564,23 +570,74 @@ def processIteBranches (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNe
   -- with no exit label, we can merge both states into one.
   | [{ stk := stk_t, env := E_t, exitLabel := .none}],
     [{ stk := stk_f, env := E_f, exitLabel := .none}] =>
-    let s' := Imperative.Stmt.ite cond' stk_t.top stk_f.top md
+    let s' := Imperative.Stmt.ite (.det cond') stk_t.top stk_f.top md
     [EnvWithNext.mk (Env.merge cond' E_t E_f).popScope
                     .none
                     (orig_stk.appendToTop [s'])]
   | _, _ =>
     let Ewns_t := Ewns_t.map
                       (fun (ewn : EnvWithNext) =>
-                        let s' := Imperative.Stmt.ite (LExpr.true ()) ewn.stk.top [] md
+                        let s' := Imperative.Stmt.ite (.det (LExpr.true ())) ewn.stk.top [] md
                         { ewn with env := ewn.env.popScope,
                                    stk := orig_stk.appendToTop [s']})
     let Ewns_f := Ewns_f.map
                       (fun (ewn : EnvWithNext) =>
-                        let s' := Imperative.Stmt.ite (LExpr.false ()) [] ewn.stk.top md
+                        let s' := Imperative.Stmt.ite (.det (LExpr.false ())) [] ewn.stk.top md
                         { ewn with env := ewn.env.popScope,
                                    stk := orig_stk.appendToTop [s']})
   Ewns_t ++ Ewns_f
   termination_by (steps, Imperative.Block.sizeOf then_ss + Imperative.Block.sizeOf else_ss)
+
+def processIteBranchesNondet (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext)
+    (then_ss else_ss : Statements)
+    (md : Imperative.MetaData Expression) (orig_stk : StmtsStack) : List EnvWithNext :=
+  -- Introduce a fresh boolean variable for the non-deterministic condition
+  let freshName : CoreIdent := ⟨s!"$__nondet_cond_{Ewn.env.pathConditions.length}", ()⟩
+  let freshVar : Expression.Expr := .fvar () freshName none
+  let Ewn := { Ewn with env := Ewn.env.pushEmptyScope }
+  have : 1 <= Imperative.Block.sizeOf then_ss := by
+   unfold Imperative.Block.sizeOf; split <;> omega
+  have : 1 <= Imperative.Block.sizeOf else_ss := by
+   unfold Imperative.Block.sizeOf; split <;> omega
+  have : Imperative.Block.sizeOf then_ss < Imperative.Block.sizeOf then_ss +
+                                          Imperative.Block.sizeOf else_ss := by
+    omega
+  have : Imperative.Block.sizeOf else_ss < Imperative.Block.sizeOf then_ss +
+                                          Imperative.Block.sizeOf else_ss := by
+   omega
+  let label_true := toString (f!"<label_nondet_ite_true: {freshName}>")
+  let label_false := toString (f!"<label_nondet_ite_false: !{freshName}>")
+  let path_conds_true := Ewn.env.pathConditions.push [(label_true, freshVar)]
+  let path_conds_false := Ewn.env.pathConditions.push
+                            [(label_false, (.ite () freshVar (LExpr.false ()) (LExpr.true ())))]
+  let Ewns_t := evalAuxGo steps old_var_subst
+                  {Ewn with env := {Ewn.env with pathConditions := path_conds_true}}
+                  then_ss .none
+  let Ewns_f := evalAuxGo steps old_var_subst
+                  {Ewn with env := {Ewn.env with pathConditions := path_conds_false,
+                                                 deferred := #[]}}
+                  else_ss .none
+  match Ewns_t, Ewns_f with
+  | [{ stk := stk_t, env := E_t, exitLabel := .none}],
+    [{ stk := stk_f, env := E_f, exitLabel := .none}] =>
+    let initStmt := Statement.init freshName (.forAll [] (.tcons "bool" [])) .nondet md
+    let s' := Imperative.Stmt.ite (.det freshVar) stk_t.top stk_f.top md
+    [EnvWithNext.mk (Env.merge freshVar E_t E_f).popScope
+                    .none
+                    (orig_stk.appendToTop [initStmt, s'])]
+  | _, _ =>
+    let Ewns_t := Ewns_t.map
+                      (fun (ewn : EnvWithNext) =>
+                        let s' := Imperative.Stmt.ite (.det (LExpr.true ())) ewn.stk.top [] md
+                        { ewn with env := ewn.env.popScope,
+                                   stk := orig_stk.appendToTop [s']})
+    let Ewns_f := Ewns_f.map
+                      (fun (ewn : EnvWithNext) =>
+                        let s' := Imperative.Stmt.ite (.det (LExpr.false ())) [] ewn.stk.top md
+                        { ewn with env := ewn.env.popScope,
+                                   stk := orig_stk.appendToTop [s']})
+    Ewns_t ++ Ewns_f
+  termination_by (steps, Imperative.Block.sizeOf then_ss + Imperative.Block.sizeOf else_ss)
 end
 
 def evalAux (E : Env) (old_var_subst : SubstMap) (ss : Statements) (optExit : Option (Option String)) :
diff --git a/Strata/Languages/Core/StatementSemanticsProps.lean b/Strata/Languages/Core/StatementSemanticsProps.lean
index 87607103c..e86b0d5ca 100644
--- a/Strata/Languages/Core/StatementSemanticsProps.lean
+++ b/Strata/Languages/Core/StatementSemanticsProps.lean
@@ -1740,7 +1740,7 @@ theorem EvalCmdTouch
     constructor
   case eval_set δ σ x v σ' σ₀ e Hsm Hup Hwf =>
     exact TouchVars.update_some Hup TouchVars.none
-  case eval_havoc x v σ' σ₀ e Hsm Hup Hwf =>
+  case eval_set_nondet x v σ' σ₀ e Hsm Hup Hwf =>
     exact TouchVars.update_some Hup TouchVars.none
   case eval_assert => exact TouchVars.none
   case eval_assume => exact TouchVars.none
@@ -2065,6 +2065,8 @@ theorem EvalStmtRefinesContract
   | .block_sem Heval => .block_sem (EvalBlockRefinesContract Heval)
   | .ite_true_sem Hcond Hwf Heval => .ite_true_sem Hcond Hwf (EvalBlockRefinesContract Heval)
   | .ite_false_sem Hcond Hwf Heval => .ite_false_sem Hcond Hwf (EvalBlockRefinesContract Heval)
+  | .ite_nondet_true_sem Heval => .ite_nondet_true_sem (EvalBlockRefinesContract Heval)
+  | .ite_nondet_false_sem Heval => .ite_nondet_false_sem (EvalBlockRefinesContract Heval)
   | .funcDecl_sem => .funcDecl_sem
   | .typeDecl_sem => .typeDecl_sem
 
diff --git a/Strata/Languages/Core/StatementType.lean b/Strata/Languages/Core/StatementType.lean
index 142bce6ca..4d589b281 100644
--- a/Strata/Languages/Core/StatementType.lean
+++ b/Strata/Languages/Core/StatementType.lean
@@ -106,24 +106,38 @@ where
           .ok (s', Env, C)
 
         | .ite cond tss ess md => do try
-          let _ ← Env.freeVarCheck cond f!"[{s}]" |>.mapError DiagnosticModel.fromFormat
-          let (conda, Env) ← LExpr.resolve C Env cond |>.mapError DiagnosticModel.fromFormat
-          let condty := conda.toLMonoTy
-          match condty with
-          | .tcons "bool" [] =>
+          match cond with
+          | .det c =>
+            let _ ← Env.freeVarCheck c f!"[{s}]" |>.mapError DiagnosticModel.fromFormat
+            let (conda, Env) ← LExpr.resolve C Env c |>.mapError DiagnosticModel.fromFormat
+            let condty := conda.toLMonoTy
+            match condty with
+            | .tcons "bool" [] =>
+              let (tss, Env, C) ← goBlock C Env tss [] labels
+              let (ess, Env, C) ← goBlock C Env ess [] labels
+              let s' := Stmt.ite (.det conda.unresolved) tss ess md
+              .ok (s', Env, C)
+            | _ => .error <| md.toDiagnosticF f!"[{s}]: If's condition {c} is not of type `bool`!"
+          | .nondet =>
             let (tss, Env, C) ← goBlock C Env tss [] labels
             let (ess, Env, C) ← goBlock C Env ess [] labels
-            let s' := Stmt.ite conda.unresolved tss ess md
+            let s' := Stmt.ite .nondet tss ess md
             .ok (s', Env, C)
-          | _ => .error <| md.toDiagnosticF f!"[{s}]: If's condition {cond} is not of type `bool`!"
           catch e =>
             -- Add source location to error messages.
             .error (errorWithSourceLoc e md)
 
         | .loop guard measure invariant bss md => do try
-          let _ ← Env.freeVarCheck guard f!"[{s}]" |>.mapError DiagnosticModel.fromFormat
-          let (conda, Env) ← LExpr.resolve C Env guard |>.mapError DiagnosticModel.fromFormat
-          let condty := conda.toLMonoTy
+          let guardResult ← match guard with
+            | .det g => do
+              let _ ← Env.freeVarCheck g f!"[{s}]" |>.mapError DiagnosticModel.fromFormat
+              let (conda, Env) ← LExpr.resolve C Env g |>.mapError DiagnosticModel.fromFormat
+              let condty := conda.toLMonoTy
+              if condty != .tcons "bool" [] then
+                throw <| md.toDiagnosticF f!"[{s}]: Loop's guard {g} is not of type `bool`!"
+              pure (some conda, Env)
+            | .nondet => pure (none, Env)
+          let (guarda, Env) := guardResult
           let (mt, Env) ← (match measure with
           | .some m => do
             let _ ← Env.freeVarCheck m f!"[{s}]" |>.mapError DiagnosticModel.fromFormat
@@ -139,17 +153,16 @@ where
               .error <| md.toDiagnosticF f!"[{s}]: Loop's invariant {i} is not of type `bool`!"
           ) ([], Env)
           let mty := mt.map LExpr.toLMonoTy
-          match (condty, mty) with
-          | (.tcons "bool" [], none)
-          | (.tcons "bool" [], some (.tcons "int" [])) =>
+          match mty with
+          | none | some (.tcons "int" []) =>
             let (tb, Env, C) ← goBlock C Env bss [] labels
-            let s' := Stmt.loop conda.unresolved (mt.map LExpr.unresolved) (it.map LExpr.unresolved) tb md
+            let guarda' : ExprOrNondet Expression := match guarda with
+              | some e => .det e.unresolved
+              | none => .nondet
+            let s' := Stmt.loop guarda' (mt.map LExpr.unresolved) (it.map LExpr.unresolved) tb md
             .ok (s', Env, C)
           | _ =>
-            match condty with
-            | .tcons "bool" [] =>
-              .error <| md.toDiagnosticF f!"[{s}]: Loop's measure {measure} is not of type `int`!"
-            | _ => .error <| md.toDiagnosticF f!"[{s}]: Loop's guard {guard} is not of type `bool`!"
+            .error <| md.toDiagnosticF f!"[{s}]: Loop's measure {measure} is not of type `int`!"
           catch e =>
             -- Add source location to error messages.
             .error (errorWithSourceLoc e md)
@@ -208,6 +221,9 @@ private def substOptionExpr (S : Subst) (oe : Option Expression.Expr) : Option E
   | some e => some (LExpr.applySubst e S)
   | none => none
 
+private def substExprOrNondet (S : Subst) (e : Imperative.ExprOrNondet Expression) : Imperative.ExprOrNondet Expression :=
+  e.map (LExpr.applySubst · S)
+
 /--
 Apply type substitution `S` to a command.
 -/
@@ -215,10 +231,9 @@ def Command.subst (S : Subst) (c : Command) : Command :=
   match c with
   | .cmd c => match c with
     | .init x ty e md =>
-      .cmd $ .init x (LTy.subst S ty) (substOptionExpr S e) md
+      .cmd $ .init x (LTy.subst S ty) (substExprOrNondet S e) md
     | .set x e md =>
-      .cmd $ .set x (e.applySubst S) md
-    | .havoc _ _ => .cmd $ c
+      .cmd $ .set x (substExprOrNondet S e) md
     | .assert label b md =>
       .cmd $ .assert label (b.applySubst S) md
     | .assume label b md =>
@@ -243,9 +258,15 @@ def Statement.subst (S : Subst) (s : Statement) : Statement :=
   | .block label bss md =>
     .block label (go S bss []) md
   | .ite cond tss ess md =>
-    .ite (cond.applySubst S) (go S tss []) (go S ess []) md
+    let cond' := match cond with
+      | .det e => ExprOrNondet.det (e.applySubst S)
+      | .nondet => .nondet
+    .ite cond' (go S tss []) (go S ess []) md
   | .loop guard m i bss md =>
-    .loop (guard.applySubst S) (substOptionExpr S m) (i.map (·.applySubst S)) (go S bss []) md
+    let guard' := match guard with
+      | .det e => ExprOrNondet.det (e.applySubst S)
+      | .nondet => .nondet
+    .loop guard' (substOptionExpr S m) (i.map (·.applySubst S)) (go S bss []) md
   | .exit _ _ => s
   | .funcDecl decl md =>
     let decl' := { decl with
diff --git a/Strata/Languages/Core/WF.lean b/Strata/Languages/Core/WF.lean
index 959b1e47a..124349604 100644
--- a/Strata/Languages/Core/WF.lean
+++ b/Strata/Languages/Core/WF.lean
@@ -67,9 +67,9 @@ structure WFcallProp (p : Program) (lhs : List Expression.Ident) (procName : Str
 
 structure WFblockProp (Cmd : Type) (p : Program) (label : String) (b : Block) : Prop where
 
-structure WFifProp    (Cmd : Type) (p : Program) (cond : Expression.Expr)  (thenb : Block) (elseb : Block) : Prop where
+structure WFifProp    (Cmd : Type) (p : Program) (cond : ExprOrNondet Expression)  (thenb : Block) (elseb : Block) : Prop where
 
-structure WFloopProp    (Cmd : Type) (p : Program) (guard : Expression.Expr) (measure : Option Expression.Expr) (invariant : List Expression.Expr) (b : Block) : Prop where
+structure WFloopProp    (Cmd : Type) (p : Program) (guard : ExprOrNondet Expression) (measure : Option Expression.Expr) (invariant : List Expression.Expr) (b : Block) : Prop where
 
 structure WFexitProp  (p : Program) (label : Option String) : Prop where
 
@@ -91,9 +91,9 @@ structure WFfuncDeclProp (p : Program) (decl : Imperative.PureFunc Expression) :
 def WFStatementProp (p : Program) (stmt : Statement) : Prop := match stmt with
   | .cmd   cmd => WFCmdExtProp p cmd
   | .block (label : String) (b : Block) _ => WFblockProp (CmdExt Expression) p label b
-  | .ite   (cond : Expression.Expr) (thenb : Block) (elseb : Block) _ =>
+  | .ite   (cond : ExprOrNondet Expression) (thenb : Block) (elseb : Block) _ =>
      WFifProp (CmdExt Expression) p cond thenb elseb
-  | .loop  (guard : Expression.Expr) (measure : Option Expression.Expr) (invariant : List Expression.Expr) (body : Block) _ =>
+  | .loop  (guard : ExprOrNondet Expression) (measure : Option Expression.Expr) (invariant : List Expression.Expr) (body : Block) _ =>
      WFloopProp (CmdExt Expression) p guard measure invariant body
   | .exit (label : Option String) _ => WFexitProp p label
   | .funcDecl decl _ => WFfuncDeclProp p decl
@@ -136,7 +136,7 @@ structure WFSpecProp (p : Program) (spec : Procedure.Spec) (d : Procedure): Prop
 
 /- Procedure Wellformedness -/
 
-structure WFVarProp (p : Program) (name : Expression.Ident) (ty : Expression.Ty) (e : Option Expression.Expr) : Prop where
+structure WFVarProp (p : Program) (name : Expression.Ident) (ty : Expression.Ty) (e : Imperative.ExprOrNondet Expression) : Prop where
 
 structure WFTypeDeclarationProp (p : Program) (f : TypeDecl) : Prop where
 
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index 125fac35f..5c64c70ea 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -330,7 +330,7 @@ private def exprAsUnusedInit (expr : StmtExprMd) (md : Imperative.MetaData Core.
   let ident : Core.CoreIdent := ⟨s!"$unused_{id}", ()⟩
   let tyVarName := s!"$__ty_unused_{id}"
   let coreType := LTy.forAll [tyVarName] (.ftvar tyVarName)
-  return [Core.Statement.init ident coreType (some coreExpr) md]
+  return [Core.Statement.init ident coreType (.det coreExpr) md]
 
 /--
 Translate Laurel StmtExpr to Core Statements using the `TranslateM` monad.
@@ -364,27 +364,27 @@ def translateStmt (outputParams : List Parameter) (stmt : StmtExprMd)
           if model.isFunction callee then
             -- Translate as expression (function application)
             let coreExpr ← translateExpr (⟨ .StaticCall callee args, callMd ⟩)
-            return [Core.Statement.init ident coreType (some coreExpr) md]
+            return [Core.Statement.init ident coreType (.det coreExpr) md]
           else
             -- Translate as: var name; call name := callee(args)
             let coreArgs ← args.mapM (fun a => translateExpr a)
             let defaultExpr := defaultExprForType model ty
-            let initStmt := Core.Statement.init ident coreType (some defaultExpr) md
+            let initStmt := Core.Statement.init ident coreType (.det defaultExpr) md
             let callStmt := Core.Statement.call [ident] callee.text coreArgs md
             return [initStmt, callStmt]
       | some (⟨ .InstanceCall .., _⟩) =>
           -- Instance method call as initializer: var name := target.method(args)
           -- Havoc the result since instance methods may be on unmodeled types
-          let initStmt := Core.Statement.init ident coreType none md
+          let initStmt := Core.Statement.init ident coreType .nondet md
           return [initStmt]
       | some (⟨ .Hole _ _, _⟩) =>
           -- Hole initializer: treat as havoc (init without value)
-          return [Core.Statement.init ident coreType none md]
+          return [Core.Statement.init ident coreType .nondet md]
       | some initExpr =>
           let coreExpr ← translateExpr initExpr
-          return [Core.Statement.init ident coreType (some coreExpr) md]
+          return [Core.Statement.init ident coreType (.det coreExpr) md]
       | none =>
-          return [Core.Statement.init ident coreType none md]
+          return [Core.Statement.init ident coreType .nondet md]
   | .Assign targets value =>
       match targets with
       | [⟨ .Identifier targetId, _ ⟩] =>
@@ -433,7 +433,7 @@ def translateStmt (outputParams : List Parameter) (stmt : StmtExprMd)
       let belse ← match elseBranch with
                   | some e => translateStmt outputParams e
                   | none => pure []
-      return [Imperative.Stmt.ite bcond bthen belse .empty]
+      return [Imperative.Stmt.ite (.det bcond) bthen belse .empty]
   | .StaticCall callee args =>
       -- Check if this is a function or procedure
       if model.isFunction callee then
@@ -462,7 +462,7 @@ def translateStmt (outputParams : List Parameter) (stmt : StmtExprMd)
       let invExprs ← invariants.mapM (translateExpr)
       let decreasingExprCore ← decreasesExpr.mapM (translateExpr)
       let bodyStmts ← translateStmt outputParams body
-      return [Imperative.Stmt.loop condExpr decreasingExprCore invExprs bodyStmts md]
+      return [Imperative.Stmt.loop (.det condExpr) decreasingExprCore invExprs bodyStmts md]
   | .Exit target =>
       return [Imperative.Stmt.exit (some target) md]
   | _ =>
diff --git a/Strata/Languages/Python/PythonToCore.lean b/Strata/Languages/Python/PythonToCore.lean
index 5f47e4e3c..17a8f99ec 100644
--- a/Strata/Languages/Python/PythonToCore.lean
+++ b/Strata/Languages/Python/PythonToCore.lean
@@ -328,7 +328,7 @@ def noneOrExpr (translation_ctx : TranslationContext) (fname n : String) (e: Cor
 
 def handleCallThrow (jmp_target : String) : Core.Statement :=
   let cond := .app () (.op () "ExceptOrNone..isExceptOrNone_mk_code" none) (.fvar () "maybe_except" none)
-  .ite cond [.exit (some jmp_target) .empty] [] .empty
+  .ite (.det cond) [.exit (some jmp_target) .empty] [] .empty
 
 def deduplicateTypeAnnotations (l : List (String × Option String)) : List (String × String) := Id.run do
   let mut m : Map String String := []
@@ -367,24 +367,24 @@ partial def collectVarDecls (translation_ctx : TranslationContext) (stmts: Array
     let name := p.fst
     let ty_name := p.snd
     match ty_name with
-    | "bool" => [(.init name t[bool] (some (.boolConst () false)) .empty), (.havoc name .empty)]
-    | "str" => [(.init name t[string] (some (.strConst () "")) .empty), (.havoc name .empty)]
-    | "int" => [(.init name t[int] (some (.intConst () 0)) .empty), (.havoc name .empty)]
-    | "float" => [(.init name t[string] (some (.strConst () "0.0")) .empty), (.havoc name .empty)] -- Floats as strs for now
-    | "bytes" => [(.init name t[string] (some (.strConst () "")) .empty), (.havoc name .empty)]
-    | "Client" => [(.init name clientType (some dummyClient) .empty), (.havoc name .empty)]
-    | "Dict[str Any]" => [(.init name dictStrAnyType (some dummyDictStrAny) .empty), (.havoc name .empty)]
-    | "List[str]" => [(.init name listStrType (some dummyListStr) .empty), (.havoc name .empty)]
-    | "datetime" => [(.init name datetimeType (some dummyDatetime) .empty), (.havoc name .empty)]
-    | "date" => [(.init name dateType (some dummyDate) .empty), (.havoc name .empty)]
-    | "timedelta" => [(.init name timedeltaType (some dummyTimedelta) .empty), (.havoc name .empty)]
+    | "bool" => [(.init name t[bool] (.det (.boolConst () false)) .empty), (.havoc name .empty)]
+    | "str" => [(.init name t[string] (.det (.strConst () "")) .empty), (.havoc name .empty)]
+    | "int" => [(.init name t[int] (.det (.intConst () 0)) .empty), (.havoc name .empty)]
+    | "float" => [(.init name t[string] (.det (.strConst () "0.0")) .empty), (.havoc name .empty)] -- Floats as strs for now
+    | "bytes" => [(.init name t[string] (.det (.strConst () "")) .empty), (.havoc name .empty)]
+    | "Client" => [(.init name clientType (.det dummyClient) .empty), (.havoc name .empty)]
+    | "Dict[str Any]" => [(.init name dictStrAnyType (.det dummyDictStrAny) .empty), (.havoc name .empty)]
+    | "List[str]" => [(.init name listStrType (.det dummyListStr) .empty), (.havoc name .empty)]
+    | "datetime" => [(.init name datetimeType (.det dummyDatetime) .empty), (.havoc name .empty)]
+    | "date" => [(.init name dateType (.det dummyDate) .empty), (.havoc name .empty)]
+    | "timedelta" => [(.init name timedeltaType (.det dummyTimedelta) .empty), (.havoc name .empty)]
     | _ =>
       let user_defined_class := translation_ctx.class_infos.find? (λ i => i.name == ty_name)
       match user_defined_class with
       | .some i =>
         let user_defined_class_ty := .forAll [] (.tcons i.name [])
         let user_defined_class_dummy := .fvar () ("DUMMY_" ++ i.name) none
-        [(.init name user_defined_class_ty (some user_defined_class_dummy) .empty), (.havoc name .empty)]
+        [(.init name user_defined_class_ty (.det user_defined_class_dummy) .empty), (.havoc name .empty)]
       | .none => panic! s!"Unsupported type annotation: `{ty_name}`"
   let foo := dedup.map toCore
   foo.flatten
@@ -606,11 +606,11 @@ partial def initTmpParam (translation_ctx: TranslationContext) (p: Python.expr S
     match f with
     | .Name _ n _ =>
       match n.val with
-      | "json_dumps" => [(.init p.snd t[string] (some (.strConst () "")) md), .call [p.snd, "maybe_except"] "json_dumps" [(.app () (.op () "DictStrAny_mk" none) (.strConst () "DefaultDict")), (Strata.Python.TypeStrToCoreExpr "IntOrNone")] md]
+      | "json_dumps" => [(.init p.snd t[string] (.det (.strConst () "")) md), .call [p.snd, "maybe_except"] "json_dumps" [(.app () (.op () "DictStrAny_mk" none) (.strConst () "DefaultDict")), (Strata.Python.TypeStrToCoreExpr "IntOrNone")] md]
       | "str" =>
         assert! args.val.size == 1
-        [(.init p.snd t[string] (some (.strConst () "")) md), .set p.snd (.app () (.op () "datetime_to_str" none) ((PyExprToCore default args.val[0]!).expr)) md]
-      | "int" => [(.init p.snd t[int] (some (.intConst () 0)) md), .set p.snd (.op () "datetime_to_int" none) md]
+        [(.init p.snd t[string] (.det (.strConst () "")) md), .set p.snd (.app () (.op () "datetime_to_str" none) ((PyExprToCore default args.val[0]!).expr)) md]
+      | "int" => [(.init p.snd t[int] (.det (.intConst () 0)) md), .set p.snd (.op () "datetime_to_int" none) md]
       | _ => panic! s!"Unsupported name {n.val}"
     | _ => panic! s!"Unsupported tmp param init call: {repr f}"
   | _ => panic! "Expected Call"
@@ -634,7 +634,7 @@ partial def exceptHandlersToCore (jmp_targets: List String) (translation_ctx: Tr
       [.set "exception_ty_matches" (.boolConst () false) md]
     let cond := .fvar () "exception_ty_matches" none
     let body_if_matches := body.val.toList.flatMap (λ s => (PyStmtToCore jmp_targets.tail! translation_ctx s).fst) ++ [.exit (some jmp_targets[1]!) md]
-    set_ex_ty_matches ++ [.ite cond body_if_matches [] md]
+    set_ex_ty_matches ++ [.ite (.det cond) body_if_matches [] md]
 
 partial def handleFunctionCall (lhs: List Core.Expression.Ident)
                                (fname: String)
@@ -677,7 +677,7 @@ partial def handleComprehension (translation_ctx: TranslationContext) (lhs: Pyth
     let guard := .app () (.op () "Bool.Not" none) (.eq () (.app () (.op () "dict_str_any_length" none) res.expr) (.intConst () 0))
     let then_ss: List Core.Statement := [.havoc (PyExprToString lhs) md]
     let else_ss: List Core.Statement := [.set (PyExprToString lhs) (.op () "ListStr_nil" none) md]
-    res.stmts ++ [.ite guard then_ss else_ss md]
+    res.stmts ++ [.ite (.det guard) then_ss else_ss md]
 
 partial def PyStmtToCore (jmp_targets: List String) (translation_ctx : TranslationContext) (s : Python.stmt SourceRange) : List Core.Statement × TranslationContext :=
   assert! jmp_targets.length > 0
@@ -730,7 +730,7 @@ partial def PyStmtToCore (jmp_targets: List String) (translation_ctx : Translati
     | .FunctionDef _ _ _ _ _ _ _ _ => panic! "Can't translate FunctionDef to Strata Core statement"
     | .If _ test then_b else_b =>
       let guard_ctx := {translation_ctx with expectedType := some (.tcons "bool" [])}
-      ([.ite (PyExprToCore guard_ctx test).expr (ArrPyStmtToCore translation_ctx then_b.val).fst (ArrPyStmtToCore translation_ctx else_b.val).fst md], none)
+      ([.ite (.det (PyExprToCore guard_ctx test).expr) (ArrPyStmtToCore translation_ctx then_b.val).fst (ArrPyStmtToCore translation_ctx else_b.val).fst md], none)
     | .Return _ v =>
       match v.val with
       | .some v => ([.set "ret" (PyExprToCore translation_ctx v).expr md, .exit (some jmp_targets[0]!) md], none) -- TODO: need to thread return value name here. For now, assume "ret"
@@ -740,14 +740,14 @@ partial def PyStmtToCore (jmp_targets: List String) (translation_ctx : Translati
       let guard := .app () (.op () "Bool.Not" none) (.eq () (.app () (.op () "dict_str_any_length" none) (PyExprToCore default itr).expr) (.intConst () 0))
       match tgt with
       | .Name _ n _ =>
-        let assign_tgt := [(.init n.val dictStrAnyType (some dummyDictStrAny) md)]
-        ([.ite guard (assign_tgt ++ (ArrPyStmtToCore translation_ctx body.val).fst) [] md], none)
+        let assign_tgt := [(.init n.val dictStrAnyType (.det dummyDictStrAny) md)]
+        ([.ite (.det guard) (assign_tgt ++ (ArrPyStmtToCore translation_ctx body.val).fst) [] md], none)
       | _ => panic! s!"tgt must be single name: {repr tgt}"
       -- TODO: missing havoc
     | .While _ test body _ =>
       -- Do one unrolling:
       let guard := .app () (.op () "Bool.Not" none) (.eq () (.app () (.op () "dict_str_any_length" none) (PyExprToCore default test).expr) (.intConst () 0))
-      ([.ite guard (ArrPyStmtToCore translation_ctx body.val).fst [] md], none)
+      ([.ite (.det guard) (ArrPyStmtToCore translation_ctx body.val).fst [] md], none)
       -- TODO: missing havoc
     | .Assert sr a _ =>
       let res := PyExprToCore translation_ctx a
@@ -816,7 +816,7 @@ def pyTyStrToLMonoTy (ty_str: String) : Lambda.LMonoTy :=
 
 def pythonFuncToCore (name : String) (args: List (String × String)) (body: Array (Python.stmt SourceRange)) (ret : Option (Python.expr SourceRange)) (spec : Core.Procedure.Spec) (translation_ctx : TranslationContext) : Core.Procedure :=
   let inputs : List (Lambda.Identifier Unit × Lambda.LMonoTy) := args.map (λ p => (p.fst, pyTyStrToLMonoTy p.snd))
-  let varDecls := collectVarDecls translation_ctx body ++ [(.init "exception_ty_matches" t[bool] (some (.boolConst () false)) .empty), (.havoc "exception_ty_matches" .empty)]
+  let varDecls := collectVarDecls translation_ctx body ++ [(.init "exception_ty_matches" t[bool] (.det (.boolConst () false)) .empty), (.havoc "exception_ty_matches" .empty)]
   let stmts := (ArrPyStmtToCore translation_ctx body).fst
   let body := varDecls ++ [.block "end" stmts .empty]
   let constructor := name.endsWith "___init__"
@@ -891,7 +891,7 @@ def pythonToCore (signatures : Python.Signatures) (pgm: Strata.Program) (prelude
   | .ClassDef _ _ _ _ _ _ _ => false
   | _ => true)
 
-  let globals := [(.var "__name__" (.forAll [] mty[string]) (some (.strConst () "__main__")))]
+  let globals := [(.var "__name__" (.forAll [] mty[string]) (.det (.strConst () "__main__")))]
 
   let rec helper {α : Type} (f : Python.stmt SourceRange → TranslationContext → List Core.Decl × α)
                (update : TranslationContext → α → TranslationContext)
diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean
index ba58a1bd6..72081f83b 100644
--- a/Strata/Transform/CallElimCorrect.lean
+++ b/Strata/Transform/CallElimCorrect.lean
@@ -843,7 +843,7 @@ theorem EvalStatementsContractHavocVars :
     apply EvalStmtRefinesContract
     apply Imperative.EvalStmt.cmd_sem
     apply EvalCommand.cmd_sem
-    apply Imperative.EvalCmd.eval_havoc <;> try assumption
+    apply Imperative.EvalCmd.eval_set_nondet <;> try assumption
     . simp [Imperative.isDefinedOver, Command.modifiedVars,Imperative.Cmd.modifiedVars,
             Imperative.HasVarsImp.modifiedVars]
       simp [Imperative.isDefined] at Hdef ⊢
diff --git a/Strata/Transform/CoreTransform.lean b/Strata/Transform/CoreTransform.lean
index bc3cafcbe..8b846da6b 100644
--- a/Strata/Transform/CoreTransform.lean
+++ b/Strata/Transform/CoreTransform.lean
@@ -223,7 +223,7 @@ def createInit (trip : (Expression.Ident × Expression.Ty) × Expression.Expr)
     (md:Imperative.MetaData Expression)
   : Statement :=
   match trip with
-  | ((v', ty), e) => Statement.init v' ty (some e) md
+  | ((v', ty), e) => Statement.init v' ty (.det e) md
 
 def createInits (trips : List ((Expression.Ident × Expression.Ty) × Expression.Expr))
     (md: (Imperative.MetaData Expression))
@@ -237,7 +237,7 @@ def createInitVar (trip : (Expression.Ident × Expression.Ty) × Expression.Iden
     (md:Imperative.MetaData Expression)
   : Statement :=
   match trip with
-  | ((v', ty), v) => Statement.init v' ty (some (Lambda.LExpr.fvar () v none)) md
+  | ((v', ty), v) => Statement.init v' ty (.det (Lambda.LExpr.fvar () v none)) md
 
 def createInitVars (trips : List ((Expression.Ident × Expression.Ty) × Expression.Ident))
     (md : (Imperative.MetaData Expression))
diff --git a/Strata/Transform/DetToNondet.lean b/Strata/Transform/DetToNondet.lean
index 1653b34a9..aa4e07b6d 100644
--- a/Strata/Transform/DetToNondet.lean
+++ b/Strata/Transform/DetToNondet.lean
@@ -26,11 +26,17 @@ def StmtToNondetStmt {P : PureExpr} [Imperative.HasBool P] [HasNot P]
   | .cmd    cmd => .cmd cmd
   | .block  _ bss _ => BlockToNondetStmt bss
   | .ite    cond tss ess md =>
-    .choice
-      (.seq (.assume "true_cond" cond md) (BlockToNondetStmt tss))
-      (.seq ((.assume "false_cond" (Imperative.HasNot.not cond) md)) (BlockToNondetStmt ess))
+    match cond with
+    | .det c =>
+      .choice
+        (.seq (.assume "true_cond" c md) (BlockToNondetStmt tss))
+        (.seq ((.assume "false_cond" (Imperative.HasNot.not c) md)) (BlockToNondetStmt ess))
+    | .nondet =>
+      .choice (BlockToNondetStmt tss) (BlockToNondetStmt ess)
   | .loop   guard _measure _inv bss md =>
-    .loop (.seq (.assume "guard" guard md) (BlockToNondetStmt bss))
+    match guard with
+    | .det g => .loop (.seq (.assume "guard" g md) (BlockToNondetStmt bss))
+    | .nondet => .loop (BlockToNondetStmt bss)
   | .typeDecl _ md => (.assume "skip" Imperative.HasBool.tt md)
   | .exit _ md => (.assume "skip" Imperative.HasBool.tt md)
   | .funcDecl _ md => (.assume "skip" Imperative.HasBool.tt md)
diff --git a/Strata/Transform/DetToNondetCorrect.lean b/Strata/Transform/DetToNondetCorrect.lean
index 74647b99c..1687a8ed3 100644
--- a/Strata/Transform/DetToNondetCorrect.lean
+++ b/Strata/Transform/DetToNondetCorrect.lean
@@ -86,6 +86,12 @@ theorem EvalStmt_noFuncDecl_preserves_δ
     | ite_false_sem _ _ Heval =>
       simp [Stmt.noFuncDecl] at Hno
       exact noFuncDecl_preserves_δ_block_aux extendEval ess _ _ _ _ ih_e Hno.2 Heval
+    | ite_nondet_true_sem Heval =>
+      simp [Stmt.noFuncDecl] at Hno
+      exact noFuncDecl_preserves_δ_block_aux extendEval tss _ _ _ _ ih_t Hno.1 Heval
+    | ite_nondet_false_sem Heval =>
+      simp [Stmt.noFuncDecl] at Hno
+      exact noFuncDecl_preserves_δ_block_aux extendEval ess _ _ _ _ ih_e Hno.2 Heval
   | loop_case guard measure invariant body md ih =>
     intros Hno Heval
     cases Heval
@@ -207,12 +213,30 @@ theorem StmtToNondetCorrect
         . apply EvalNondetStmt.cmd_sem
           refine EvalCmd.eval_assume ?_ Hwfb
           simp [WellFormedSemanticEvalBool] at Hwfb
-          exact (Hwfb σ c).2.mp Hfalse
+          exact (Hwfb σ _).2.mp Hfalse
           simp [isDefinedOver, HasVarsImp.modifiedVars, Cmd.modifiedVars, isDefined]
         . apply (ih _ _).2
           omega
           exact Hno.2
           rw [← Hδ]; exact Heval
+      | ite_nondet_true_sem Heval =>
+        simp [Stmt.noFuncDecl] at Hno
+        have Hδ : _ = δ := EvalBlock_noFuncDecl_preserves_δ extendEval tss δ _ σ σ' Hno.1 Heval
+        specialize ih (Block.sizeOf tss) (by simp_all; omega)
+        refine EvalNondetStmt.choice_left_sem Hwfb ?_
+        apply (ih _ _).2
+        omega
+        exact Hno.1
+        rw [← Hδ]; exact Heval
+      | ite_nondet_false_sem Heval =>
+        simp [Stmt.noFuncDecl] at Hno
+        have Hδ : _ = δ := EvalBlock_noFuncDecl_preserves_δ extendEval ess δ _ σ σ' Hno.2 Heval
+        specialize ih (Block.sizeOf ess) (by simp_all; omega)
+        refine EvalNondetStmt.choice_right_sem Hwfb ?_
+        apply (ih _ _).2
+        omega
+        exact Hno.2
+        rw [← Hδ]; exact Heval
     | .exit _ _ =>
       cases Heval
     | .loop _ _ _ _ _ =>
diff --git a/Strata/Transform/LoopElim.lean b/Strata/Transform/LoopElim.lean
index 19eba8aed..38d1a0235 100644
--- a/Strata/Transform/LoopElim.lean
+++ b/Strata/Transform/LoopElim.lean
@@ -100,11 +100,13 @@ def Stmt.removeLoopsM
   match s with
   | .loop guard measure invariants bss md => do
     let loop_num ← StateT.modifyGet (fun x => (x, x + 1))
-    let neg_guard : P.Expr := HasNot.not guard
     let assigned_vars := Block.modifiedVars bss
     -- All of the replaced statements reuse the metadata md.
     let havocd : Stmt P C :=
       .block s!"loop_havoc_{loop_num}" (assigned_vars.map (λ n => Stmt.cmd (HasHavoc.havoc n md))) {}
+    match guard with
+    | .det g =>
+    let neg_guard : P.Expr := HasNot.not g
     let entry_invariants := invariants.mapIdx fun i inv =>
       Stmt.cmd (HasPassiveCmds.assert s!"entry_invariant_{loop_num}_{i}" inv md)
     let entry_invariant_assumes := invariants.mapIdx fun i inv =>
@@ -114,7 +116,7 @@ def Stmt.removeLoopsM
     let inv_assumes := invariants.mapIdx fun i inv =>
       Stmt.cmd (HasPassiveCmds.assume s!"assume_invariant_{loop_num}_{i}" inv md)
     let arbitrary_iter_assumes := .block s!"arbitrary_iter_assumes_{loop_num}"
-      ([Stmt.cmd (HasPassiveCmds.assume s!"assume_guard_{loop_num}" guard md)] ++ inv_assumes)
+      ([Stmt.cmd (HasPassiveCmds.assume s!"assume_guard_{loop_num}" g md)] ++ inv_assumes)
       md
     let maintain_invariants := invariants.mapIdx fun i inv =>
       Stmt.cmd (HasPassiveCmds.assert s!"arbitrary_iter_maintain_invariant_{loop_num}_{i}" inv md)
@@ -130,7 +132,7 @@ def Stmt.removeLoopsM
         -- Variables with `$__` prefix are internal variables.
         let m_old_ident    := HasIdent.ident s!"$__loop_measure_{loop_num}"
         let m_old_expr     := HasFvar.mkFvar m_old_ident
-        let init_m_old     := Stmt.cmd (HasInit.init m_old_ident HasIntOrder.intTy none md)
+        let init_m_old     := Stmt.cmd (HasInit.init m_old_ident HasIntOrder.intTy .nondet md)
         let assume_m_old   := Stmt.cmd (HasPassiveCmds.assume
           s!"assume_measure_{loop_num}" (HasIntOrder.eq m_old_expr m) md)
         let assert_lb      := Stmt.cmd (HasPassiveCmds.assert
@@ -148,7 +150,30 @@ def Stmt.removeLoopsM
       Stmt.cmd (HasPassiveCmds.assume s!"invariant_{loop_num}_{i}" inv md)
     let exit_state_assumes := [havocd, not_guard] ++ invariant_assumes
     let loop_passive :=
-      .ite guard (arbitrary_iter_facts :: exit_state_assumes) [] {}
+      .ite (.det g) (arbitrary_iter_facts :: exit_state_assumes) [] {}
+    pure (.block s!"loop_{loop_num}" [first_iter_facts, loop_passive] {})
+    | .nondet =>
+    -- Non-deterministic loop: havoc assigned vars, then non-deterministically
+    -- enter the body or exit
+    let body_statements ← Block.removeLoopsM bss
+    let entry_invariants := invariants.mapIdx fun i inv =>
+      Stmt.cmd (HasPassiveCmds.assert s!"entry_invariant_{loop_num}_{i}" inv md)
+    let entry_invariant_assumes := invariants.mapIdx fun i inv =>
+      Stmt.cmd (HasPassiveCmds.assume s!"assume_entry_invariant_{loop_num}_{i}" inv md)
+    let first_iter_facts :=
+      .block s!"first_iter_asserts_{loop_num}" (entry_invariants ++ entry_invariant_assumes) {}
+    let inv_assumes := invariants.mapIdx fun i inv =>
+      Stmt.cmd (HasPassiveCmds.assume s!"assume_invariant_{loop_num}_{i}" inv md)
+    let arbitrary_iter_assumes := .block s!"arbitrary_iter_assumes_{loop_num}" inv_assumes md
+    let maintain_invariants := invariants.mapIdx fun i inv =>
+      Stmt.cmd (HasPassiveCmds.assert s!"arbitrary_iter_maintain_invariant_{loop_num}_{i}" inv md)
+    let arbitrary_iter_facts := .block s!"arbitrary_iter_facts_{loop_num}"
+      ([havocd, arbitrary_iter_assumes] ++ body_statements ++ maintain_invariants) {}
+    let invariant_assumes := invariants.mapIdx fun i inv =>
+      Stmt.cmd (HasPassiveCmds.assume s!"invariant_{loop_num}_{i}" inv md)
+    let exit_state_assumes := [havocd] ++ invariant_assumes
+    let loop_passive :=
+      .ite .nondet (arbitrary_iter_facts :: exit_state_assumes) [] {}
     pure (.block s!"loop_{loop_num}" [first_iter_facts, loop_passive] {})
   | .ite c tss ess md => do
     let tss ← Block.removeLoopsM tss
diff --git a/Strata/Transform/PrecondElim.lean b/Strata/Transform/PrecondElim.lean
index afdd200dc..361e61a51 100644
--- a/Strata/Transform/PrecondElim.lean
+++ b/Strata/Transform/PrecondElim.lean
@@ -79,13 +79,13 @@ Collect assertions for all expressions in a command.
 def collectCmdPrecondAsserts (F : @Lambda.Factory CoreLParams)
   (cmd : Imperative.Cmd Expression) : List Statement :=
   match cmd with
-  | .init _ _ (some e) md => collectPrecondAsserts F e "init" md
-  | .init _ _ _ _ => []
-  | .set x e md => collectPrecondAsserts F e s!"set_{x.name}" md
+  | .init _ _ (.det e) md => collectPrecondAsserts F e "init" md
+  | .init _ _ .nondet _ => []
+  | .set x (.det e) md => collectPrecondAsserts F e s!"set_{x.name}" md
+  | .set _ .nondet _ => []
   | .assert l e md => collectPrecondAsserts F e s!"assert_{l}" md
   | .assume l e md => collectPrecondAsserts F e s!"assume_{l}" md
   | .cover l e md => collectPrecondAsserts F e s!"cover_{l}" md
-  | .havoc _ _ => []
 
 /--
 Collect assertions for call arguments.
@@ -224,7 +224,9 @@ def transformStmt (s : Statement)
     setFactory savedF
     return (changed, [.block lbl b' md])
   | .ite c thenb elseb md => do
-    let condAsserts := collectPrecondAsserts F c "ite_cond" md
+    let condAsserts := match c with
+      | .det e => collectPrecondAsserts F e "ite_cond" md
+      | .nondet => []
     let savedF ← getFactory
     let (changed, thenb') ← transformStmts thenb
     setFactory savedF
@@ -240,8 +242,12 @@ def transformStmt (s : Statement)
       | none => []
       | some m => collectPrecondAsserts F m "loop_measure_end" md
     let invAsserts := invariant.flatMap (fun inv => collectPrecondAsserts F inv "loop_invariant" md)
-    let guardAsserts := collectPrecondAsserts F guard "loop_guard" md
-    let guardAssertsEnd := collectPrecondAsserts F guard "loop_guard_end" md
+    let guardAsserts := match guard with
+      | .det g => collectPrecondAsserts F g "loop_guard" md
+      | .nondet => []
+    let guardAssertsEnd := match guard with
+      | .det g => collectPrecondAsserts F g "loop_guard_end" md
+      | .nondet => []
     let savedF ← getFactory
     let (changed, body') ← transformStmts body
     setFactory savedF
@@ -263,7 +269,7 @@ def transformStmt (s : Statement)
     | some wfStmts =>
       -- Add init statements for function parameters so they're in scope
       let paramInits := decl.inputs.toList.map fun (name, ty) =>
-        Statement.init name ty none md
+        Statement.init name ty .nondet md
       return (hasPreconds, [.block s!"{funcName}{wfSuffix}" (paramInits ++ wfStmts) md, .funcDecl decl' md])
   | .typeDecl _ _ =>
     return (false, [s])  -- Type declarations pass through unchanged
diff --git a/Strata/Transform/StructuredToUnstructured.lean b/Strata/Transform/StructuredToUnstructured.lean
index 216c6db40..5818a9e68 100644
--- a/Strata/Transform/StructuredToUnstructured.lean
+++ b/Strata/Transform/StructuredToUnstructured.lean
@@ -83,7 +83,10 @@ match ss with
   let (tl, tbs) ← stmtsToBlocks kNext tss exitConts []
   let (fl, fbs) ← stmtsToBlocks kNext fss exitConts []
   -- Flush accumulated commands
-  let (accumEntry, accumBlocks) ← flushCmds "ite$" accum (.some (.condGoto c tl fl)) l
+  let cExpr := match c with
+    | .det e => e
+    | .nondet => HasBool.tt  -- Fallback: treat nondet as true (conservative)
+  let (accumEntry, accumBlocks) ← flushCmds "ite$" accum (.some (.condGoto cExpr tl fl)) l
   pure (accumEntry, accumBlocks ++ tbs ++ fbs ++ bsNext)
 | .loop c m is bss _md :: rest => do
   -- Process rest first
@@ -99,7 +102,7 @@ match ss with
       let mLabel ← StringGenState.gen "loop_measure$"
       let mIdent := HasIdent.ident mLabel
       let mOldExpr := HasFvar.mkFvar mIdent
-      let initCmd  := HasInit.init mIdent HasIntOrder.intTy none MetaData.empty
+      let initCmd  := HasInit.init mIdent HasIntOrder.intTy .nondet MetaData.empty
       let assumeCmd := HasPassiveCmds.assume s!"assume_{mLabel}"
                          (HasIntOrder.eq mOldExpr mExpr) MetaData.empty
       let lbCmd    := HasPassiveCmds.assert s!"measure_lb_{mLabel}"
@@ -115,7 +118,10 @@ match ss with
     is.mapM (fun i => do
       let invLabel ← StringGenState.gen "inv$"
       pure (HasPassiveCmds.assert invLabel i MetaData.empty))
-  let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto c bl kNext })
+  let cExpr := match c with
+    | .det e => e
+    | .nondet => HasBool.tt  -- Fallback: treat nondet as true (conservative)
+  let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto cExpr bl kNext })
   -- Flush accumulated commands
   let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry
   pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext)
diff --git a/StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean b/StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean
index b6848552a..546c52528 100644
--- a/StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean
+++ b/StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean
@@ -61,10 +61,10 @@ open Lambda.LTy.Syntax
 
 def ExampleProgram1 : Imperative.Cmds LExprTP :=
   [.init (Lambda.Identifier.mk "s" ()) mty[bv32]
-    (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0)))
+    (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0)))
     .empty,
    .set (Lambda.Identifier.mk "s" ())
-    (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100))
+    (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100)))
     .empty]
 
 /--
@@ -88,11 +88,11 @@ private def addBV32LExpr (op1 op2 : Lambda.LExprT TestParams.mono) : Lambda.LExp
 
 def ExampleProgram2 : Imperative.Cmds LExprTP :=
   [.init (Lambda.Identifier.mk "s" ()) mty[bv32]
-    (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0)))
+    (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0)))
     .empty,
    .set (Lambda.Identifier.mk "s" ())
-    (addBV32LExpr (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100))
-    (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 200)))
+    (.det (addBV32LExpr (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100))
+    (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 200))))
     .empty]
 
 /--
@@ -110,15 +110,15 @@ info: ok: #[DECL (decl (s : unsignedbv[32])),
 
 def ExampleProgram3 : Imperative.Cmds LExprTP :=
   [.init (Lambda.Identifier.mk "x" ()) mty[bv32]
-    (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0)))
+    (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0)))
     .empty,
    .init (Lambda.Identifier.mk "y" ()) mty[bv32]
-    (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0)))
+    (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0)))
     .empty,
-   .havoc (Lambda.Identifier.mk "x" ()) .empty,
-   .havoc (Lambda.Identifier.mk "y" ()) .empty,
+   .set (Lambda.Identifier.mk "x" ()) .nondet .empty,
+   .set (Lambda.Identifier.mk "y" ()) .nondet .empty,
    .init (Lambda.Identifier.mk "z" ()) mty[bv32]
-    (some (addBV32LExpr (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "x" ()) (some mty[bv32])) (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "y" ()) (some mty[bv32]))))
+    (.det (addBV32LExpr (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "x" ()) (some mty[bv32])) (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "y" ()) (some mty[bv32]))))
     .empty]
 
 /--
@@ -142,8 +142,8 @@ info: ok: #[DECL (decl (x : unsignedbv[32])),
 /-- Test block statement transformation -/
 def ExampleStmt1 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
   [.block "test_block"
-    [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))) {}),
-     .cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)) {})]
+    [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))) {}),
+     .cmd (.set (Lambda.Identifier.mk "x" ()) (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20))) {})]
     {}]
 
 /--
@@ -161,12 +161,12 @@ info: ok: #[LOCATION skip,
 
 /-- Test if-then-else (ite) statement transformation -/
 def ExampleStmt2 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
-  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
-   .cmd (.init (Lambda.Identifier.mk "y" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
-   .ite
-     (.const { underlying := (), type := mty[bool] } (.boolConst true))
-     [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10)) {})]
-     [.cmd (.set (Lambda.Identifier.mk "y" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)) {})]
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .cmd (.init (Lambda.Identifier.mk "y" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .ite (.det
+     (.const { underlying := (), type := mty[bool] } (.boolConst true)))
+     [.cmd (.set (Lambda.Identifier.mk "x" ()) (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))) {})]
+     [.cmd (.set (Lambda.Identifier.mk "y" ()) (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20))) {})]
      {}]
 
 /--
@@ -189,14 +189,14 @@ info: ok: #[DECL (decl (x : unsignedbv[32])),
 
 /-- Test loop statement transformation -/
 def ExampleStmt3 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
-  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
-   .loop
-     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .loop (.det
+     (.const { underlying := (), type := mty[bool] } (.boolConst true)))
      none
      []
-     [.cmd (.set (Lambda.Identifier.mk "i" ()) (addBV32LExpr
+     [.cmd (.set (Lambda.Identifier.mk "i" ()) (.det (addBV32LExpr
        (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))
-       (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1))) {})]
+       (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1)))) {})]
      {}]
 
 /--
@@ -217,10 +217,10 @@ info: ok: #[DECL (decl (i : unsignedbv[32])),
 /-- Test nested control flow: if inside block -/
 def ExampleStmt4 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
   [.block "outer"
-    [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
-     .ite
-       (.const { underlying := (), type := mty[bool] } (.boolConst true))
-       [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100)) {})]
+    [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+     .ite (.det
+       (.const { underlying := (), type := mty[bool] } (.boolConst true)))
+       [.cmd (.set (Lambda.Identifier.mk "x" ()) (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100))) {})]
        []
        {}]
     {}]
@@ -244,11 +244,11 @@ info: ok: #[LOCATION skip,
 
 /-- Test exit statement transformation -/
 def ExampleStmt5 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
-  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
    .exit (some "target_label") {},
-   .cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10)) {}),
+   .cmd (.set (Lambda.Identifier.mk "x" ()) (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))) {}),
    .block "target_label"
-     [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)) {})]
+     [.cmd (.set (Lambda.Identifier.mk "x" ()) (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20))) {})]
      {}]
 
 /--
@@ -268,22 +268,22 @@ info: ok: #[DECL (decl (x : unsignedbv[32])),
 
 /-- Test complex nested control flow: loop with if inside -/
 def ExampleStmt6 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
-  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
-   .cmd (.init (Lambda.Identifier.mk "sum" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
-   .loop
-     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .cmd (.init (Lambda.Identifier.mk "sum" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .loop (.det
+     (.const { underlying := (), type := mty[bool] } (.boolConst true)))
      none
      []
-     [.ite
-       (.const { underlying := (), type := mty[bool] } (.boolConst true))
-       [.cmd (.set (Lambda.Identifier.mk "sum" ()) (addBV32LExpr
+     [.ite (.det
+       (.const { underlying := (), type := mty[bool] } (.boolConst true)))
+       [.cmd (.set (Lambda.Identifier.mk "sum" ()) (.det (addBV32LExpr
          (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "sum" ()) (some mty[bv32]))
-         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))) {})]
+         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32])))) {})]
        []
        {},
-      .cmd (.set (Lambda.Identifier.mk "i" ()) (addBV32LExpr
+      .cmd (.set (Lambda.Identifier.mk "i" ()) (.det (addBV32LExpr
         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))
-        (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1))) {})]
+        (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1)))) {})]
      {}]
 
 /--
@@ -311,16 +311,16 @@ info: ok: #[DECL (decl (i : unsignedbv[32])),
 /-- Test multiple blocks in sequence -/
 def ExampleStmt7 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
   [.block "block1"
-     [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))) {})]
+     [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))) {})]
      {},
    .block "block2"
-     [.cmd (.init (Lambda.Identifier.mk "y" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20))) {})]
+     [.cmd (.init (Lambda.Identifier.mk "y" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20))) {})]
      {},
    .block "block3"
      [.cmd (.set (Lambda.Identifier.mk "x" ())
-       (addBV32LExpr
+       (.det (addBV32LExpr
          (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "x" ()) (some mty[bv32]))
-         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "y" ()) (some mty[bv32]))) {})]
+         (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "y" ()) (some mty[bv32])))) {})]
      {}]
 
 /--
@@ -344,11 +344,11 @@ info: ok: #[LOCATION skip,
 
 /-- Test empty branches in if-then-else -/
 def ExampleStmt8 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
-  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
-   .ite
-     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .ite (.det
+     (.const { underlying := (), type := mty[bool] } (.boolConst true)))
      []
-     [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100)) {})]
+     [.cmd (.set (Lambda.Identifier.mk "x" ()) (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100))) {})]
      {}]
 
 /--
@@ -368,8 +368,8 @@ info: ok: #[DECL (decl (x : unsignedbv[32])),
 
 /-- Test loop with empty body -/
 def ExampleStmt9 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
-  [.loop
-     (.const { underlying := (), type := mty[bool] } (.boolConst false))
+  [.loop (.det
+     (.const { underlying := (), type := mty[bool] } (.boolConst false)))
      none
      []
      []
@@ -386,11 +386,11 @@ info: ok: #[LOCATION skip, GOTO skip [((not(false : bool)) : bool)], GOTO skip,
 
 /-- Test assertions and assumptions within control flow -/
 def ExampleStmt10 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
-  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 5))) {}),
-   .ite
-     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+  [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 5))) {}),
+   .ite (.det
+     (.const { underlying := (), type := mty[bool] } (.boolConst true)))
      [.cmd (.assume "precond" (.const { underlying := (), type := mty[bool] } (.boolConst true)) {}),
-      .cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10)) {}),
+      .cmd (.set (Lambda.Identifier.mk "x" ()) (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))) {}),
       .cmd (.assert "postcond" (.const { underlying := (), type := mty[bool] } (.boolConst true)) {})]
      []
      {}]
@@ -445,14 +445,14 @@ info: ok: #[ASSERT skip]
 
 -- Test loop with invariant attaches #spec_loop_invariant to backward GOTO
 def ExampleLoopInvariant : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
-  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (some (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
-   .loop
-     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+  [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (.det (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))) {}),
+   .loop (.det
+     (.const { underlying := (), type := mty[bool] } (.boolConst true)))
      none
      [(.const { underlying := (), type := mty[bool] } (.boolConst true))]  -- invariant: true
-     [.cmd (.set (Lambda.Identifier.mk "i" ()) (addBV32LExpr
+     [.cmd (.set (Lambda.Identifier.mk "i" ()) (.det (addBV32LExpr
        (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))
-       (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1))) {})]
+       (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1)))) {})]
      {}]
 
 /--
@@ -485,10 +485,10 @@ info: ok: #[DECL (decl (i : unsignedbv[32])),
 private def ExampleLoopMeasure : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
   open Lambda.LTy.Syntax Lambda.LExpr.Syntax in
   [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[int]
-     (some (.const { underlying := (), type := mty[int] } (.intConst 10))) {}),
+     (.det (.const { underlying := (), type := mty[int] } (.intConst 10))) {}),
    .loop
      -- guard: true
-     (.const { underlying := (), type := mty[bool] } (.boolConst true))
+     (.det (.const { underlying := (), type := mty[bool] } (.boolConst true)))
      -- measure: i
      (some (.fvar { underlying := (), type := mty[int] } (Lambda.Identifier.mk "i" ()) (some mty[int])))
      -- invariants: [true]
diff --git a/StrataTest/DL/Imperative/Arith.lean b/StrataTest/DL/Imperative/Arith.lean
index 5cec3b39d..61b7fa404 100644
--- a/StrataTest/DL/Imperative/Arith.lean
+++ b/StrataTest/DL/Imperative/Arith.lean
@@ -19,8 +19,8 @@ def typeCheckAndPartialEval (cmds : Commands) : Except Format (Commands × Eval.
   return (cmds, S)
 
 private def testProgram1 : Commands :=
-  [.init "x" .Num (some (.Var "y" (.some .Num))) .empty,
-   .havoc "x" .empty,
+  [.init "x" .Num (.det (.Var "y" (.some .Num))) .empty,
+   .set "x" .nondet .empty,
    .assert "x_value_eq" (.Eq (.Var "x" .none) (.Var "y" none)) .empty]
 
 /--
@@ -48,8 +48,8 @@ genNum: 1
 
 
 private def testProgram2 : Commands :=
-  [.init "x" .Num (some (.Num 0)) .empty,
-   .set "x" (.Plus (.Var "x" .none) (.Num 100)) .empty,
+  [.init "x" .Num (.det (.Num 0)) .empty,
+   .set "x" (.det (.Plus (.Var "x" .none) (.Num 100))) .empty,
    .assert "x_value_eq" (.Eq (.Var "x" .none) (.Num 100)) .empty]
 
 /--
diff --git a/StrataTest/DL/Imperative/ArithEval.lean b/StrataTest/DL/Imperative/ArithEval.lean
index 9cd1e3f40..a697176a2 100644
--- a/StrataTest/DL/Imperative/ArithEval.lean
+++ b/StrataTest/DL/Imperative/ArithEval.lean
@@ -170,8 +170,8 @@ instance : ToFormat (Cmds PureExpr × State) where
 /- Tests -/
 
 private def testProgram1 : Cmds PureExpr :=
-  [.init "x" .Num (some (.Num 0)) .empty,
-   .set "x" (.Plus (.Var "x" .none) (.Num 100)) .empty,
+  [.init "x" .Num (.det (.Num 0)) .empty,
+   .set "x" (.det (.Plus (.Var "x" .none) (.Num 100))) .empty,
    .assert "x_value_eq" (.Eq (.Var "x" .none) (.Num 100)) .empty]
 
 /--
@@ -198,8 +198,8 @@ genNum: 0
 
 
 private def testProgram2 : Cmds PureExpr :=
-  [.init "x" .Num (some (.Var "y" .none)) .empty,
-   .havoc "x" .empty,
+  [.init "x" .Num (.det (.Var "y" .none)) .empty,
+   .set "x" .nondet .empty,
    .assert "x_value_eq" (.Eq (.Var "x" .none) (.Num 100)) .empty]
 
 /--
diff --git a/StrataTest/DL/Imperative/ArithType.lean b/StrataTest/DL/Imperative/ArithType.lean
index 4d82c7c22..c0cd92f18 100644
--- a/StrataTest/DL/Imperative/ArithType.lean
+++ b/StrataTest/DL/Imperative/ArithType.lean
@@ -49,8 +49,8 @@ def inferType (T : TEnv) (c : Cmd PureExpr) (e : Expr) : Except DiagnosticModel
     let T ← match c with
       | .init _ _ init_e _ =>
         match init_e with
-        | none => .ok T
-        | some e =>
+        | .nondet => .ok T
+        | .det e =>
           let init_e_fvs := Expr.freeVars e
           if init_e_fvs.any (fun (_, ty) => ty.isNone) then
             .error (DiagnosticModel.fromFormat f!"Cannot infer the types of free variables in the initialization expression!\n\
@@ -118,8 +118,8 @@ instance : ToFormat (Cmds PureExpr × TEnv) where
 ---------------------------------------------------------------------
 
 private def testProgram1 : Cmds Arith.PureExpr :=
-  [.init "x" .Num (some (.Num 0)) .empty,
-   .set "x" (.Plus (.Var "x" .none) (.Num 100)) .empty,
+  [.init "x" .Num (.det (.Num 0)) .empty,
+   .set "x" (.det (.Plus (.Var "x" .none) (.Num 100))) .empty,
    .assert "x_value_eq" (.Eq (.Var "x" .none) (.Num 100)) .empty]
 
 /--
@@ -136,7 +136,7 @@ TEnv:
           return format (cs, τ)
 
 private def testProgram2 : Cmds Arith.PureExpr :=
-  [.init "x" .Bool (some (.Num 0)) .empty]
+  [.init "x" .Bool (.det (.Num 0)) .empty]
 
 /-- info: error: Types .Bool and Num cannot be unified! -/
 #guard_msgs in
@@ -144,7 +144,7 @@ private def testProgram2 : Cmds Arith.PureExpr :=
           return format (cs, τ)
 
 private def testProgram3 : Cmds Arith.PureExpr :=
-  [.init "x" .Bool (some (.Var "x" .none)) .empty]
+  [.init "x" .Bool (.det (.Var "x" .none)) .empty]
 
 /-- info: error: Variable x cannot appear in its own initialization expression! -/
 #guard_msgs in
@@ -152,8 +152,8 @@ private def testProgram3 : Cmds Arith.PureExpr :=
           return format (cs, τ)
 
 private def testProgram4 : Cmds Arith.PureExpr :=
-  [.init "x" .Num (some (.Num 5)) .empty,
-   .set "x" (.Var "x" .none) .empty]
+  [.init "x" .Num (.det (.Num 5)) .empty,
+   .set "x" (.det (.Var "x" .none)) .empty]
 
 /--
 info: ok: Commands:
@@ -169,8 +169,8 @@ TEnv:
 
 
 private def testProgram5 : Cmds Arith.PureExpr :=
-  [.init "x" .Num (some (.Num 5)) .empty,
-   .init "x" .Bool (some (.Eq (.Num 1) (.Num 2))) .empty]
+  [.init "x" .Num (.det (.Num 5)) .empty,
+   .init "x" .Bool (.det (.Eq (.Num 1) (.Num 2))) .empty]
 
 /-- info: error: Variable x of type Num already in context. -/
 #guard_msgs in
@@ -178,7 +178,7 @@ private def testProgram5 : Cmds Arith.PureExpr :=
           return format (cs, τ)
 
 private def testProgram6 : Cmds Arith.PureExpr :=
-  [.init "x" .Num (some (.Var "y" .none)) .empty]
+  [.init "x" .Num (.det (.Var "y" .none)) .empty]
 
 /--
 info: error: Cannot infer the types of free variables in the initialization expression!
@@ -189,7 +189,7 @@ y
           return format (cs, τ)
 
 private def testProgram7 : Cmds Arith.PureExpr :=
-  [.init "x" .Num (some (.Plus (.Var "y" (some .Num)) (.Var "z" (some .Num)))) .empty]
+  [.init "x" .Num (.det (.Plus (.Var "y" (some .Num)) (.Var "z" (some .Num)))) .empty]
 
 /--
 info: ok: Commands:
@@ -203,8 +203,8 @@ TEnv:
           return format (cs, τ)
 
 private def testProgram8 : Cmds Arith.PureExpr :=
-  [.init "x" .Num (some (.Num 1)) .empty,
-   .set "x" (.Var "y" (some .Num)) .empty]
+  [.init "x" .Num (.det (.Num 1)) .empty,
+   .set "x" (.det (.Var "y" (some .Num))) .empty]
 
 /-- info: error: Variable y not found in type context! -/
 #guard_msgs in
diff --git a/StrataTest/DL/Imperative/DDMTranslate.lean b/StrataTest/DL/Imperative/DDMTranslate.lean
index 733e4e544..7e06275df 100644
--- a/StrataTest/DL/Imperative/DDMTranslate.lean
+++ b/StrataTest/DL/Imperative/DDMTranslate.lean
@@ -50,7 +50,7 @@ instance : ToFormat TransBindings where
                  varGen: {b.varGen}"
 
 instance : Inhabited (TransBindings × Arith.Command) where
-  default := ({}, .havoc "default_var" .empty)
+  default := ({}, .set "default_var" .nondet .empty)
 
 /--
 info: inductive ArithPrograms.ArithProgramsType : Type → Type
@@ -139,7 +139,7 @@ ArithPrograms.Command.havoc : {α : Type} → α → Strata.Ann String α → Co
 #print Command
 
 instance : Inhabited (Arith.Command × TransBindings) where
-  default := (.havoc "default" .empty, {})
+  default := (.set "default" .nondet .empty, {})
 
 instance : Inhabited (Arith.Commands × TransBindings) where
   default := ([], {})
@@ -151,15 +151,15 @@ def translateCommand (bindings : TransBindings) (c : ArithPrograms.Command α) :
     let bindings := { bindings with freeVars := bindings.freeVars ++ [name.val] }
     let tp := translateType tp
     let (init_var_name, bindings) := genInitVar bindings name.val
-    return ((.init name.val tp (some (.Var init_var_name tp)) .empty), bindings)
+    return ((.init name.val tp (.det (.Var init_var_name tp)) .empty), bindings)
   | .init _ name tp expr =>
     let tp := translateType tp
     let expr ← translateExpr bindings expr
     let bindings := { bindings with freeVars := bindings.freeVars ++ [name.val] }
-    return ((.init name.val tp (some expr) .empty), bindings)
+    return ((.init name.val tp (.det expr) .empty), bindings)
   | .assign _ label expr =>
     let expr ← translateExpr bindings expr
-    return ((.set label.val expr .empty), bindings)
+    return ((.set label.val (.det expr) .empty), bindings)
   | .assume _ label expr =>
     let label ← translateLabel bindings label
     let expr ← translateExpr bindings expr
@@ -169,7 +169,7 @@ def translateCommand (bindings : TransBindings) (c : ArithPrograms.Command α) :
     let expr ← translateExpr bindings expr
     return ((.assert label expr .empty), bindings)
   | .havoc _ name =>
-    return ((.havoc name.val .empty), bindings)
+    return ((.set name.val .nondet .empty), bindings)
 
 partial def translateProgram (ops : Array Strata.Operation) : TransM Arith.Commands := do
   let (cmds, _) ← go 0 ops.size {} ops
diff --git a/StrataTest/DL/Imperative/FormatStmtTest.lean b/StrataTest/DL/Imperative/FormatStmtTest.lean
index 97e14aee7..3f98ccb78 100644
--- a/StrataTest/DL/Imperative/FormatStmtTest.lean
+++ b/StrataTest/DL/Imperative/FormatStmtTest.lean
@@ -29,7 +29,7 @@ private def xEq1 : E := .eq () x int1
 
 -- 1. cmd: init
 /-- info: init (x : int) := #0 -/
-#guard_msgs in #eval! format (Statement.init "x" intTy int0 .empty : S)
+#guard_msgs in #eval! format (Statement.init "x" intTy (.det int0) .empty : S)
 
 -- 2. cmd: set
 /-- info: x := #42 -/
@@ -72,7 +72,7 @@ info: myBlock :
 #eval! format (Stmt.block "myBlock" ([Statement.set "x" int1 .empty,
                                       Statement.assert "check" xEq1 .empty] : Ss) .empty : S)
 
-def p := (Stmt.ite xEq0
+def p := (Stmt.ite (.det xEq0)
                 ([Statement.set "y" int1 .empty] : Ss)
                 ([Statement.set "y" int2 .empty] : Ss)
                 .empty : S)
@@ -114,7 +114,7 @@ else {
 info: if #true {}
 else {}
 -/
-#guard_msgs in #eval! format (Stmt.ite tt ([] : Ss) ([] : Ss) .empty : S)
+#guard_msgs in #eval! format (Stmt.ite (.det tt) ([] : Ss) ([] : Ss) .empty : S)
 
 -- 12. loop: no measure, no invariant
 /--
@@ -127,7 +127,7 @@ info: while
 }
 -/
 #guard_msgs in
-#eval! format (Stmt.loop xEq0 none []
+#eval! format (Stmt.loop (.det xEq0) none []
                 ([Statement.set "x" int1 .empty] : Ss) .empty : S)
 
 -- 13. loop: with measure and invariant
@@ -141,7 +141,7 @@ info: while
 }
 -/
 #guard_msgs in
-#eval! format (Stmt.loop xEq0 (some x) [tt]
+#eval! format (Stmt.loop (.det xEq0) (some x) [tt]
                 ([Statement.set "x" int1 .empty] : Ss) .empty : S)
 
 -- 14. exit with label
diff --git a/StrataTest/Languages/Core/Tests/CmdEvalTests.lean b/StrataTest/Languages/Core/Tests/CmdEvalTests.lean
index 2c93a0c1d..47a21ebf6 100644
--- a/StrataTest/Languages/Core/Tests/CmdEvalTests.lean
+++ b/StrataTest/Languages/Core/Tests/CmdEvalTests.lean
@@ -14,8 +14,8 @@ open Std (ToFormat Format format)
 open LExpr.SyntaxMono LTy.Syntax Core.Syntax
 
 private def testProgram1 : Cmds Expression :=
-  [.init "x" t[int] (some eb[#0]) .empty,
-   .set "x" eb[#10] .empty,
+  [.init "x" t[int] (.det eb[#0]) .empty,
+   .set "x" (.det eb[#10]) .empty,
    .assert "x_value_eq" eb[x == #10] .empty]
 
 /--
@@ -59,7 +59,7 @@ Proof Obligation:
 #eval format $ Imperative.Cmds.eval (Env.init (empty_factory := true)) testProgram1
 
 private def testProgram2 : Cmds Expression :=
-  [.init "x" t[int] (some eb[(y : int)]) .empty,
+  [.init "x" t[int] (.det eb[(y : int)]) .empty,
    .assert "x_eq_12" eb[x == #12] .empty]
 
 /--
diff --git a/StrataTest/Languages/Core/Tests/ProgramTypeTests.lean b/StrataTest/Languages/Core/Tests/ProgramTypeTests.lean
index b7f27519a..ba6c00372 100644
--- a/StrataTest/Languages/Core/Tests/ProgramTypeTests.lean
+++ b/StrataTest/Languages/Core/Tests/ProgramTypeTests.lean
@@ -325,11 +325,11 @@ def outOfScopeVarProg : Program := { decls := [
                   postconditions := [] },
               body := [
                 Statement.set "y" eb[((~Bool.Or x) x)] .empty,
-                .ite eb[(x == #true)]
-                  [Statement.init "q" t[int] (some eb[#0]) .empty,
+                .ite (.det eb[(x == #true)])
+                  [Statement.init "q" t[int] (.det eb[#0]) .empty,
                            Statement.set "q" eb[#1] .empty,
                            Statement.set "y" eb[#true] .empty]
-                  [Statement.init "q" t[int] (some eb[#0]) .empty,
+                  [Statement.init "q" t[int] (.det eb[#0]) .empty,
                            Statement.set "q" eb[#2] .empty,
                            Statement.set "y" eb[#true] .empty]
                   .empty,
@@ -370,7 +370,7 @@ def polyFuncProg : Program := { decls := [
                     postconditions := [] },
           body := [
             -- var m : Map int bool;
-            Statement.init "m" (.forAll [] (.tcons "Map" [.tcons "int" [], .tcons "bool" []])) none .empty,
+            Statement.init "m" (.forAll [] (.tcons "Map" [.tcons "int" [], .tcons "bool" []])) Imperative.ExprOrNondet.nondet .empty,
             -- m := makePair(identity(42), identity(true));
             Statement.set "m" eb[((~makePair (~identity #42)) (~identity #true))] .empty
           ]
diff --git a/StrataTest/Languages/Core/Tests/StatementEvalTests.lean b/StrataTest/Languages/Core/Tests/StatementEvalTests.lean
index 7f33c7348..3db7961f9 100644
--- a/StrataTest/Languages/Core/Tests/StatementEvalTests.lean
+++ b/StrataTest/Languages/Core/Tests/StatementEvalTests.lean
@@ -47,7 +47,7 @@ Proof Obligation:
 #true
 -/
 #guard_msgs in
-#eval (evalOne ∅ ∅ [.init "x" t[int] (some eb[#0]) .empty,
+#eval (evalOne ∅ ∅ [.init "x" t[int] (.det eb[#0]) .empty,
                     .set "x" eb[#18] .empty,
                     .assert "x_eq_18" eb[x == #18] .empty]) |>.snd |> format
 
@@ -87,7 +87,7 @@ Proof Obligation:
 #eval (evalOne
   ((Env.init (empty_factory := true)).pushScope [("y", (mty[int], eb[_yinit]))])
   ∅
-  [.init "x" t[int] (some eb[#0]) .empty,
+  [.init "x" t[int] (.det eb[#0]) .empty,
   .set "x" eb[y] .empty,
   .assert "x_eq_12" eb[x == #12] .empty]) |>.snd |> format
 
@@ -122,7 +122,7 @@ Deferred Proof Obligations:
 -- though because `x` can't appear in its own initialization expression.
 #eval evalOne ∅ ∅
        [
-       .init "x" t[bool] (some eb[x == #true]) .empty
+       .init "x" t[bool] (.det eb[x == #true]) .empty
        ] |>.snd |> format
 
 /--
@@ -178,8 +178,8 @@ Proof Obligation:
   ((Env.init (empty_factory := true)).pushScope
     [("minit", (mty[int → int], eb[(_minit : int → int)]))])
   ∅
-  [.init "m" t[int → int] (some eb[minit]) .empty,
-  .init "m0" t[int] (some eb[(m #0)]) .empty,
+  [.init "m" t[int → int] (.det eb[minit]) .empty,
+  .init "m0" t[int] (.det eb[(m #0)]) .empty,
   .set "m" eb[λ (if (%0 == #1) then #10 else ((m : int → int) %0))] .empty,
   .set "m" eb[λ (if (%0 == #2) then #20 else ((m : int → int) %0))] .empty,
   .assert "m_5_eq_50" eb[(m #5) == #50] .empty,
@@ -239,7 +239,7 @@ Proof Obligation:
 #eval (evalOne
   ((Env.init (empty_factory := true)).pushScope [("minit", (none, eb[_minit]))])
   ∅
-  [.init "m" t[int → int] (some eb[minit]) .empty,
+  [.init "m" t[int → int] (.det eb[minit]) .empty,
   .set "m" eb[λ (if (%0 == #1) then #10 else (m %0))] .empty,
   .set "m" eb[λ (if (%0 == #2) then #20 else (m %0))] .empty,
   .assert "m_5_eq_50" eb[(m #5) == #50] .empty,
@@ -252,14 +252,14 @@ Proof Obligation:
 
 private def prog1 : Statements :=
  [
- .init "x" t[int] (some eb[#0]) .empty,
- .init "y" t[int] (some eb[#6]) .empty,
+ .init "x" t[int] (.det eb[#0]) .empty,
+ .init "y" t[int] (.det eb[#6]) .empty,
  .block "label_0"
 
-   [Statement.init "z" t[bool] (some eb[zinit]) .empty,
+   [Statement.init "z" t[bool] (.det eb[zinit]) .empty,
     Statement.assume "z_false" eb[z == #false] .empty,
 
-   .ite eb[z == #false]
+   .ite (.det eb[z == #false])
      [Statement.set "x" eb[y] .empty]
      -- The "trivial" assertion, though unreachable, is still verified away by the
      -- PE because the conclusion of the proof obligation evaluates to `true`.
@@ -333,7 +333,7 @@ Proof Obligation:
 
 
 private def prog2 : Statements := [
-  .init "x" t[int] (some eb[#0]) .empty,
+  .init "x" t[int] (.det eb[#0]) .empty,
   .set "x" eb[#1] .empty,
   .havoc "x" .empty,
   .assert "x_eq_1" eb[x == #1] .empty, -- error
@@ -405,7 +405,7 @@ def testFuncDecl : List Statement :=
   }
   [
     .funcDecl doubleFunc .empty,
-    .init "y" t[int] (some eb[(~double #5)]) .empty,
+    .init "y" t[int] (.det eb[(~double #5)]) .empty,
     .assert "y_eq_10" eb[y == #10] .empty
   ]
 
@@ -461,10 +461,10 @@ def testFuncDeclSymbolic : List Statement :=
     axioms := []
   }
   [
-    .init "n" t[int] (some eb[#10]) .empty,  -- Initialize n to 10
+    .init "n" t[int] (.det eb[#10]) .empty,  -- Initialize n to 10
     .funcDecl addNFunc .empty,  -- Function captures n = 10 at declaration time
     .set "n" eb[#20] .empty,  -- Mutate n to 20
-    .init "result" t[int] (some eb[(~addN #5)]) .empty,  -- Call function
+    .init "result" t[int] (.det eb[(~addN #5)]) .empty,  -- Call function
     .assert "result_eq_15" eb[result == #15] .empty  -- Result is 5 + 10 = 15 (uses captured value)
   ]
 
@@ -531,10 +531,10 @@ def testPolymorphicFuncDecl : List Statement :=
   [
     .funcDecl chooseFunc .empty,
     -- Use with int type (curried application)
-    .init "intResult" t[int] (some eb[(((~choose #true) #1) #2)]) .empty,
+    .init "intResult" t[int] (.det eb[(((~choose #true) #1) #2)]) .empty,
     .assert "intResult_eq_1" eb[intResult == #1] .empty,
     -- Use with bool type (curried application)
-    .init "boolResult" t[bool] (some eb[(((~choose #false) #true) #false)]) .empty,
+    .init "boolResult" t[bool] (.det eb[(((~choose #false) #true) #false)]) .empty,
     .assert "boolResult_eq_false" eb[boolResult == #false] .empty
   ]
 
diff --git a/StrataTest/Languages/Core/Tests/StatementTypeTests.lean b/StrataTest/Languages/Core/Tests/StatementTypeTests.lean
index 946bfd45d..470bd0869 100644
--- a/StrataTest/Languages/Core/Tests/StatementTypeTests.lean
+++ b/StrataTest/Languages/Core/Tests/StatementTypeTests.lean
@@ -27,9 +27,9 @@ info: ok: {
 #eval do let ans ← typeCheck LContext.default (TEnv.default.updateContext {types := [[("xinit", t[int])]] })
                    Program.init
                    none
-                   [.init "x" t[int] (some eb[xinit]) .empty,
+                   [.init "x" t[int] (.det eb[xinit]) .empty,
                     .set "x" eb[xinit] .empty,
-                    .init "y" t[∀α. %α] (some eb[xinit]) .empty]
+                    .init "y" t[∀α. %α] (.det eb[xinit]) .empty]
          return format ans.fst
 
 
@@ -39,7 +39,7 @@ info: ok: {
                    Program.init
                    none
                    [
-                    .init "x" t[bool] (some eb[#true]) .empty
+                    .init "x" t[bool] (.det eb[#true]) .empty
                    ]
          return format ans
 
@@ -59,14 +59,14 @@ subst:
                     Program.init
                     none
                     [
-                    .init "x" t[int] (some eb[#0]) .empty,
-                    .init "y" t[int] (some eb[#6]) .empty,
+                    .init "x" t[int] (.det eb[#0]) .empty,
+                    .init "y" t[int] (.det eb[#6]) .empty,
                     .block "label_0"
 
-                      [Statement.init "z" t[bool] (some eb[zinit]) .empty,
+                      [Statement.init "z" t[bool] (.det eb[zinit]) .empty,
                        Statement.assume "z_false" eb[z == #false] .empty,
 
-                      .ite eb[z == #false]
+                      .ite (.det eb[z == #false])
                         [Statement.set "x" eb[y] .empty]
                         [Statement.assert "trivial" eb[#true] .empty]
                         .empty,
@@ -82,9 +82,9 @@ subst:
 #guard_msgs in
 #eval do let ans ← typeCheck LContext.default TEnv.default Program.init none
                     [
-                    .init "x" t[int] (some eb[#0]) .empty,
-                    .init "y" t[int] (some eb[#6]) .empty,
-                    .init "z" t[bool] (some eb[if (x == y) then #true else #2]) .empty
+                    .init "x" t[int] (.det eb[#0]) .empty,
+                    .init "y" t[int] (.det eb[#6]) .empty,
+                    .init "z" t[bool] (.det eb[if (x == y) then #true else #2]) .empty
                     ]
           return format ans
 
@@ -92,9 +92,9 @@ subst:
 #guard_msgs in
 #eval do let ans ← typeCheck LContext.default TEnv.default Program.init none
                     [
-                    .init "x" t[bool] (some eb[#true]) .empty,
+                    .init "x" t[bool] (.det eb[#true]) .empty,
                     .block "label_0"
-                      [ Statement.init "x" t[int] (some eb[#1]) .empty ]
+                      [ Statement.init "x" t[int] (.det eb[#1]) .empty ]
                       .empty
                     ]
           return format ans
@@ -113,13 +113,13 @@ subst: [($__ty0, int)]
 #guard_msgs in
 #eval do let ans ← typeCheck LContext.default TEnv.default Program.init none
                     [
-                    .init "x" t[int] (some eb[#0]) .empty,
-                    .ite eb[x == #3]
+                    .init "x" t[int] (.det eb[#0]) .empty,
+                    .ite (.det eb[x == #3])
                     [
-                      Statement.init "y" t[∀α. %α] (some eb[x]) .empty,
+                      Statement.init "y" t[∀α. %α] (.det eb[x]) .empty,
                       Statement.assert "local_y_eq_3" eb[y == #3] .empty
                     ]
-                    [ Statement.init "z" t[bool] (some eb[#true]) .empty ]
+                    [ Statement.init "z" t[bool] (.det eb[#true]) .empty ]
                     .empty
                     ]
           return format ans.snd
@@ -133,7 +133,7 @@ info: ok: {
 #guard_msgs in
 #eval do let ans ← typeCheck LContext.default TEnv.default Program.init none
               [
-              .init "x" t[∀a. %a] (some eb[#1]) .empty,
+              .init "x" t[∀a. %a] (.det eb[#1]) .empty,
               .set "x" eb[#2] .empty
               ]
           return (format ans.fst)
@@ -153,8 +153,8 @@ subst: [($__ty0, int) ($__ty2, int) ($__ty6, (arrow bool int)) ($__ty7, bool) ($
 #eval do let ans ← typeCheck LContext.default (TEnv.default.updateContext { types := [[("fn", t[∀a. %a → %a])]] })
                       Program.init none
               [
-              .init "m1" t[∀a. %a → int] (some eb[fn]) .empty, -- var m : <a>[a]int
-              .init "m2" t[∀a. %a → int] (some eb[(λ (%0 (fn #true)))]) .empty,
+              .init "m1" t[∀a. %a → int] (.det eb[fn]) .empty, -- var m : <a>[a]int
+              .init "m2" t[∀a. %a → int] (.det eb[(λ (%0 (fn #true)))]) .empty,
               ]
           return (format ans.snd)
 
@@ -186,7 +186,7 @@ def testFuncDeclTypeCheck : List Statement :=
   }
   [
     .funcDecl identityFunc .empty,
-    .init "y" t[int] (some eb[(~identity #5)]) .empty,  -- Call the declared function
+    .init "y" t[int] (.det eb[(~identity #5)]) .empty,  -- Call the declared function
     .assert "y_eq_5" eb[y == #5] .empty
   ]
 
diff --git a/StrataTest/Transform/DetToNondet.lean b/StrataTest/Transform/DetToNondet.lean
index 36371a5ce..895626835 100644
--- a/StrataTest/Transform/DetToNondet.lean
+++ b/StrataTest/Transform/DetToNondet.lean
@@ -18,12 +18,12 @@ section NondetExamples
 open Imperative
 
 def NondetTest1 : Stmt Expression (Cmd Expression) :=
-  .ite (Core.true) [.cmd $ .havoc "x" .empty ] [.cmd $ .havoc "y" .empty ] .empty
+  .ite (.det Core.true) [.cmd $ .set "x" .nondet .empty ] [.cmd $ .set "y" .nondet .empty ] .empty
 
 def NondetTest1Ans : NondetStmt Expression (Cmd Expression) :=
   .choice
-    (.seq (.cmd (.assume "true_cond" Core.true .empty)) (.seq (.cmd $ .havoc "x" .empty) (.assume "skip" Imperative.HasBool.tt .empty)))
-    (.seq (.cmd (.assume "false_cond" Core.false .empty)) (.seq (.cmd $ .havoc "y" .empty) (.assume "skip" Imperative.HasBool.tt .empty)))
+    (.seq (.cmd (.assume "true_cond" Core.true .empty)) (.seq (.cmd $ .set "x" .nondet .empty) (.assume "skip" Imperative.HasBool.tt .empty)))
+    (.seq (.cmd (.assume "false_cond" Core.false .empty)) (.seq (.cmd $ .set "y" .nondet .empty) (.assume "skip" Imperative.HasBool.tt .empty)))
 
 
 -- #eval toString $ Std.format (StmtToNondetStmt NondetTest1)
diff --git a/StrataTest/Transform/ProcedureInlining.lean b/StrataTest/Transform/ProcedureInlining.lean
index 3d38a17f9..942c2cd7f 100644
--- a/StrataTest/Transform/ProcedureInlining.lean
+++ b/StrataTest/Transform/ProcedureInlining.lean
@@ -126,7 +126,11 @@ def alphaEquivStatement (s1 s2: Core.Statement) (map:IdMap)
     alphaEquivBlock b1 b2 map
 
   | .ite cond1 thenb1 elseb1 _, .ite cond2 thenb2 elseb2 _ => do
-    if alphaEquivExprs cond1 cond2 map then
+    let condsMatch := match cond1, cond2 with
+      | .det e1, .det e2 => alphaEquivExprs e1 e2 map
+      | .nondet, .nondet => true
+      | _, _ => false
+    if condsMatch then
       let map' <- alphaEquivBlock thenb1 thenb2 map
       let map'' <- alphaEquivBlock elseb1 elseb2 map'
       return map''
@@ -134,7 +138,11 @@ def alphaEquivStatement (s1 s2: Core.Statement) (map:IdMap)
       .error "if conditions do not match"
 
   | .loop g1 m1 i1 b1 _, .loop g2 m2 i2 b2 _ =>
-    if ¬ alphaEquivExprs g1 g2 map then
+    let guardsMatch := match g1, g2 with
+      | .det e1, .det e2 => alphaEquivExprs e1 e2 map
+      | .nondet, .nondet => true
+      | _, _ => false
+    if !guardsMatch then
       .error "guard does not match"
     else if ¬ (← alphaEquivExprsOpt m1 m2 map) then
       .error "measure does not match"
@@ -170,7 +178,7 @@ def alphaEquivStatement (s1 s2: Core.Statement) (map:IdMap)
       -- The updateVars below must be the only place that updates the
       -- variable name mapping.
       IdMap.updateVars map [(n1.name,n2.name)]
-    | .cmd (.set n1 e1 _), .cmd (.set n2 e2 _) =>
+    | .cmd (.set n1 (.det e1) _), .cmd (.set n2 (.det e2) _) =>
       if ¬ alphaEquivExprs e1 e2 map then
         mk_err f!"RHS of sets do not match \
         \n(subst of e1: {repr (substExpr e1 map.vars.fst false)})\n(e2: {repr e2})
@@ -179,9 +187,9 @@ def alphaEquivStatement (s1 s2: Core.Statement) (map:IdMap)
         mk_err "LHS of sets do not match"
       else
         return map
-    | .cmd (.havoc n1 _), .cmd (.havoc n2 _) =>
+    | .cmd (.set n1 .nondet _), .cmd (.set n2 .nondet _) =>
       if ¬ alphaEquivIdents n1 n2 map then
-        mk_err "LHS of havocs do not match"
+        mk_err "LHS of sets do not match"
       else
         return map
     | .cmd (.assert _ e1 _), .cmd (.assert _ e2 _) =>