diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 2caa0262..73e47d54 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -105,13 +105,33 @@ jobs:
       run: sbt universal:packageBin
 
   test-macos:
-    runs-on: macos-13
+    runs-on: macos-14
 
     steps:
     - uses: actions/checkout@v2
-    - uses: olafurpg/setup-scala@v10
+
+    - name: Set up JDK 11
+      uses: actions/setup-java@v4
+      with:
+        distribution: 'zulu'
+        java-version: '11'
+
+    - name: Cache SBT ivy cache
+      uses: actions/cache@v4
       with:
-        java-version: openjdk@1.11
+        path: ~/.ivy2/cache
+        key: ${{ runner.os }}-sbt-ivy-cache-${{ hashFiles('**/build.sbt') }}
+
+    - name: Cache SBT
+      uses: actions/cache@v4
+      with:
+        path: ~/.sbt
+        key: ${{ runner.os }}-sbt-${{ hashFiles('**/build.sbt') }}
+
+    - name: Set up SBT
+      uses: coursier/setup-action@v1
+      with:
+        apps: sbt
 
     - name: Cache Z3
       id: cache-z3
diff --git a/build.sbt b/build.sbt
index ada7fdad..dd4aa7ea 100644
--- a/build.sbt
+++ b/build.sbt
@@ -15,6 +15,16 @@ libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.2" % "test"
 libraryDependencies += "com.github.scopt" %% "scopt" % "3.7.1"
 libraryDependencies += "org.json4s" %% "json4s-jackson" % "4.0.3"
 
+// Fork the JVM for run/test so that javaOptions take effect. The java.library.path
+// setting is needed for Z3 JNI native library loading (libz3java). While the setup
+// scripts (setup-z3-linux.sh, etc.) set LD_LIBRARY_PATH for shell use, java.library.path
+// must be set at JVM startup to locate native libraries when running via sbt.
+fork in run := true
+javaOptions in run += s"-Djava.library.path=${baseDirectory.value}/z3/bin"
+
+fork in Test := true
+javaOptions in Test += s"-Djava.library.path=${baseDirectory.value}/z3/bin"
+
 // do not require tests before building a fat JAR
 test in assembly := {}
 
