From 6a7d28c33963cdc2bfb5995724512834057e21c3 Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Fri, 13 Feb 2026 13:26:07 -0800
Subject: [PATCH 01/10] Add IC3/PDR engine for unbounded safety property
 verification

IC3/PDR (Property Directed Reachability) proves safety properties without
requiring a bound, complementing the existing BMC and k-induction engines.
It incrementally constructs frame-based over-approximations of reachable
states, blocks counterexample cubes via generalization (unsat cores +
integer inequality abstraction), and detects fixpoints through clause
propagation. Supports counterexample trace generation for print_cex.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 build.sbt                                     |   6 +
 src/main/scala/uclid/IC3Engine.scala          | 444 ++++++++++++++++++
 src/main/scala/uclid/SymbolicSimulator.scala  |  17 +-
 .../uclid/lang/ControlCommandChecker.scala    |   5 +
 src/main/scala/uclid/smt/Context.scala        |   6 +
 src/main/scala/uclid/smt/Z3Interface.scala    |  23 +
 test/test-ic3-0.ucl                           |  20 +
 test/test-ic3-1.ucl                           |  21 +
 test/test-ic3-2.ucl                           |  23 +
 9 files changed, 564 insertions(+), 1 deletion(-)
 create mode 100644 src/main/scala/uclid/IC3Engine.scala
 create mode 100644 test/test-ic3-0.ucl
 create mode 100644 test/test-ic3-1.ucl
 create mode 100644 test/test-ic3-2.ucl

diff --git a/build.sbt b/build.sbt
index ada7fdad8..824e98f5f 100644
--- a/build.sbt
+++ b/build.sbt
@@ -15,6 +15,12 @@ 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 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 000000000..83bdd1915
--- /dev/null
+++ b/src/main/scala/uclid/IC3Engine.scala
@@ -0,0 +1,444 @@
+/*
+ * 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
+
+  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))
+    }
+  }
+
+  /**
+   * Try to generalize a primed integer equality (v' == c) to a sign-based inequality.
+   * 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 {
+      case smt.OperatorApplication(smt.EqualityOp, List(sym: smt.Symbol, smt.IntLit(value))) =>
+        val zero = smt.IntLit(BigInt(0))
+        val candidate = if (value < 0) {
+          smt.OperatorApplication(smt.IntLTOp, List(sym, zero))
+        } else if (value > 0) {
+          smt.OperatorApplication(smt.IntGTOp, List(sym, zero))
+        } else {
+          return primedLit // value == 0, keep as is
+        }
+        // Check if replacing this literal still gives UNSAT
+        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()
+        if (result.isFalse) candidate else primedLit
+      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)
+  }
+
+  /** Main IC3 algorithm. Returns None if proved, Some(depth) if CEX found at given depth. */
+  def checkProperty(propExpr: smt.Expr): Option[Int] = {
+    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 Some(0)
+    }
+
+    frames.clear()
+    frames += ArrayBuffer() // F[0]
+    frames += ArrayBuffer() // F[1]
+
+    var k = 1
+    val MAX_FRAMES = 500
+
+    while (k < MAX_FRAMES) {
+      log.debug(s"IC3: working on frame $k")
+
+      if (!strengthen(k, propExpr)) {
+        log.debug("IC3: counterexample found")
+        return Some(k)
+      }
+
+      if (propagate(k)) {
+        log.debug("IC3: fixpoint reached, property proved")
+        return None
+      }
+
+      k += 1
+      frames += ArrayBuffer()
+    }
+
+    throw new Utils.RuntimeError("IC3: exceeded maximum number of frames")
+  }
+
+  /** Strengthen frame k by blocking all bad cubes. Returns false if CEX found. */
+  def strengthen(k: Int, propExpr: smt.Expr): Boolean = {
+    val obligations = ListBuffer[ProofObligation]()
+
+    while (true) {
+      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. */
+  def propagate(k: Int): Boolean = {
+    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 true
+      }
+    }
+    false
+  }
+
+  /** Run IC3 on all properties matching the filter. */
+  def run(propertyFilter: (Identifier, List[ExprDecorator]) => Boolean, label: String = "ic3"): List[CheckResult] = {
+    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 cexDepth = checkProperty(propExpr)
+
+        val (solverResult, assertFrameTable, assertIter) = cexDepth match {
+          case None =>
+            // Property proved.
+            (smt.SolverResult(Some(true), None), ArrayBuffer(frameTbl), 0)
+          case Some(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)
+        }
+
+        val assertInfo = AssertInfo(
+          prop.name, label,
+          assertFrameTable, scope, assertIter,
+          smt.BooleanLit(true), propExpr,
+          prop.params, prop.expr.position
+        )
+
+        Some(CheckResult(assertInfo, solverResult))
+      } else {
+        None
+      }
+    }
+  }
+}
diff --git a/src/main/scala/uclid/SymbolicSimulator.scala b/src/main/scala/uclid/SymbolicSimulator.scala
index 08e394d62..d0df2455b 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 0931531df..6562e35da 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 accda51c6..2573605f5 100644
--- a/src/main/scala/uclid/smt/Context.scala
+++ b/src/main/scala/uclid/smt/Context.scala
@@ -244,6 +244,12 @@ abstract trait Context {
   def preassert(e: Expr)
   def check(produceModel: Boolean = true) : SolverResult
   def checkSynth() : SolverResult
+  def checkAssumptions(assumptions: List[Expr]): SolverResult = {
+    throw new Utils.UnimplementedException("checkAssumptions not implemented.")
+  }
+  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 545daa452..b26ba8938 100644
--- a/src/main/scala/uclid/smt/Z3Interface.scala
+++ b/src/main/scala/uclid/smt/Z3Interface.scala
@@ -664,6 +664,29 @@ 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
+
+  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)
+    }
+  }
+
+  override def getUnsatCore(): List[Expr] = {
+    val core = solver.getUnsatCore()
+    core.toList.map(e => assumptionMap(e))
+  }
+
   override def finish() {
     ctx.close()
   }
