Is this really using PleaseRunAll? Isn't there just one possible value?
I just want to make sure we are testing what we want to test.

Yes, there are at least two known address here: the deployed C and T contracts. The origin addresses are also valid ones.

Fair point.

With current main, running: cabal run exe:hevm -- test --root tmp --match "only_deployed_force_addr" --only-deployed gives us:

[RUNNING] prove_only_deployed_force_addr(address)
   [FAIL] prove_only_deployed_force_addr
   Counterexample:   [not reproducible]
     calldata: prove_only_deployed_force_addr(0x0470C202ca30050800087234Ffee81fb7FCEaFc4)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

This current branch gives:

[RUNNING] prove_only_deployed_force_addr(address)
   [FAIL] prove_only_deployed_force_addr
   Counterexample:   [validated]
     calldata: prove_only_deployed_force_addr(0xD95322745865822719164b1fC167930754c248DE)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001

The difference between the two is only this PR. The reason for this is that this runAll:

onlyDeployed addrExpr fallback continue = do
    vm <- get
    if not (?conf.onlyDeployed) then fallback addrExpr
    else case eqT @t @Symbolic of
      Just Refl -> do
        let deployedAddrs = map forceEAddrToEWord $ mapMaybe (codeMustExist vm) $ Map.keys vm.env.contracts
        runAll (?conf.maxDepth) vm.exploreDepth $ PleaseRunAll addrExpr deployedAddrs runAllPaths
      _ -> internalError "Unknown address in Concrete mode"

Will run for all --only-deployed as long as there are too many solutions. So it will run for this case, too, since the address can be anything here:

  function prove_only_deployed_force_addr(address x) pure public {
    uint256 y = C(x).f();
    assert(y != 42);
  }

There is no restriction on x. So the SMT solver gets 100 different soltuions and then it gives up, and falls back to onlyDeployed:

forceAddr addrExpr fallback continue = case wordToAddr addrExpr of
  Nothing -> manySolutions (?conf).maxDepth addrExpr 20 $ \case
    Just sol -> continue $ LitAddr (truncateToAddr sol)
    Nothing -> onlyDeployed addrExpr fallback continue
  Just c -> continue c

I hope this is a good explanation :) Took me a while to think through this but I hope it's a good description of what's going on!