diff --git a/src/main/scala/uclid/IC3Engine.scala b/src/main/scala/uclid/IC3Engine.scala
new file mode 100644
index 00000000..219c346c
--- /dev/null
+++ b/src/main/scala/uclid/IC3Engine.scala
@@ -0,0 +1,543 @@
+/*
+ * UCLID5 Verification and Synthesis Engine
+ *
+ * IC3/PDR (Property Directed Reachability) engine for safety property verification.
+ *
+ */
+
+package uclid
+
+import lang._
+import scala.collection.mutable.{ArrayBuffer, ListBuffer}
+import scala.collection.mutable.{Map => MutableMap}
+import com.typesafe.scalalogging.Logger
+
+class IC3Engine(module: Module, solver: smt.Z3Interface) {
+
+  val log = Logger(classOf[IC3Engine])
+
+  // Create a fresh SymbolicSimulator to extract formulas.
+  val symSim = new SymbolicSimulator(module)
+  val scope = Scope.empty + module
+
+  val passAllFilter: (Identifier, List[ExprDecorator]) => Boolean = (_, _) => true
+
+  // Extract init formula and current-state symbol table.
+  val (initLambda, _, initSymbolTable, _, _) =
+    symSim.getInitLambda(false, false, false, scope, "ic3", passAllFilter, passAllFilter)
+  val initFormula: smt.Expr = initLambda.e
+
+  // Extract transition formula and next-state symbol table.
+  val (transLambda, _, nextSymTab, _, _, _) =
+    symSim.getNextLambda(initSymbolTable, false, false, scope, "ic3", passAllFilter, passAllFilter)
+  val transFormula: smt.Expr = transLambda.e
+
+  // Build mapping from current-state symbols to next-state symbols.
+  val curToNextMap: Map[smt.Symbol, smt.Symbol] = initSymbolTable.flatMap { case (id, curExpr) =>
+    scope.get(id) match {
+      case Some(Scope.StateVar(_, _)) | Some(Scope.OutputVar(_, _)) |
+           Some(Scope.SharedVar(_, _)) | Some(Scope.InputVar(_, _)) =>
+        nextSymTab.get(id).map { nextExpr =>
+          (curExpr.asInstanceOf[smt.Symbol], nextExpr.asInstanceOf[smt.Symbol])
+        }
+      case _ => None
+    }
+  }.toMap
+
+  val nextToCurMap: Map[smt.Symbol, smt.Symbol] = curToNextMap.map(_.swap)
+
+  // State variable symbols for cube extraction (excludes inputs and constants).
+  val stateSymbols: List[smt.Symbol] = initSymbolTable.flatMap { case (id, expr) =>
+    scope.get(id) match {
+      case Some(Scope.StateVar(_, _)) | Some(Scope.OutputVar(_, _)) | Some(Scope.SharedVar(_, _)) =>
+        Some(expr.asInstanceOf[smt.Symbol])
+      case _ => None
+    }
+  }.toList
+
+  // Reverse map: internal symbol name -> user-level variable name (for pretty-printing).
+  val symbolToName: Map[String, String] = initSymbolTable.flatMap { case (id, expr) =>
+    scope.get(id) match {
+      case Some(Scope.StateVar(_, _)) | Some(Scope.OutputVar(_, _)) |
+           Some(Scope.SharedVar(_, _)) | Some(Scope.InputVar(_, _)) =>
+        Some(expr.asInstanceOf[smt.Symbol].id -> id.name)
+      case _ => None
+    }
+  }.toMap
+
+  type Clause = smt.Expr
+  val frames: ArrayBuffer[ArrayBuffer[Clause]] = ArrayBuffer()
+
+  case class ProofObligation(frame: Int, cube: smt.Expr)
+
+  def prime(expr: smt.Expr): smt.Expr = {
+    smt.Context.rewriteExpr(expr, (e: smt.Expr) => e match {
+      case s: smt.Symbol => curToNextMap.getOrElse(s, s)
+      case other => other
+    }, MutableMap.empty)
+  }
+
+  def unprime(expr: smt.Expr): smt.Expr = {
+    smt.Context.rewriteExpr(expr, (e: smt.Expr) => e match {
+      case s: smt.Symbol => nextToCurMap.getOrElse(s, s)
+      case other => other
+    }, MutableMap.empty)
+  }
+
+  def negate(expr: smt.Expr): smt.Expr = {
+    smt.OperatorApplication(smt.NegationOp, List(expr))
+  }
+
+  /** Extract a concrete cube (conjunction of equalities) from a model over state variables.
+   *  Skips symbols whose types can't be evaluated (e.g., arrays, uninterpreted sorts). */
+  def extractConcreteCube(model: smt.Model): smt.Expr = {
+    val lits = stateSymbols.flatMap { sym =>
+      try {
+        val value = model.evaluate(sym)
+        Some(smt.OperatorApplication(smt.EqualityOp, List(sym, value)))
+      } catch {
+        case _: Utils.RuntimeError => None
+      }
+    }
+    if (lits.isEmpty) smt.BooleanLit(true)
+    else if (lits.size == 1) lits.head
+    else smt.OperatorApplication(smt.ConjunctionOp, lits)
+  }
+
+  /** Assert all clauses in a frame. Frame 0 is the init formula. */
+  def assertFrame(frameIdx: Int): Unit = {
+    if (frameIdx == 0) {
+      solver.assert(initFormula)
+    } else {
+      frames(frameIdx).foreach(clause => solver.assert(clause))
+    }
+  }
+
+  /**
+   * Check if a candidate generalization preserves the UNSAT consecution check.
+   * Returns true if the candidate can replace the original literal.
+   */
+  private def checkGeneralizationCandidate(
+    candidate: smt.Expr,
+    otherAssumptions: List[smt.Expr],
+    frame: Int
+  ): Boolean = {
+    val newAssumptions = candidate :: otherAssumptions
+    solver.push()
+    if (frame == 0) solver.assert(initFormula) else assertFrame(frame)
+    solver.assert(negate(unprime(candidate)))
+    solver.assert(transFormula)
+    val result = solver.checkAssumptions(newAssumptions)
+    solver.pop()
+    result.isFalse
+  }
+
+  /**
+   * Try to generalize a primed equality (v' == c) to a sign-based inequality.
+   * Handles integers, reals, and bitvectors.
+   * E.g., if c < 0, try v' < 0 instead of v' == c.
+   * Returns the generalized literal if successful, otherwise the original.
+   */
+  def tryGeneralizeLiteral(
+    primedLit: smt.Expr,
+    otherAssumptions: List[smt.Expr],
+    frame: Int,
+    cube: smt.Expr
+  ): smt.Expr = {
+    primedLit match {
+      // Integer generalization: (sym == intConst) -> (sym < 0) or (sym > 0)
+      case smt.OperatorApplication(smt.EqualityOp, List(sym: smt.Symbol, smt.IntLit(value))) =>
+        if (value == 0) return primedLit
+        val zero = smt.IntLit(BigInt(0))
+        val candidate = if (value < 0) {
+          smt.OperatorApplication(smt.IntLTOp, List(sym, zero))
+        } else {
+          smt.OperatorApplication(smt.IntGTOp, List(sym, zero))
+        }
+        if (checkGeneralizationCandidate(candidate, otherAssumptions, frame)) candidate else primedLit
+
+      // Real number generalization: (sym == realConst) -> (sym < 0.0) or (sym > 0.0)
+      case smt.OperatorApplication(smt.EqualityOp, List(sym: smt.Symbol, smt.RealLit(integral, fractional))) =>
+        val isZero = integral == 0 && fractional.forall(_ == '0')
+        if (isZero) return primedLit
+        val zero = smt.RealLit(BigInt(0), "0")
+        val candidate = if (integral < 0) {
+          smt.OperatorApplication(smt.RealLTOp, List(sym, zero))
+        } else {
+          // integral > 0, or integral == 0 with non-zero fractional part (positive)
+          smt.OperatorApplication(smt.RealGTOp, List(sym, zero))
+        }
+        if (checkGeneralizationCandidate(candidate, otherAssumptions, frame)) candidate else primedLit
+
+      // Bitvector: no sign-based generalization — finite domain works well with
+      // concrete equalities and unsat core minimization.
+      case _ => primedLit
+    }
+  }
+
+  /** Generalize a cube using unsat cores and integer inequality generalization. */
+  def generalize(frame: Int, cube: smt.Expr): smt.Expr = {
+    val literals = cube match {
+      case smt.OperatorApplication(smt.ConjunctionOp, args) => args
+      case other => List(other)
+    }
+
+    val primedLiterals = literals.map(prime)
+
+    // Get unsat core to find minimal set of needed literals.
+    solver.push()
+    if (frame == 0) {
+      solver.assert(initFormula)
+    } else {
+      assertFrame(frame)
+    }
+    solver.assert(negate(cube))
+    solver.assert(transFormula)
+    val result = solver.checkAssumptions(primedLiterals)
+    solver.pop()
+
+    if (result.isFalse) {
+      var coreLiterals = solver.getUnsatCore()
+      if (coreLiterals.isEmpty) coreLiterals = primedLiterals
+
+      // Try to generalize each core literal (integer equalities to inequalities).
+      val generalizedLiterals = coreLiterals.map { lit =>
+        val others = coreLiterals.filter(_ != lit)
+        tryGeneralizeLiteral(lit, others, frame, cube)
+      }
+
+      val unprimedLiterals = generalizedLiterals.map(unprime)
+      val coreConj = if (unprimedLiterals.size == 1) unprimedLiterals.head
+                     else smt.OperatorApplication(smt.ConjunctionOp, unprimedLiterals)
+      negate(coreConj)
+    } else {
+      negate(cube)
+    }
+  }
+
+  /** Substitute symbols in an expression using the given map. */
+  def substitute(expr: smt.Expr, substMap: Map[smt.Symbol, smt.Symbol]): smt.Expr = {
+    smt.Context.rewriteExpr(expr, (e: smt.Expr) => e match {
+      case s: smt.Symbol => substMap.getOrElse(s, s)
+      case other => other
+    }, MutableMap.empty)
+  }
+
+  /**
+   * Build a concrete counterexample trace by doing a BMC-style unrolling.
+   * Returns (stepSymbolTables, model) where stepSymbolTables(i) is the
+   * symbol table at step i, and model provides concrete values.
+   */
+  def buildCexTrace(depth: Int, propExpr: smt.Expr): (ArrayBuffer[SymbolicSimulator.SymbolTable], smt.Model) = {
+    val stepSymTables = ArrayBuffer[SymbolicSimulator.SymbolTable]()
+
+    // Step 0: reuse initSymbolTable symbols (init formula is expressed in these).
+    stepSymTables += initSymbolTable
+
+    // Steps 1..depth: create fresh symbols for state/input/output/shared vars.
+    for (step <- 1 to depth) {
+      val newSymTab = initSymbolTable.map { case (id, expr) =>
+        scope.get(id) match {
+          case Some(Scope.StateVar(_, _)) | Some(Scope.OutputVar(_, _)) |
+               Some(Scope.SharedVar(_, _)) | Some(Scope.InputVar(_, _)) =>
+            val sym = expr.asInstanceOf[smt.Symbol]
+            (id, smt.Symbol(s"ic3_cex_${step}_${sym.id}", sym.symbolTyp).asInstanceOf[smt.Expr])
+          case _ =>
+            (id, expr) // Constants, enums, functions stay the same.
+        }
+      }
+      stepSymTables += newSymTab
+    }
+
+    solver.push()
+
+    // Assert init at step 0.
+    solver.assert(initFormula)
+
+    // Assert transition for each step i -> i+1.
+    for (step <- 0 until depth) {
+      val substMap = scala.collection.mutable.Map[smt.Symbol, smt.Symbol]()
+
+      // Map original current-state symbols to step i symbols.
+      initSymbolTable.foreach { case (id, expr) =>
+        scope.get(id) match {
+          case Some(Scope.StateVar(_, _)) | Some(Scope.OutputVar(_, _)) |
+               Some(Scope.SharedVar(_, _)) | Some(Scope.InputVar(_, _)) =>
+            substMap(expr.asInstanceOf[smt.Symbol]) = stepSymTables(step)(id).asInstanceOf[smt.Symbol]
+          case _ => // skip
+        }
+      }
+
+      // Map original next-state symbols to step i+1 symbols.
+      nextSymTab.foreach { case (id, expr) =>
+        scope.get(id) match {
+          case Some(Scope.StateVar(_, _)) | Some(Scope.OutputVar(_, _)) |
+               Some(Scope.SharedVar(_, _)) | Some(Scope.InputVar(_, _)) =>
+            substMap(expr.asInstanceOf[smt.Symbol]) = stepSymTables(step + 1)(id).asInstanceOf[smt.Symbol]
+          case _ => // skip
+        }
+      }
+
+      solver.assert(substitute(transFormula, substMap.toMap))
+    }
+
+    // Assert ¬P at the last step.
+    val propSubst: Map[smt.Symbol, smt.Symbol] = initSymbolTable.flatMap { case (id, expr) =>
+      scope.get(id) match {
+        case Some(Scope.StateVar(_, _)) | Some(Scope.OutputVar(_, _)) |
+             Some(Scope.SharedVar(_, _)) | Some(Scope.InputVar(_, _)) =>
+          Some(expr.asInstanceOf[smt.Symbol] -> stepSymTables(depth)(id).asInstanceOf[smt.Symbol])
+        case _ => None
+      }
+    }.toMap
+
+    solver.assert(negate(substitute(propExpr, propSubst)))
+
+    val result = solver.check()
+    solver.pop()
+
+    Utils.assert(result.isTrue, "IC3: BMC unrolling for CEX must be SAT")
+    (stepSymTables, result.model.get)
+  }
+
+  /** Result type for the IC3 algorithm. */
+  sealed trait IC3Result
+  case object IC3Proved extends IC3Result
+  case class IC3Cex(depth: Int) extends IC3Result
+  case object IC3Unknown extends IC3Result
+
+  class IC3ObligationLimitExceeded extends RuntimeException("IC3: exceeded obligation limit")
+
+  /** Maximum number of frames before IC3 gives up and reports UNKNOWN. */
+  val MAX_FRAMES = 100
+  val MAX_OBLIGATIONS = 1000
+
+  /** Main IC3 algorithm. Returns IC3Proved, IC3Cex(depth), or IC3Unknown. */
+  def checkProperty(propExpr: smt.Expr): IC3Result = {
+    log.debug("IC3: checking property")
+
+    // Step 1: Check init ∧ ¬P
+    solver.push()
+    solver.assert(initFormula)
+    solver.assert(negate(propExpr))
+    val initCheck = solver.check()
+    solver.pop()
+    if (initCheck.isTrue) {
+      log.debug("IC3: property violated in initial state")
+      return IC3Cex(0)
+    }
+
+    frames.clear()
+    frames += ArrayBuffer() // F[0]
+    frames += ArrayBuffer() // F[1]
+
+    var k = 1
+
+    try {
+      while (k < MAX_FRAMES) {
+        log.debug(s"IC3: working on frame $k")
+
+        if (!strengthen(k, propExpr)) {
+          log.debug("IC3: counterexample found")
+          return IC3Cex(k)
+        }
+
+        propagate(k) match {
+          case Some(fixpointFrame) =>
+            log.debug("IC3: fixpoint reached, property proved")
+            printInductiveInvariant(fixpointFrame)
+            return IC3Proved
+          case None => // continue
+        }
+
+        k += 1
+        frames += ArrayBuffer()
+      }
+
+      UclidMain.printResult("IC3: exceeded maximum frame depth (%d), result is UNKNOWN".format(MAX_FRAMES))
+      IC3Unknown
+    } catch {
+      case _: IC3ObligationLimitExceeded =>
+        UclidMain.printResult("IC3: exceeded obligation limit (%d), result is UNKNOWN".format(MAX_OBLIGATIONS))
+        IC3Unknown
+    }
+  }
+
+  /** Strengthen frame k by blocking all bad cubes. Returns false if CEX found.
+   *  Returns true if frame is strengthened. Throws if obligation limit exceeded. */
+  def strengthen(k: Int, propExpr: smt.Expr): Boolean = {
+    val obligations = ListBuffer[ProofObligation]()
+    var iterations = 0
+
+    while (true) {
+      iterations += 1
+      if (iterations > MAX_OBLIGATIONS) {
+        throw new IC3ObligationLimitExceeded()
+      }
+      if (obligations.isEmpty) {
+        // Check for bad cubes: F[k] ∧ ¬P SAT?
+        solver.push()
+        assertFrame(k)
+        solver.assert(negate(propExpr))
+        val badCheck = solver.check()
+        solver.pop()
+
+        if (badCheck.isTrue) {
+          // Use ¬P as the cube (not concrete model values).
+          // This is critical for infinite-state (integer) systems.
+          obligations += ProofObligation(k, negate(propExpr))
+        } else {
+          return true
+        }
+      }
+
+      // Process the lowest-frame obligation first.
+      val sortedIdx = obligations.zipWithIndex.minBy(_._1.frame)._2
+      val obligation = obligations.remove(sortedIdx)
+
+      if (obligation.frame == 0) {
+        // Check if cube is reachable from init.
+        solver.push()
+        solver.assert(initFormula)
+        solver.assert(obligation.cube)
+        val initCheck = solver.check()
+        solver.pop()
+
+        if (initCheck.isTrue) {
+          return false // Real counterexample
+        }
+        // Block at frame 1.
+        val blockingClause = generalize(0, obligation.cube)
+        if (frames.size > 1) {
+          frames(1) += blockingClause
+        }
+      } else {
+        // Consecution check: F[i-1] ∧ ¬cube ∧ T ∧ cube' SAT?
+        solver.push()
+        assertFrame(obligation.frame - 1)
+        solver.assert(negate(obligation.cube))
+        solver.assert(transFormula)
+        solver.assert(prime(obligation.cube))
+        val consecCheck = solver.check()
+        solver.pop()
+
+        if (consecCheck.isTrue) {
+          // Found predecessor — use concrete cube from model.
+          val predCube = extractConcreteCube(consecCheck.model.get)
+          obligations += ProofObligation(obligation.frame - 1, predCube)
+          obligations += obligation
+        } else {
+          // Cube blocked — generalize and add blocking clause.
+          val blockingClause = generalize(obligation.frame - 1, obligation.cube)
+          for (i <- 1 to obligation.frame) {
+            if (i < frames.size) {
+              frames(i) += blockingClause
+            }
+          }
+        }
+      }
+    }
+    true // unreachable
+  }
+
+  /** Propagate clauses forward and check for fixpoint.
+   *  Returns Some(i) if fixpoint found (frames(i) ⊆ frames(i+1)), None otherwise. */
+  def propagate(k: Int): Option[Int] = {
+    for (i <- 1 until k) {
+      val clausesToPush = ArrayBuffer[Clause]()
+      frames(i).foreach { clause =>
+        solver.push()
+        assertFrame(i)
+        solver.assert(clause)
+        solver.assert(transFormula)
+        solver.assert(prime(negate(clause)))
+        val pushCheck = solver.check(false)
+        solver.pop()
+
+        if (pushCheck.isFalse) {
+          clausesToPush += clause
+        }
+      }
+      clausesToPush.foreach { clause =>
+        if (!frames(i + 1).contains(clause)) {
+          frames(i + 1) += clause
+        }
+      }
+      if (frames(i).forall(c => frames(i + 1).contains(c))) {
+        return Some(i)
+      }
+    }
+    None
+  }
+
+  /** Rename internal symbol names to user-level variable names in an expression. */
+  def prettifyExpr(expr: smt.Expr): smt.Expr = {
+    smt.Context.rewriteExpr(expr, (e: smt.Expr) => e match {
+      case s: smt.Symbol =>
+        symbolToName.get(s.id) match {
+          case Some(name) => smt.Symbol(name, s.symbolTyp)
+          case None => s
+        }
+      case other => other
+    }, MutableMap.empty)
+  }
+
+  /** Pretty-print the inductive invariant from the fixpoint frame. */
+  def printInductiveInvariant(fixpointFrame: Int): Unit = {
+    val clauses = frames(fixpointFrame).distinct
+    UclidMain.printResult("IC3: Inductive invariant (frame %d):".format(fixpointFrame))
+    if (clauses.isEmpty) {
+      UclidMain.printResult("  true")
+    } else {
+      clauses.foreach { clause =>
+        UclidMain.printResult("  " + prettifyExpr(clause).toString)
+      }
+    }
+  }
+
+  /** Run IC3 on all properties matching the filter. */
+  def run(propertyFilter: (Identifier, List[ExprDecorator]) => Boolean, label: String = "ic3"): List[CheckResult] = {
+    // IC3 requires real solver responses (not SMT file dumps). Disable SMT file
+    // generation on the shared solver during IC3 execution.
+    val savedFilePrefix = solver.filePrefix
+    solver.filePrefix = ""
+
+    try {
+      val frameTbl = ArrayBuffer(initSymbolTable)
+
+      module.properties.flatMap { prop =>
+        if (propertyFilter(prop.id, prop.params) && !ExprDecorator.isLTLProperty(prop.params)) {
+          val propExpr = symSim.evaluate(prop.expr, initSymbolTable, frameTbl, 0, scope)
+          val ic3Result = checkProperty(propExpr)
+
+          val (solverResult, assertFrameTable, assertIter) = ic3Result match {
+            case IC3Proved =>
+              // Property proved.
+              (smt.SolverResult(Some(true), None), ArrayBuffer(frameTbl), 0)
+            case IC3Cex(depth) =>
+              // CEX found — build concrete trace via BMC unrolling.
+              val (stepSymTables, model) = buildCexTrace(depth, propExpr)
+              val cexFrameTbl: ArrayBuffer[SymbolicSimulator.SymbolTable] = stepSymTables
+              (smt.SolverResult(Some(false), Some(model)), ArrayBuffer(cexFrameTbl), depth)
+            case IC3Unknown =>
+              // Exceeded maximum frame depth — result is inconclusive.
+              (smt.SolverResult(None, None), ArrayBuffer(frameTbl), 0)
+          }
+
+          val assertInfo = AssertInfo(
+            prop.name, label,
+            assertFrameTable, scope, assertIter,
+            smt.BooleanLit(true), propExpr,
+            prop.params, prop.expr.position
+          )
+
+          Some(CheckResult(assertInfo, solverResult))
+        } else {
+          None
+        }
+      }
+    } finally {
+      solver.filePrefix = savedFilePrefix
+    }
+  }
+}
diff --git a/src/main/scala/uclid/SymbolicSimulator.scala b/src/main/scala/uclid/SymbolicSimulator.scala
index 08e394d6..d0df2455 100644
--- a/src/main/scala/uclid/SymbolicSimulator.scala
+++ b/src/main/scala/uclid/SymbolicSimulator.scala
@@ -358,9 +358,24 @@ class SymbolicSimulator (module : Module) {
             UclidMain.printStats(f"symbolic simulation for verify took $delta%.1f ms")
             check(solver, config, cmd);
             needToPrintResults=true
+          case "ic3" =>
+            val label : String = cmd.resultVar match {
+              case Some(l) => l.toString
+              case None    => "ic3"
+            }
+            val properties = extractProperties(Identifier("properties"), cmd.params)
+            val propertyFilter = createNoLTLFilter(properties)
+            solver match {
+              case z3Solver: smt.Z3Interface =>
+                val engine = new IC3Engine(module, z3Solver)
+                proofResults = engine.run(propertyFilter, label)
+              case _ =>
+                throw new Utils.RuntimeError("IC3 engine requires the Z3 solver backend.")
+            }
+            needToPrintResults = true
           case "check" => {
             // deprecated command: do nothing because we checked after every verification command
-          } 
+          }
           case "print" =>
             UclidMain.printStatus(cmd.args(0)._1.asInstanceOf[StringLit].value)
           case "print_results" =>