diff --git a/test/test-ic3-0.ucl b/test/test-ic3-0.ucl
new file mode 100644
index 000000000..6b8444ece
--- /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 000000000..d9ad44b64
--- /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 000000000..ffeb0279c
--- /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;
+  }
+}

From b1d7b57aca0bd8843ee2f1c82e67897dbb81f15c Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Fri, 13 Feb 2026 13:38:38 -0800
Subject: [PATCH 02/10] Update macOS CI runner from macos-13 to macos-14

macos-13 is no longer supported by GitHub Actions.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .github/workflows/test.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 2caa0262a..61241a3a8 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -105,7 +105,7 @@ jobs:
       run: sbt universal:packageBin
 
   test-macos:
-    runs-on: macos-13
+    runs-on: macos-14
 
     steps:
     - uses: actions/checkout@v2

From 57c3130053b2f73d159228bd2e859268a94eec67 Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Fri, 13 Feb 2026 13:51:30 -0800
Subject: [PATCH 03/10] Fix macOS CI: replace deprecated setup-scala with
 proper JDK/SBT setup

The macOS CI was failing because olafurpg/setup-scala (deprecated) relied
on the sbt launcher to bootstrap from Maven Central without caching,
causing transient download failures. Align macOS job with Ubuntu by using
actions/setup-java + coursier/setup-action + SBT caching.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .github/workflows/test.yml | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 61241a3a8..64b81eedb 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -109,9 +109,28 @@ jobs:
 
     steps:
     - uses: actions/checkout@v2
-    - uses: olafurpg/setup-scala@v10
+
+    - name: Set up JDK 11
+      uses: actions/setup-java@v1
       with:
-        java-version: openjdk@1.11
+        java-version: 11
+
+    - name: Cache SBT ivy cache
+      uses: actions/cache@v4
+      with:
+        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

From a09a1ce1567e586e7317f6c0f0b353b81c781bbc Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Fri, 13 Feb 2026 14:01:56 -0800
Subject: [PATCH 04/10] Fix macOS CI: use setup-java@v4 with Zulu for ARM64
 compatibility

