some flags for model_checker (e.g. `show_unproved`) not parsed and fed into solc correctly

[xenide]

Component

Forge

Have you ensured that all of these are up to date?

• Foundry
• Foundryup

What version of Foundry are you on?

forge Version: 1.5.0-stable Commit SHA: 1c57854 Build Timestamp: 2025-11-26T09:16:58.269730000Z (1764148618) Build Profile: maxperf

What version of Foundryup are you on?

foundryup: 1.5.0

What command(s) is the bug in?

forge build

Operating System

macOS (Apple Silicon)

Describe the bug

Under the [model_checker] config, even when we set show_unproved = true and show_unsupported = true, I think that these config are not parsed correctly as I observed that

1. when running forge config, those flags don't show up
2. getting outputs like the following even when those flags are set

Warning (5840): CHC: 3 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
Warning (5724): SMTChecker: 229 unsupported language feature(s). Enable the model checker option "show unsupported" to see all of them.

Sample repo

• https://github.com/xenide/erc721-harberger/tree/feat/smt-solver

[grandizzy]

@xenide thank you, will fix, the issue is that you need to add the configs in camel case for now, e.g.

[profile.default.model_checker]
contracts = { 'a.sol' = [ 'A1', 'A2' ], 'b.sol' = [ 'B1', 'B2' ] }
engine = 'chc'
targets = [ 'assert', 'outOfBounds' ]
timeout = 100001
showUnproved = true
showUnsupported = true
showProvedSafe = true

[grandizzy]

on a 2nd thought this will be a breaking change (unless we won't support both snake case / camel case), maybe we should just fix docs on it @zerosnacks @DaniPopes wdyt?

[zerosnacks]

stylistically & for simplicity I prefer we always use snake_case for foundry.toml keys and handle the casting to camelcase for solc correctly