From edb6ba10070de34cd596af581d0e479db90b957f Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Wed, 22 May 2024 02:59:54 -0400 Subject: [PATCH] Use correct sort for x in #testPowerAddiSymbolic 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'. --- src/ArchC-Core-Tests/AcInstrDecodeTest.class.st | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ArchC-Core-Tests/AcInstrDecodeTest.class.st b/src/ArchC-Core-Tests/AcInstrDecodeTest.class.st index 68af299..8e49112 100644 --- a/src/ArchC-Core-Tests/AcInstrDecodeTest.class.st +++ b/src/ArchC-Core-Tests/AcInstrDecodeTest.class.st @@ -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 . ]