actions/setup-java@v1 defaults to x64 architecture, installing an x86_64
JVM on the macos-14 ARM64 runner. This causes UnsatisfiedLinkError when
loading the ARM64 Z3 native libraries. Use setup-java@v4 with Zulu
distribution which provides native ARM64 JDK 11 for macOS.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .github/workflows/test.yml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 64b81eedb..73e47d544 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -111,9 +111,10 @@ jobs:
     - uses: actions/checkout@v2
 
     - name: Set up JDK 11
-      uses: actions/setup-java@v1
+      uses: actions/setup-java@v4
       with:
-        java-version: 11
+        distribution: 'zulu'
+        java-version: '11'
 
     - name: Cache SBT ivy cache
       uses: actions/cache@v4

From 0716ebc03971d37d2aa43e92e975a37c7d6d79e3 Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Mon, 23 Feb 2026 10:57:16 -0800
Subject: [PATCH 05/10] Add IC3 tests to CI regression suite

Register test-ic3-0, test-ic3-1, and test-ic3-2 in VerifierSpec.scala
under a new IC3VerifSpec class, following the existing test pattern.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/test/scala/VerifierSpec.scala | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala
index 94a281475..0cb68c999 100644
--- a/src/test/scala/VerifierSpec.scala
+++ b/src/test/scala/VerifierSpec.scala
@@ -706,6 +706,17 @@ 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)
+  }
+}
 
 object PrintCexSpec {
   def checkPrintCex(filename: String, n : Int) {

From 20c3cd5423d41ad0f2062a0286c0f7605b3042b3 Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Mon, 23 Feb 2026 10:58:53 -0800
Subject: [PATCH 06/10] Clean up IC3/PDR PR review items

- build.sbt: Add comments explaining fork/javaOptions are needed for Z3
  JNI native library loading via sbt (complements LD_LIBRARY_PATH from
  setup scripts)
- Context.scala, Z3Interface.scala: Document checkAssumptions and
  getUnsatCore as standard SMT-LIB operations (check-sat-assuming,
  get-unsat-core)
- IC3Engine.scala: Disable SMT file generation during IC3 execution to
  prevent empty/broken output files from the shared solver's filePrefix
  mechanism

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 build.sbt                                  |  4 +
 src/main/scala/uclid/IC3Engine.scala       | 92 ++++++++++++++--------
 src/main/scala/uclid/smt/Context.scala     |  4 +
 src/main/scala/uclid/smt/Z3Interface.scala |  3 +
 4 files changed, 70 insertions(+), 33 deletions(-)

diff --git a/build.sbt b/build.sbt
index 824e98f5f..dd4aa7ea7 100644
--- a/build.sbt
+++ b/build.sbt
@@ -15,6 +15,10 @@ 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"
 
diff --git a/src/main/scala/uclid/IC3Engine.scala b/src/main/scala/uclid/IC3Engine.scala
index 83bdd1915..35b1a3048 100644
--- a/src/main/scala/uclid/IC3Engine.scala
+++ b/src/main/scala/uclid/IC3Engine.scala
@@ -296,9 +296,12 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
         return Some(k)
       }
 
-      if (propagate(k)) {
-        log.debug("IC3: fixpoint reached, property proved")
-        return None
+      propagate(k) match {
+        case Some(fixpointFrame) =>
+          log.debug("IC3: fixpoint reached, property proved")
+          printInductiveInvariant(fixpointFrame)
+          return None
+        case None => // continue
       }
 
       k += 1
@@ -379,8 +382,9 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
     true // unreachable
   }
 
-  /** Propagate clauses forward and check for fixpoint. */
-  def propagate(k: Int): Boolean = {
+  /** 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 =>
@@ -402,43 +406,65 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
         }
       }
       if (frames(i).forall(c => frames(i + 1).contains(c))) {
-        return true
+        return Some(i)
+      }
+    }
+    None
+  }
+
+  /** 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("  " + clause.toString)
       }
     }
-    false
   }
 
   /** Run IC3 on all properties matching the filter. */
   def run(propertyFilter: (Identifier, List[ExprDecorator]) => Boolean, label: String = "ic3"): List[CheckResult] = {
-    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 cexDepth = checkProperty(propExpr)
-
-        val (solverResult, assertFrameTable, assertIter) = cexDepth match {
-          case None =>
-            // Property proved.
-            (smt.SolverResult(Some(true), None), ArrayBuffer(frameTbl), 0)
-          case Some(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)
-        }
+    // 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 cexDepth = checkProperty(propExpr)
+
+          val (solverResult, assertFrameTable, assertIter) = cexDepth match {
+            case None =>
+              // Property proved.
+              (smt.SolverResult(Some(true), None), ArrayBuffer(frameTbl), 0)
+            case Some(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)
+          }
 
-        val assertInfo = AssertInfo(
-          prop.name, label,
-          assertFrameTable, scope, assertIter,
-          smt.BooleanLit(true), propExpr,
-          prop.params, prop.expr.position
-        )
+          val assertInfo = AssertInfo(
+            prop.name, label,
+            assertFrameTable, scope, assertIter,
+            smt.BooleanLit(true), propExpr,
+            prop.params, prop.expr.position
+          )
 
-        Some(CheckResult(assertInfo, solverResult))
-      } else {
-        None
+          Some(CheckResult(assertInfo, solverResult))
+        } else {
+          None
+        }
       }
+    } finally {
+      solver.filePrefix = savedFilePrefix
     }
   }
 }
