Skip to content

Commit

Permalink
Use correct sort for x in #testPowerAddiSymbolic
Browse files Browse the repository at this point in the history
In this line:

``` self assert: (instr fieldValue: 'd') equals: 'x'

the `instr fieldValue: 'd'` is a Z3Int, so the #= down in assert:equals: coerces the 'x' to a Z3Int.  So now we have two `x` symbols: a BV16 `x` and an Int `x`, which are not necessarily equal.  The correct thing to do is to start from the same BV `x`, and compare the Int interpretation of `d` to the signed Int interpretation of `x`.
  • Loading branch information
shingarov committed May 22, 2024
1 parent 82015e2 commit 5f885cd
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/ArchC-Core-Tests/AcInstrDecodeTest.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ AcInstrDecodeTest >> testPowerAddiSymbolic [
self assert: instr name equals: 'addi'.
self assert: (instr fieldValue: 'rt') equals: 0.
self assert: (instr fieldValue: 'ra') equals: 0.
self assert: (instr fieldValue: 'd') equals: 'x'.
self assert: (instr fieldValue: 'd') equals: ('x'///16) toSignedInt .

]

Expand Down

0 comments on commit 5f885cd

Please sign in to comment.