diff --git a/src/main/scala/uclid/lang/ControlCommandChecker.scala b/src/main/scala/uclid/lang/ControlCommandChecker.scala
index 0931531d..6562e35d 100644
--- a/src/main/scala/uclid/lang/ControlCommandChecker.scala
+++ b/src/main/scala/uclid/lang/ControlCommandChecker.scala
@@ -230,6 +230,11 @@ class ControlCommandCheckerPass extends ReadOnlyPass[Unit] {
         checkHasOneIdentifierArg(cmd, filename)
         checkHasMacroBody(cmd, filename)
         checkHasValidMacroIdentifier(cmd, filename, context)
+      case "ic3" =>
+        checkPropertiesValid(Identifier("properties"), cmd, context, filename)
+        checkParamsValid(cmd, filename, List(Identifier("properties")))
+        checkNoArgs(cmd, filename)
+        checkNoArgObj(cmd, filename)
       case "concrete" =>
         checkNoArgObj(cmd, filename)
       case "print_concrete_trace" =>
diff --git a/src/main/scala/uclid/smt/Context.scala b/src/main/scala/uclid/smt/Context.scala
index accda51c..1c7cb27c 100644
--- a/src/main/scala/uclid/smt/Context.scala
+++ b/src/main/scala/uclid/smt/Context.scala
@@ -244,6 +244,16 @@ abstract trait Context {
   def preassert(e: Expr)
   def check(produceModel: Boolean = true) : SolverResult
   def checkSynth() : SolverResult
+  /** SMT-LIB standard check-sat-assuming: check satisfiability under the given assumptions.
+   *  Used by IC3 for incremental solving and cube generalization. */
+  def checkAssumptions(assumptions: List[Expr]): SolverResult = {
+    throw new Utils.UnimplementedException("checkAssumptions not implemented.")
+  }
+  /** SMT-LIB standard get-unsat-core: retrieve the subset of assumptions responsible for UNSAT.
+   *  Used by IC3 for clause generalization via minimal unsat cores. */
+  def getUnsatCore(): List[Expr] = {
+    throw new Utils.UnimplementedException("getUnsatCore not implemented.")
+  }
   def finish()
 
   def addOption(option: String, value: Context.SolverOption)
diff --git a/src/main/scala/uclid/smt/Z3Interface.scala b/src/main/scala/uclid/smt/Z3Interface.scala
index 545daa45..15308544 100644
--- a/src/main/scala/uclid/smt/Z3Interface.scala
+++ b/src/main/scala/uclid/smt/Z3Interface.scala
@@ -197,6 +197,43 @@ class Z3Model(interface: Z3Interface, val model : z3.Model) extends Model {
         if (value.isIntNum()) {
           val bigInt = value.asInstanceOf[z3.IntNum].getBigInteger()
           smt.IntLit(bigInt)
+        } else if (value.isInstanceOf[z3.RatNum]) {
+          // Z3 returns RatNum for real-valued expressions.
+          val ratNum = value.asInstanceOf[z3.RatNum]
+          val num = BigInt(ratNum.getNumerator().getBigInteger())
+          val den = BigInt(ratNum.getDenominator().getBigInteger())
+          // Z3 normalizes rationals so denominator is always positive.
+          val negative = num < 0
+          val absNum = num.abs
+          val integral = absNum / den
+          val remainder = absNum % den
+          if (remainder == BigInt(0)) {
+            smt.RealLit(if (negative) -integral else integral, "0")
+          } else if (negative && integral == BigInt(0)) {
+            // Value is between -1 and 0 (e.g., -0.5). RealLit cannot represent
+            // negative zero in BigInt, so use (0.0 - positive_value).
+            val precision = 34
+            val scale = BigInt(10).pow(precision)
+            val fracDigits = (remainder * scale) / den
+            val fracStr = fracDigits.toString().reverse.padTo(precision, '0').reverse.replaceAll("0+$", "")
+            val frac = if (fracStr.isEmpty) "0" else fracStr
+            val posLit = smt.RealLit(BigInt(0), frac)
+            smt.OperatorApplication(smt.RealSubOp, List(smt.RealLit(BigInt(0), "0"), posLit))
+          } else {
+            // Compute fractional decimal digits via scaled long division.
+            val precision = 34
+            val scale = BigInt(10).pow(precision)
+            val fracDigits = (remainder * scale) / den
+            // Left-pad with zeros to get correct decimal place values.
+            val fracStr = fracDigits.toString().reverse.padTo(precision, '0').reverse.replaceAll("0+$", "")
+            val frac = if (fracStr.isEmpty) "0" else fracStr
+            smt.RealLit(if (negative) -integral else integral, frac)
+          }
+        } else if (value.isInstanceOf[z3.BitVecNum]) {
+          val bvNum = value.asInstanceOf[z3.BitVecNum]
+          val bigInt = bvNum.getBigInteger()
+          val width = e.typ.asInstanceOf[BitVectorType].width
+          smt.BitVectorLit(bigInt, width)
         } else if (value.isBool()) {
           val boolValue = value.asInstanceOf[z3.BoolExpr].getBoolValue()
           if (boolValue == Z3_lbool.Z3_L_TRUE) {
@@ -206,7 +243,19 @@ class Z3Model(interface: Z3Interface, val model : z3.Model) extends Model {
           } else {
             throw new Utils.RuntimeError("Unable to get model value for: " + e.toString)
           }
+        } else if (e.typ.isInstanceOf[EnumType]) {
+          // Z3 enum constants are named after the enum member strings.
+          val enumTyp = e.typ.asInstanceOf[EnumType]
+          val valueStr = value.toString()
+          if (enumTyp.members.contains(valueStr)) {
+            smt.EnumLit(valueStr, enumTyp)
+          } else {
+            throw new Utils.RuntimeError(
+              "Unknown enum value '" + valueStr + "' for type " + enumTyp.toString + " in: " + e.toString)
+          }
         } else {
+          // Unsupported types (arrays, records, tuples, maps, uninterpreted, etc.)
+          // throw RuntimeError so callers like IC3Engine.extractConcreteCube can skip gracefully.
           throw new Utils.RuntimeError("Unable to get model value for: " + e.toString)
         }
     }
@@ -664,6 +713,32 @@ class Z3Interface() extends Context {
     throw new Utils.UnimplementedException("Can't use an SMT solver for synthesis!")
   }
 
+  /** Store mapping from Z3 BoolExpr to smt.Expr for unsat core retrieval. */
+  var assumptionMap: scala.collection.immutable.Map[z3.BoolExpr, Expr] = scala.collection.immutable.Map.empty
+
+  /** SMT-LIB standard check-sat-assuming via Z3's solver.check(assumptions...).
+   *  Used by IC3 for incremental consecution and generalization queries. */
+  override def checkAssumptions(assumptions: List[Expr]): SolverResult = {
+    val z3Assumptions = assumptions.map(e => exprToZ3(e).asInstanceOf[z3.BoolExpr])
+    assumptionMap = z3Assumptions.zip(assumptions).toMap
+    val z3Result = solver.check(z3Assumptions: _*)
+    z3Result match {
+      case z3.Status.SATISFIABLE =>
+        val z3Model = solver.getModel()
+        SolverResult(Some(true), Some(new Z3Model(this, z3Model)))
+      case z3.Status.UNSATISFIABLE =>
+        SolverResult(Some(false), None)
+      case _ =>
+        SolverResult(None, None)
+    }
+  }
+
+  /** SMT-LIB standard get-unsat-core: maps Z3 core back to smt.Expr via assumptionMap. */
+  override def getUnsatCore(): List[Expr] = {
+    val core = solver.getUnsatCore()
+    core.toList.map(e => assumptionMap(e))
+  }
+
   override def finish() {
     ctx.close()
   }
diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala
index 94a28147..5cd4572a 100644
--- a/src/test/scala/VerifierSpec.scala
+++ b/src/test/scala/VerifierSpec.scala
@@ -706,6 +706,39 @@ class HyperPropertySpec extends AnyFlatSpec {
     VerifierSpec.expectedFails("./test/test-hyperproperty-7.ucl", 0)
   }
 }
+class IC3VerifSpec extends AnyFlatSpec {
+  "test-ic3-0.ucl" should "verify all assertions." in {
+    VerifierSpec.expectedFails("./test/test-ic3-0.ucl", 0)
+  }
+  "test-ic3-1.ucl" should "fail to verify 1 assertion." in {
+    VerifierSpec.expectedFails("./test/test-ic3-1.ucl", 1)
+  }
+  "test-ic3-2.ucl" should "verify all assertions." in {
+    VerifierSpec.expectedFails("./test/test-ic3-2.ucl", 0)
+  }
+  "test-ic3-bv-fail.ucl" should "fail to verify 1 assertion." in {
+    VerifierSpec.expectedFails("./test/test-ic3-bv-fail.ucl", 1)
+  }
+  "test-ic3-real-fail.ucl" should "report unknown for real-valued property." in {
+    UclidMain.enableStringOutput()
+    UclidMain.clearStringOutput()
+    val modules = UclidMain.compile(ConfigCons.createConfig("./test/test-ic3-real-fail.ucl"), lang.Identifier("main"), true)
+    val mainModule = UclidMain.instantiate(UclidMain.Config(), modules, lang.Identifier("main"))
+    assert(mainModule.isDefined)
+    val results = UclidMain.execute(mainModule.get, UclidMain.Config())
+    // IC3 cannot prove or disprove this — should report unknown, not falsely PASSED.
+    assert(results.count((e) => e.result.isTrue) == 0)
+  }
+  "test-ic3-int-nonterm.ucl" should "report unknown without looping forever." in {
+    UclidMain.enableStringOutput()
+    UclidMain.clearStringOutput()
+    val modules = UclidMain.compile(ConfigCons.createConfig("./test/test-ic3-int-nonterm.ucl"), lang.Identifier("main"), true)
+    val mainModule = UclidMain.instantiate(UclidMain.Config(), modules, lang.Identifier("main"))
+    assert(mainModule.isDefined)
+    val results = UclidMain.execute(mainModule.get, UclidMain.Config())
+    assert(results.count((e) => e.result.isUndefined) >= 1)
+  }
+}
 
 object PrintCexSpec {
   def checkPrintCex(filename: String, n : Int) {
diff --git a/test/test-ic3-0.ucl b/test/test-ic3-0.ucl
new file mode 100644
index 00000000..6b8444ec
--- /dev/null
+++ b/test/test-ic3-0.ucl
@@ -0,0 +1,20 @@
+/* Test IC3: property should hold (simple counter, x >= 0). */
+module main {
+  var x : integer;
+
+  init {
+    x = 0;
+  }
+
+  next {
+    x' = x + 1;
+  }
+
+  invariant x_non_neg : x >= 0;
+
+  control {
+    ic3;
+    check;
+    print_results;
+  }
+}
diff --git a/test/test-ic3-1.ucl b/test/test-ic3-1.ucl
new file mode 100644
index 00000000..d9ad44b6
--- /dev/null
+++ b/test/test-ic3-1.ucl
@@ -0,0 +1,21 @@
+/* Test IC3: property should fail (x < 5 eventually violated). */
+module main {
+  var x : integer;
+
+  init {
+    x = 0;
+  }
+
+  next {
+    x' = x + 1;
+  }
+
+  invariant x_lt_5 : x < 5;
+
+  control {
+    v = ic3;
+    check;
+    print_results;
+    v.print_cex;
+  }
+}
diff --git a/test/test-ic3-2.ucl b/test/test-ic3-2.ucl
new file mode 100644
index 00000000..ffeb0279
--- /dev/null
+++ b/test/test-ic3-2.ucl
@@ -0,0 +1,23 @@
+/* Test IC3: property requires strengthening (y <= x, not 1-inductive). */
+module main {
+  var x : integer;
+  var y : integer;
+
+  init {
+    x = 1;
+    y = 1;
+  }
+
+  next {
+    y' = y + 1;
+    x' = x + y';
+  }
+
+  invariant y_le_x : y <= x;
+
+  control {
+    ic3;
+    check;
+    print_results;
+  }
+}
diff --git a/test/test-ic3-bv-fail.ucl b/test/test-ic3-bv-fail.ucl
new file mode 100644
index 00000000..72aae4b6
--- /dev/null
+++ b/test/test-ic3-bv-fail.ucl
@@ -0,0 +1,25 @@
+/* Test IC3: property should fail (bitvector overflow).
+ * x starts at 1bv3, increments by 1bv3 each step.
+ * After 7 steps, x wraps from 7bv3 to 0bv3 due to 3-bit overflow.
+ * The invariant x >_u 0bv3 should be violated.
+ */
+module main {
+  var x : bv3;
+
+  init {
+    x = 1bv3;
+  }
+
+  next {
+    x' = x + 1bv3;
+  }
+
+  invariant x_pos : x >_u 0bv3;
+
+  control {
+    v = ic3;
+    check;
+    print_results;
+    v.print_cex;
+  }
+}
diff --git a/test/test-ic3-int-nonterm.ucl b/test/test-ic3-int-nonterm.ucl
new file mode 100644
index 00000000..334e721f
--- /dev/null
+++ b/test/test-ic3-int-nonterm.ucl
@@ -0,0 +1,27 @@
+/* Test IC3: integer property that previously caused non-termination.
+ * x starts at 0, y at 5; x' = x + y, y' = y - 10.
+ * IC3 should report unknown (max depth exceeded) rather than loop forever.
+ */
+module main {
+  var x : integer;
+  var y : integer;
+
+  init {
+    x = 0;
+    y = 5;
+  }
+
+  next {
+    x' = x + y;
+    y' = y - 10;
+  }
+
+  invariant x_pos : x >= 0;
+
+  control {
+    v = ic3;
+    check;
+    print_results;
+    v.print_cex;
+  }
+}
diff --git a/test/test-ic3-real-fail.ucl b/test/test-ic3-real-fail.ucl
new file mode 100644
index 00000000..b7d63081
--- /dev/null
+++ b/test/test-ic3-real-fail.ucl
@@ -0,0 +1,27 @@
+/* Test IC3: real-valued property that should fail.
+ * x starts at 0.0, y at 5.0; x' = x + y, y' = y - 2.0.
+ * x goes: 0, 5, 8, 9, 8, 5, 0, -7 => fails at step 7.
+ */
+module main {
+  var x : real;
+  var y : real;
+
+  init {
+    x = 0.0;
+    y = 5.0;
+  }
+
+  next {
+    x' = x + y;
+    y' = y - 2.0;
+  }
+
+  invariant x_pos : x >= 0.0;
+
+  control {
+    v = ic3;
+    check;
+    print_results;
+    v.print_cex;
+  }
+}