diff --git a/src/main/scala/uclid/smt/Context.scala b/src/main/scala/uclid/smt/Context.scala
index 2573605f5..1c7cb27cb 100644
--- a/src/main/scala/uclid/smt/Context.scala
+++ b/src/main/scala/uclid/smt/Context.scala
@@ -244,9 +244,13 @@ 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.")
   }
diff --git a/src/main/scala/uclid/smt/Z3Interface.scala b/src/main/scala/uclid/smt/Z3Interface.scala
index b26ba8938..cc0f9f56b 100644
--- a/src/main/scala/uclid/smt/Z3Interface.scala
+++ b/src/main/scala/uclid/smt/Z3Interface.scala
@@ -667,6 +667,8 @@ class Z3Interface() extends Context {
   /** 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
@@ -682,6 +684,7 @@ class Z3Interface() extends Context {
     }
   }
 
+  /** 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))

From f45b5db36767b72c8edd900509231359c612e3f6 Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Mon, 23 Feb 2026 11:00:01 -0800
Subject: [PATCH 07/10] Print inductive invariant when IC3 proves a property
 safe

After IC3 reaches a fixpoint, output the final frame clauses as the
inductive invariant. Clauses are deduplicated and printed with
user-level variable names instead of internal symbol encodings.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/main/scala/uclid/IC3Engine.scala | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/uclid/IC3Engine.scala b/src/main/scala/uclid/IC3Engine.scala
index 35b1a3048..8430a41bb 100644
--- a/src/main/scala/uclid/IC3Engine.scala
+++ b/src/main/scala/uclid/IC3Engine.scala
@@ -55,6 +55,16 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
     }
   }.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()
 
@@ -412,6 +422,18 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
     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
@@ -420,7 +442,7 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
       UclidMain.printResult("  true")
     } else {
       clauses.foreach { clause =>
-        UclidMain.printResult("  " + clause.toString)
+        UclidMain.printResult("  " + prettifyExpr(clause).toString)
       }
     }
   }

From d8cf08e2878f0cffeaf71d23a7de43231e28e59b Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Mon, 23 Feb 2026 11:06:15 -0800
Subject: [PATCH 08/10] Fix IC3 soundness bug: handle bitvector values in Z3
 model evaluation

Z3Model.evaluate() only handled IntNum and Bool values from Z3 models,
throwing RuntimeError for bitvector (BitVecNum) values. In IC3's
extractConcreteCube(), this error was silently caught, causing all
bitvector state variables to be dropped and producing a trivial `true`
cube. This led to a `false` blocking clause that poisoned frames,
creating a spurious fixpoint and incorrectly reporting properties as
PASSED.

Add BitVecNum handling to evaluate() that returns proper BitVectorLit
with the correct width. Add regression test with 3-bit bitvector
overflow (x increments from 1bv3 and wraps to 0bv3 after 7 steps).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/main/scala/uclid/smt/Z3Interface.scala |  5 +++++
 test/test-ic3-bv-fail.ucl                  | 25 ++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 test/test-ic3-bv-fail.ucl

diff --git a/src/main/scala/uclid/smt/Z3Interface.scala b/src/main/scala/uclid/smt/Z3Interface.scala
index cc0f9f56b..73ab11803 100644
--- a/src/main/scala/uclid/smt/Z3Interface.scala
+++ b/src/main/scala/uclid/smt/Z3Interface.scala
@@ -197,6 +197,11 @@ 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.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) {
diff --git a/test/test-ic3-bv-fail.ucl b/test/test-ic3-bv-fail.ucl
new file mode 100644
index 000000000..72aae4b64
--- /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;
+  }
+}

From e3b4ff2b1f87f2e5e229653426ebf5e6b793c414 Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Mon, 23 Feb 2026 11:07:41 -0800
Subject: [PATCH 09/10] Add bitvector overflow test to IC3 CI regression suite

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/test/scala/VerifierSpec.scala | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala
index 0cb68c999..040f18987 100644
--- a/src/test/scala/VerifierSpec.scala
+++ b/src/test/scala/VerifierSpec.scala
@@ -716,6 +716,9 @@ class IC3VerifSpec extends AnyFlatSpec {
   "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)
+  }
 }
 
 object PrintCexSpec {

From 830c7488066f902af1d59a3d518d19fd04e96e99 Mon Sep 17 00:00:00 2001
From: Shaokai Lin <shaokai@berkeley.edu>
Date: Mon, 2 Mar 2026 15:01:20 -0800
Subject: [PATCH 10/10] Address round-2 review: handle all datatypes, fix
 non-termination

- Z3Interface: add RealNum (RatNum) and EnumType handling in model
  evaluate(); fix negative fractional-only reals (e.g., -0.5) via
  (0.0 - value) workaround for RealLit sign limitation
- IC3Engine: add real number generalization (sign-based, matching
  integer approach); add obligation limit (MAX_OBLIGATIONS=1000) to
  prevent infinite looping in strengthen(); add IC3Unknown result type
  with MAX_FRAMES=100 depth limit; remove BV generalization (concrete
  equalities + unsat cores work better for finite domains)
- Tests: add test-ic3-real-fail.ucl (real arithmetic, reports UNKNOWN
  soundly), test-ic3-int-nonterm.ucl (previously non-terminating,
  now reports UNKNOWN); add CI entries in VerifierSpec.scala

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/main/scala/uclid/IC3Engine.scala       | 131 ++++++++++++++-------
 src/main/scala/uclid/smt/Z3Interface.scala |  44 +++++++
 src/test/scala/VerifierSpec.scala          |  19 +++
 test/test-ic3-int-nonterm.ucl              |  27 +++++
 test/test-ic3-real-fail.ucl                |  27 +++++
 5 files changed, 208 insertions(+), 40 deletions(-)
 create mode 100644 test/test-ic3-int-nonterm.ucl
 create mode 100644 test/test-ic3-real-fail.ucl

diff --git a/src/main/scala/uclid/IC3Engine.scala b/src/main/scala/uclid/IC3Engine.scala
index 8430a41bb..219c346c2 100644
--- a/src/main/scala/uclid/IC3Engine.scala
+++ b/src/main/scala/uclid/IC3Engine.scala
@@ -114,7 +114,27 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
   }
 
   /**
-   * Try to generalize a primed integer equality (v' == c) to a sign-based inequality.
+   * 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.
    */
@@ -125,28 +145,32 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
     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 if (value > 0) {
-          smt.OperatorApplication(smt.IntGTOp, List(sym, zero))
         } else {
-          return primedLit // value == 0, keep as is
+          smt.OperatorApplication(smt.IntGTOp, List(sym, zero))
         }
-        // Check if replacing this literal still gives UNSAT
-        val newAssumptions = candidate :: otherAssumptions
-        solver.push()
-        if (frame == 0) {
-          solver.assert(initFormula)
+        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 {
-          assertFrame(frame)
+          // integral > 0, or integral == 0 with non-zero fractional part (positive)
+          smt.OperatorApplication(smt.RealGTOp, List(sym, zero))
         }
-        solver.assert(negate(unprime(candidate)))
-        solver.assert(transFormula)
-        val result = solver.checkAssumptions(newAssumptions)
-        solver.pop()
-        if (result.isFalse) candidate else primedLit
+        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
     }
   }
