halmos -v
Running 1 tests for test/Arithmetic.t.sol:TestArithmetic
[FAIL] test_add_uint256(uint256,uint256) (paths: 2/5, time: 0.40s, bounds: [])
Counterexample: [msg_sender = 0, msg_value = 0, p_a_uint256 = 0, p_b_uint256 = 0, this_address = 0]
# 3 / 5
PC: this_address 352 STOP - 0 <generated>
Stack: [3074223460]
Memory:
- 0x0: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x20: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x40: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 76]
- 0x60: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x80: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 68]
- 0xa0: [192, 246, 56, 242, Extract(255, 248, p_a_uint256), Extract(247, 240, p_a_uint256), Extract(239, 232, p_a_uint256), Extract(231, 224, p_a_uint256), Extract(223, 216, p_a_uint256), Extract(215, 208, p_a_uint256), Extract(207, 200, p_a_uint256), Extract(199, 192, p_a_uint256), Extract(191, 184, p_a_uint256), Extract(183, 176, p_a_uint256), Extract(175, 168, p_a_uint256), Extract(167, 160, p_a_uint256), Extract(159, 152, p_a_uint256), Extract(151, 144, p_a_uint256), Extract(143, 136, p_a_uint256), Extract(135, 128, p_a_uint256), Extract(127, 120, p_a_uint256), Extract(119, 112, p_a_uint256), Extract(111, 104, p_a_uint256), Extract(103, 96, p_a_uint256), Extract(95, 88, p_a_uint256), Extract(87, 80, p_a_uint256), Extract(79, 72, p_a_uint256), Extract(71, 64, p_a_uint256), Extract(63, 56, p_a_uint256), Extract(55, 48, p_a_uint256), Extract(47, 40, p_a_uint256), Extract(39, 32, p_a_uint256)]
- 0xc0: [Extract(31, 24, p_a_uint256), Extract(23, 16, p_a_uint256), Extract(15, 8, p_a_uint256), Extract(7, 0, p_a_uint256), Extract(255, 248, p_b_uint256), Extract(247, 240, p_b_uint256), Extract(239, 232, p_b_uint256), Extract(231, 224, p_b_uint256), Extract(223, 216, p_b_uint256), Extract(215, 208, p_b_uint256), Extract(207, 200, p_b_uint256), Extract(199, 192, p_b_uint256), Extract(191, 184, p_b_uint256), Extract(183, 176, p_b_uint256), Extract(175, 168, p_b_uint256), Extract(167, 160, p_b_uint256), Extract(159, 152, p_b_uint256), Extract(151, 144, p_b_uint256), Extract(143, 136, p_b_uint256), Extract(135, 128, p_b_uint256), Extract(127, 120, p_b_uint256), Extract(119, 112, p_b_uint256), Extract(111, 104, p_b_uint256), Extract(103, 96, p_b_uint256), Extract(95, 88, p_b_uint256), Extract(87, 80, p_b_uint256), Extract(79, 72, p_b_uint256), Extract(71, 64, p_b_uint256), Extract(63, 56, p_b_uint256), Extract(55, 48, p_b_uint256), Extract(47, 40, p_b_uint256), Extract(39, 32, p_b_uint256)]
- 0xe0: [Extract(31, 24, p_b_uint256), Extract(23, 16, p_b_uint256), Extract(15, 8, p_b_uint256), Extract(7, 0, p_b_uint256), 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x100: [0, 0, 0, 68, 192, 246, 56, 242, Extract(255, 248, p_a_uint256), Extract(247, 240, p_a_uint256), Extract(239, 232, p_a_uint256), Extract(231, 224, p_a_uint256), Extract(223, 216, p_a_uint256), Extract(215, 208, p_a_uint256), Extract(207, 200, p_a_uint256), Extract(199, 192, p_a_uint256), Extract(191, 184, p_a_uint256), Extract(183, 176, p_a_uint256), Extract(175, 168, p_a_uint256), Extract(167, 160, p_a_uint256), Extract(159, 152, p_a_uint256), Extract(151, 144, p_a_uint256), Extract(143, 136, p_a_uint256), Extract(135, 128, p_a_uint256), Extract(127, 120, p_a_uint256), Extract(119, 112, p_a_uint256), Extract(111, 104, p_a_uint256), Extract(103, 96, p_a_uint256), Extract(95, 88, p_a_uint256), Extract(87, 80, p_a_uint256), Extract(79, 72, p_a_uint256), Extract(71, 64, p_a_uint256)]
- 0x120: [Extract(63, 56, p_a_uint256), Extract(55, 48, p_a_uint256), Extract(47, 40, p_a_uint256), Extract(39, 32, p_a_uint256), Extract(31, 24, p_a_uint256), Extract(23, 16, p_a_uint256), Extract(15, 8, p_a_uint256), Extract(7, 0, p_a_uint256), Extract(255, 248, p_b_uint256), Extract(247, 240, p_b_uint256), Extract(239, 232, p_b_uint256), Extract(231, 224, p_b_uint256), Extract(223, 216, p_b_uint256), Extract(215, 208, p_b_uint256), Extract(207, 200, p_b_uint256), Extract(199, 192, p_b_uint256), Extract(191, 184, p_b_uint256), Extract(183, 176, p_b_uint256), Extract(175, 168, p_b_uint256), Extract(167, 160, p_b_uint256), Extract(159, 152, p_b_uint256), Extract(151, 144, p_b_uint256), Extract(143, 136, p_b_uint256), Extract(135, 128, p_b_uint256), Extract(127, 120, p_b_uint256), Extract(119, 112, p_b_uint256), Extract(111, 104, p_b_uint256), Extract(103, 96, p_b_uint256), Extract(95, 88, p_b_uint256), Extract(87, 80, p_b_uint256), Extract(79, 72, p_b_uint256), Extract(71, 64, p_b_uint256)]
- 0x140: [Extract(63, 56, p_b_uint256), Extract(55, 48, p_b_uint256), Extract(47, 40, p_b_uint256), Extract(39, 32, p_b_uint256), Extract(31, 24, p_b_uint256), Extract(23, 16, p_b_uint256), Extract(15, 8, p_b_uint256), Extract(7, 0, p_b_uint256), 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x160: [0, 0, 0, 0, 0, 0, 0, 96, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 113, 9, 112, 158, 207, 169, 26, 128, 98, 111, 243, 152]
- 0x180: [157, 104, 246, 127, 91, 29, 209, 45, 102, 97, 105, 108, 101, 100, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x1a0: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x1c0: [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x1e0: [0, 0, 0, 0, 0, 0, 0, 100, 112, 202, 16, 187, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 113, 9, 112, 158, 207, 169, 26, 128]
- 0x200: [98, 111, 243, 152, 157, 104, 246, 127, 91, 29, 209, 45, 102, 97, 105, 108, 101, 100, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x220: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x240: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 112, 202, 16, 187, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 113, 9, 112, 158]
- 0x260: [207, 169, 26, 128, 98, 111, 243, 152, 157, 104, 246, 127, 91, 29, 209, 45, 102, 97, 105, 108, 101, 100, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x280: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x2a0: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
- 0x2c0: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
Storage:
- this_address: {0: {0: Concat(Extract(255, 16, storage_slot_0_0), 1, Extract(7, 0, storage_slot_0_0))}}
Balance:
- this_address: this_balance + msg_value - 0 - 0 - 0
Path:
- msg_value == 0
- Not(call1 == 0)
- call2 == 0
- Not(call1 == 0)
- Not(call1 == 0)
- Not(call1 == 0)
- Not(call1 == 0)
- Not(call1 == 0)
- Not(call1 == 0)
- call2 == 0
- Not(extcodesize(645326474426547203313410069153905908525362434349) == 0)
Output: None
Log: [([29485693714967335757563038618841744472215891622979272243827124658718922284880], 429049853758163107186368799942587076079339706258956588087153966199096448962356661055866306375861046696051322400401741685125038281870778983368639235038904320), ([95180208686301398394554031582401412094073538926388354310127026171774931619608], 11505236063118821809467553221049758295155052665230762065499525194094891251552260362809157039377781374726210488638842056300353482370348462500409570082870200511689663829945559818529136259043050327177290308227941601695126878464399625111430179431737320830335505806068516514195737649102622530195829220243517141417984), ([95180208686301398394554031582401412094073538926388354310127026171774931619608], 11505236063118821809467553221049758295155052665230762065499525194094891251552260362809157039377781374726210488638842056300353482370348462500409570082870200511699916357724358568980581405894333766482111596248363362125840459118798500724025206904028642650840132123536673437250057636019259959519479623151633274241024)]
Storage updates:
SHA3 hashes:
External calls:
- (call1, call_544(1, gas(1), Concat(0, Extract(159, 0, this_address)), 0, Concat(3237361906, p_a_uint256, p_b_uint256)), None)
- (call2, call_544(2, gas(2), Concat(0, Extract(159, 0, this_address)), 0, Concat(3237361906, p_a_uint256, p_b_uint256)), None)
- (call3, call_800(3,
gas(3),
645326474426547203313410069153905908525362434349,
0,
2937815620610723459522636952510386841785114031644826774648436411116173207964843441748423061353483029633030135072093998600777156395894761540308991058809448955476838734537982926037376347404276804152882314295846787711769047727657335210003922945), None)