`hevm symbolic` reports an incorrect counterexample/false negative

[baolean]

hevm symbolic does not correctly identify a failing assert assert(debt == Art * rate) in the counterexample() function of the following MiniVat contract (the runtime bytecode is available here).

pragma solidity ^0.8.17;

contract MiniVat {
    uint256 public debt;
    mapping(address => uint256) public art;
    mapping(address => uint256) public dai;
    uint256 public Art;
    uint256 public rate;

    function init() public {
        require(rate == 0, "rate not zero");
        rate = 10 ** 27;
    }

    function move(address dst, int256 wad) public {
        address src = msg.sender;
        dai[src] = wad > 0
            ? dai[src] - uint256(wad)
            : dai[src] + uint256(-1 * wad);
        dai[dst] = wad > 0
            ? dai[dst] + uint256(wad)
            : dai[dst] - uint256(-1 * wad);
    }

    function frob(int256 dart) public {
        address usr = msg.sender;

        int256 _art = int256(art[usr]) + dart;
        require(_art >= 0, "negative art");
        art[usr] = uint256(_art);

        require(rate <= uint256(type(int256).max), "rate exceeds max int256");
        int256 ddai = dart * int256(rate);

        int256 _dai = int256(dai[usr]) + ddai;
        require(_dai >= 0, "negative dai");
        dai[usr] = uint256(_dai);

        Art = dart > 0 ? Art + uint256(dart) : Art - uint256(-1 * dart);
        debt = ddai > 0 ? debt + uint256(ddai) : debt - uint256(-1 * ddai);
    }

    function fold(int256 delta) public {
        address usr = msg.sender;
        rate = delta > 0 ? rate + uint256(delta) : rate - uint256(-1 * delta);
        require(Art <= uint256(type(int256).max), "Art exceeds max int256");
        int256 ddai = int256(Art) * delta;
        dai[usr] = ddai > 0
            ? dai[usr] + uint256(ddai)
            : dai[usr] - uint256(-1 * ddai);
        debt = ddai > 0 ? debt + uint256(ddai) : debt - uint256(-1 * ddai);
    }

    function counterexample() external {
        init();
        frob(10 ** 18);
        fold(-10 ** 27);
        init();
        assert(debt == Art * rate);
    }
}

counterexample() encodes the sequence of function calls with concrete parameters that lead to the assert violation, so hevm should be able to report it even without using symbolic storage (--storage-model InitialS); however, it doesn't find a violation:

hevm symbolic --code $(<MiniVat/minivat.bin-runtime) --storage-model InitialS
Exploring contract
Simplifying expression
Explored contract (164 branches)
Checking for reachability of 8 potential property violation(s)

QED: No reachable property violations discovered

The violation can only be identified if symbolic storage is enabled (the analysis takes ~8 minutes), even though it shouldn't be necessary. In addition, the generated concrete storage values also seem a bit off (at the end of the function execution, debt == 0, Art == 10 ** 18, and rate == 10 ** 27; at the beginning of the execution, all these values are supposed to be zero):

hevm symbolic --code $(<MiniVat/minivat.bin-runtime)
Exploring contract
Simplifying expression
Explored contract (174 branches)
Checking for reachability of 8 potential property violation(s)

Discovered the following counterexamples:

Calldata:
  0xf473c3a6

Storage:
  Addr 0xacab: [(0x0,0xffffffffffffffffffffffffffdb00dc7387bbc139a0571a5c25744927240000),
(0x3,0x187396c075c59861067a10040007100004cc0d2498),(0x4,0x0),
(0x20000000000000000000000000000000004,0x47004c8ba6762e2f2feb74f1f96be8874c0968ce9e011718e593610201000000),
(0x800000000000000000000000000000000000000000000000000000000000003,0x18003190008400000022404020a400802440000000180584c599c0000)]

Transaction Context:
  CallValue: 0x0
  Caller: 0x0

Steps to reproduce:

1. Download the runtime bytecode of MiniVat
2. Run hevm symbolic --code $(<MiniVat/minivat.bin-runtime) --storage-model InitialS
3. Run hevm symbolic --code $(<MiniVat/minivat.bin-runtime)

[d-xo]

thanks for the report! reproduced locally, will fix asap.