WARNING:halmos:path.append(false) in Damn Vulnerable Defi - NaiveReceiver.t.sol

[0xkarmacoma]

Describe the bug

As reported by https://t.me/c/1815219512/2277 and easily reproducible. We get the following warnings during the execution of setUp():

WARNING:halmos:path.append(false)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
WARNING:halmos:path.append(false)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)

With some extra debug info:

Running 1 tests for test/naive-receiver/NaiveReceiver.t.sol:NaiveReceiverChallenge
Constructor trace:
    CREATE NaiveReceiverChallenge::<0 bytes of initcode>
    ↩ RETURN <20027 bytes of code>

  File "halmos/.venv/bin/halmos", line 8, in <module>
    sys.exit(main())
  File "halmos/src/halmos/__main__.py", line 1677, in main
    return _main().exitcode
  File "halmos/src/halmos/__main__.py", line 1641, in _main
    test_results = run_method(run_args)
  File "halmos/src/halmos/__main__.py", line 1019, in run_sequential
    setup_ex = setup(
  File "halmos/src/halmos/__main__.py", line 520, in setup
    for idx, setup_ex in enumerate(setup_exs_all):
  File "halmos/src/halmos/sevm.py", line 2415, in run
    self.create(ex, opcode, stack, step_id)
  File "halmos/src/halmos/sevm.py", line 1913, in create
    self.transfer_value(ex, caller, new_addr, value)
  File "halmos/src/halmos/sevm.py", line 1528, in transfer_value
    balance_cond = simplify(UGE(ex.balance_of(caller), value))
  File "halmos/src/halmos/sevm.py", line 817, in balance_of
    self.path.append(ULT(value, con(2**96)))
  File "halmos/src/halmos/sevm.py", line 598, in append
    import traceback; traceback.print_stack()
WARNING:halmos:path.append(false) orig_cond=ULT(340282366920938463463374607431768211456, 79228162514264337593543950336)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
  File "halmos/.venv/bin/halmos", line 8, in <module>
    sys.exit(main())
  File "halmos/src/halmos/__main__.py", line 1677, in main
    return _main().exitcode
  File "halmos/src/halmos/__main__.py", line 1641, in _main
    test_results = run_method(run_args)
  File "halmos/src/halmos/__main__.py", line 1019, in run_sequential
    setup_ex = setup(
  File "halmos/src/halmos/__main__.py", line 520, in setup
    for idx, setup_ex in enumerate(setup_exs_all):
  File "halmos/src/halmos/sevm.py", line 2415, in run
    self.create(ex, opcode, stack, step_id)
  File "halmos/src/halmos/sevm.py", line 1913, in create
    self.transfer_value(ex, caller, new_addr, value)
  File "halmos/src/halmos/sevm.py", line 1537, in transfer_value
    ex.balance_update(caller, self.arith(ex, EVM.SUB, ex.balance_of(caller), value))
  File "halmos/src/halmos/sevm.py", line 817, in balance_of
    self.path.append(ULT(value, con(2**96)))
  File "halmos/src/halmos/sevm.py", line 598, in append
    import traceback; traceback.print_stack()
WARNING:halmos:path.append(false) orig_cond=ULT(340282366920938463463374607431768211456, 79228162514264337593543950336)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
[console.log] msg.sender 0x00000000000000000000000000000000000000000000000000000000de4107e4
[console.log] trustedForwarder 0x00000000000000000000000000000000000000000000000000000000aaaa0003
Error: setUp() failed: HalmosException: No successful path found in setUp()
Traceback (most recent call last):
  File "halmos/src/halmos/__main__.py", line 1019, in run_sequential
    setup_ex = setup(
               ^^^^^^
  File "halmos/src/halmos/__main__.py", line 560, in setup
    raise HalmosException(f"No successful path found in {setup_sig}")
halmos.exceptions.HalmosException: No successful path found in setUp()
Symbolic test result: 0 passed; 1 failed; time: 0.49s

To Reproduce

Check out https://github.com/igorganich/damn-vulnerable-defi-halmos/blob/master/test/naive-receiver/NaiveReceiver.t.sol

Run halmos --function test_naiveReceiver

Environment:

• OS: mac
• Python version: Python 3.12.1
• Halmos and other dependency versions: f7ff1f8323207334c35da1542005ae4b77d23ae3