Plugin configuration

Project-wide defaults live in the bmc { } block in your build.gradle.kts. Almost every one can be overridden for a single run with a -Dbmc.* system property, and a value on a @BmcProof always wins over the project default.

bmc {
    // unwind defaults to AUTO: each proof discovers its own loop bound
    timeoutSeconds = 60
    stringMode = "refinement"
}

Common options

bmc { }	-Dbmc.*	Default	What it does
unwind	unwind	AUTO	Default loop bound. AUTO discovers it; a positive value pins one bound for every proof.
unwindCap	(unwindCap)	16	Highest bound AUTO climbs to before giving up with Unknown.
parallelism	parallelism	CPU count	How many proofs run at once, each its own process.
timeoutSeconds	timeoutSeconds	none	Default wall-clock budget per proof.
solver	solver	MiniSat	Default SAT/SMT backend. See External solver.
stringMode	stringMode	refinement	Default String model. See String modes.
maxStringLength	maxStringLength	16	Bound on symbolic string length.
removeExceptionMessages	removeExceptionMessages	auto	Whether to drop unread exception messages.
cache	noCache	on	Skip re-verifying a proof whose inputs haven’t changed.
progress		on	Print per-proof progress during gradlew test.

Trust and scope

These control what counts as a gap versus an accepted shortcut:

bmc { }	-Dbmc.*	What it does
allowStubs	allowStubs	Methods every proof may run as havoc’d stubs without a warning.
acknowledgeUnmodelled	acknowledgeUnmodelled	JDK members bmc4j can’t model that proofs may reach as havoc instead of Unknown.
strictStubs	strictStubs	Turn an unacknowledged stub into Unknown instead of a footnote.
strictModels	strictModels	Turn an unregistered user model into Unknown.
notModeledPackages	notModeledPackages	Whole packages declared out of scope for modeling.
jbmcPath	jbmc	Use a local engine binary instead of the bundled one.

The plugin id is org.bmc4j. Apply it and proofs are just JUnit 5 tests under gradlew test.