@@ -276,8 +300,20 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
     (stepSymTables, result.model.get)
   }
 
-  /** Main IC3 algorithm. Returns None if proved, Some(depth) if CEX found at given depth. */
-  def checkProperty(propExpr: smt.Expr): Option[Int] = {
+  /** 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
@@ -288,7 +324,7 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
     solver.pop()
     if (initCheck.isTrue) {
       log.debug("IC3: property violated in initial state")
-      return Some(0)
+      return IC3Cex(0)
     }
 
     frames.clear()
@@ -296,36 +332,48 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
     frames += ArrayBuffer() // F[1]
 
     var k = 1
-    val MAX_FRAMES = 500
 
-    while (k < MAX_FRAMES) {
-      log.debug(s"IC3: working on frame $k")
+    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)
+        }
 
-      if (!strengthen(k, propExpr)) {
-        log.debug("IC3: counterexample found")
-        return Some(k)
-      }
+        propagate(k) match {
+          case Some(fixpointFrame) =>
+            log.debug("IC3: fixpoint reached, property proved")
+            printInductiveInvariant(fixpointFrame)
+            return IC3Proved
+          case None => // continue
+        }
 
-      propagate(k) match {
-        case Some(fixpointFrame) =>
-          log.debug("IC3: fixpoint reached, property proved")
-          printInductiveInvariant(fixpointFrame)
-          return None
-        case None => // continue
+        k += 1
+        frames += ArrayBuffer()
       }
 
-      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
     }
-
-    throw new Utils.RuntimeError("IC3: exceeded maximum number of frames")
   }
 
-  /** Strengthen frame k by blocking all bad cubes. Returns false if CEX found. */
+  /** 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()
@@ -460,17 +508,20 @@ class IC3Engine(module: Module, solver: smt.Z3Interface) {
       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 cexDepth = checkProperty(propExpr)
+          val ic3Result = checkProperty(propExpr)
 
-          val (solverResult, assertFrameTable, assertIter) = cexDepth match {
-            case None =>
+          val (solverResult, assertFrameTable, assertIter) = ic3Result match {
+            case IC3Proved =>
               // Property proved.
               (smt.SolverResult(Some(true), None), ArrayBuffer(frameTbl), 0)
-            case Some(depth) =>
+            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(
diff --git a/src/main/scala/uclid/smt/Z3Interface.scala b/src/main/scala/uclid/smt/Z3Interface.scala
index 73ab11803..153085440 100644
--- a/src/main/scala/uclid/smt/Z3Interface.scala
+++ b/src/main/scala/uclid/smt/Z3Interface.scala
@@ -197,6 +197,38 @@ 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()
@@ -211,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)
         }
     }
diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala
index 040f18987..5cd4572ae 100644
--- a/src/test/scala/VerifierSpec.scala
+++ b/src/test/scala/VerifierSpec.scala
@@ -719,6 +719,25 @@ class IC3VerifSpec extends AnyFlatSpec {
   "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 {
diff --git a/test/test-ic3-int-nonterm.ucl b/test/test-ic3-int-nonterm.ucl
new file mode 100644
index 000000000..334e721f4
--- /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 000000000..b7d630818
--- /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;
+  }
+}