Add IC3/PDR engine for unbounded safety verification

[lsk567]

Summary

• Adds an IC3/PDR (Property Directed Reachability) engine that proves unbounded safety properties without requiring a bound, complementing the existing BMC and k-induction engines
• Supports ic3 as a new control command (usage: v = ic3; check; print_results; v.print_cex;)
• Handles infinite-state (integer arithmetic) systems via symbolic cubes and integer inequality generalization
• Generates concrete counterexample traces compatible with print_cex and print_cex_json
• Outputs the inductive invariant (final frame) when a property is proved safe

Changes

• IC3Engine.scala (new): Core IC3/PDR algorithm — frame management, proof obligations, consecution checks, cube generalization (unsat cores + sign-based inequality abstraction for integers and reals), clause propagation, fixpoint detection, and BMC-style CEX trace reconstruction. Includes obligation limit and max frame depth to prevent non-termination.
• Context.scala: Add checkAssumptions() / getUnsatCore() — standard SMT-LIB operations for incremental solving
• Z3Interface.scala: Implement assumption-based checking and unsat core extraction via Z3 Java API; model evaluation for integers, bitvectors, reals (including negative fractional values), booleans, and enums
• ControlCommandChecker.scala: Add ic3 command validation
• SymbolicSimulator.scala: Add ic3 command dispatch with label support for print_cex
• build.sbt: Configure fork and java.library.path for Z3 JNI native library loading (commented)

Test plan

• test-ic3-0.ucl: x >= 0 proved (1-inductive, fixpoint at frame 2)
• test-ic3-1.ucl: x < 5 fails with CEX trace (x: 0→1→2→3→4→5)
• test-ic3-2.ucl: y <= x proved with strengthening (not 1-inductive, fixpoint at frame 4)
• test-ic3-bv-fail.ucl: BV overflow — x wraps 1bv3→...→7bv3→0bv3, correctly reports FAILED at step 7
• test-ic3-real-fail.ucl: Real arithmetic (x,y parabolic trajectory) — correctly reports UNKNOWN (sound: does not falsely claim PASSED)
• test-ic3-int-nonterm.ucl: Previously non-terminating integer case — correctly reports UNKNOWN within seconds
• All tests added to CI regression suite (IC3VerifSpec in VerifierSpec.scala)
• Full test suite: no regressions

[KE7]

LGTM

[polgreen]

Minor point:

• the tests aren't included in the regression tests run by the CI
• it would be helpful if it could output the final frame so you could sanity check that frame is actually inductive and sufficient to prove the property

Major point:

• this doesn't work. I haven't looked into why, but this property passes using IC3, and fails using BMC:

/* Test IC3: property should fail due to overflow */
module main {
  var x : bv3;

  init {
    x = 1bv3;
  }

  next {
    x' = x + 1bv3;
  }

  invariant x_non_neg : x > 0bv3;

  control {
    v1 = bmc(3); // fails
    check;
    v1.print_cex(x);
    v2 = ic3; // passes, and should not
    check;
    v2.print_cex(x);
  }
}

[polgreen]

why do we need this now?

[polgreen]

why do we need this now?

[polgreen]

These tests need to be added to the regression tests that are run by CI

[polgreen]

I don't know if this should be inside the Z3 interface or within IC3, it seems specific to IC3

[polgreen]

Also, really hard to debug this because I can't make sense of the SMT files it prints, because it prints one to check the initial state, and then it prints two that just contain the property and nothing else

[polgreen]

This doesn't work:

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; // passes with IC3
    //v = bmc(10); // fails with bmc
    check;
    print_results;
    v.print_cex;
  }
}

[polgreen]

See the example I've given above; this needs to handle and test all the datatypes we support, not just integers and bitvecs

[polgreen]

You need to consider all the datatypes we support, not just bitvectors and integers

[polgreen]

This never terminates:

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;
  }
}

Also, not sure how this will work for infinite datatypes that aren't integers, as you can only generalize integer types (and then you can only generalize x=constant to x>0 or x<0)

[polgreen]

Have you looked at the invariants it is printing for the final frames?

For test-ic3-2.ucl, it prints this:

IC3: Inductive invariant (frame 1):
  (not (not (<= y x)))
  (not (< x 0))
  (not (= x 0))
  (not (and (< y 0) (< x 0)))
  (not (> x 0))
  (not (and (= x 0) (< y 0)))

This simplifies to false, so it can't be inductive, and it can't imply the property y<=x?

An actual inductive invariant for this would be y<=x && x>0

Looking at another example with mixed types:

/* Test IC3: property should fail due to overflow */
module main {
  var x : real;
  var y: real;
  var z: integer;

  init {
    x = 1.0;
    assume(y > 0.0);
    z = 1;
  }

  next {
    x' = x + y;
    z' = z+1;
  }

  invariant x_non_neg : x > 0.0 && z > 0;

  control {
    v2 = ic3; // produces a final invariant which is not inductive
    check;
    v2.print_cex(x);
  }
}

This prints the invariant:

IC3: Inductive invariant (frame 1):
  (not (not (and (> x 0.0) (> z 0))))
  (not (> z 0))

Again, this simplifies to false? It also doesn't include the strengthening it should need, which is that y>0

[polgreen]

Soundness bug:
This property should fail. It passes, with the following final frame:

  (not (not (> z 0)))
  (not (> y 0))
  (not (= y 0))
  (not (< y 0))

If you remove the assignment to y=1, it fails as it should.

/* Test IC3: property should fail */
module main {
  var y: integer;
  var z: integer;

  init {
    y = 1; // remove this unrelated line to make the property fail
    z = 2;
  }

  next {
    z' = z-1;
  }

  invariant z_non_neg: z > 0;

  control {
    v2 = ic3; // produces a final invariant which is not inductive
    check;
    v2.print_cex(z);
  }
}