Kontrol returns incorrect counterexample for failing test

[lucasmt]

Kontrol returns incorrect counterexamples in certain tests, particularly if they depend on keccak computations. For example, the following test fails because if key1 == key2 + 1, then the value of _map[key1] gets overwritten to 43, so the assertion doesn't hold:

pragma solidity ^0.8.13;

import {Test} from "forge-std/Test.sol";

contract CounterexampleTest is Test {
    mapping(uint256 => uint256) _map;

    function testOverwrite(uint256 key1, uint256 key2) public {
        vm.assume(key2 < type(uint256).max);

        _map[key1] = 42;
        _map[key2 + 1] = 43;

        vm.assertEq(_map[key1], 42);
    }
}

Kontrol correctly reports a failure, but the counterexample it provides is the following, which is incorrect:

  Model:
    key2 = 0
    key1 = 0
    block.number = 16777217
    block.timestamp = 1073741825

If key1 == key2 as in the counterexample above, the value of _map[key1] is not overwritten and the test does not fail. I suspect that this incorrect counterexample might be because the SMT solver is not able to evaluate the path condition that leads to the failure, which looks like this:

( notBool 42 ==Int #lookup ( ( keccak ( #buf ( 32 , KV0_key1:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) |-> 42 ) [ keccak ( #buf ( 32 , ( KV1_key2:Int +Int 1 ) ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) <- 43 ] , keccak ( #buf ( 32 , KV0_key1:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " ) ) )

The obvious case that would satisfy this condition is if key1 == key2 + 1, but it's possible that the expression is being encoded in a way that the solver is unable to reason about. Someone who knows more about the counterexample generation than me can probably give a better assessment.