From 20ff265ff7e165474fb0199b7f1ba055cdb82355 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 9 Jul 2024 15:54:09 +0200 Subject: [PATCH] test: adapt test for arbitrary shiftRight --- Test/Bv/Shift.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Test/Bv/Shift.lean b/Test/Bv/Shift.lean index a31316d3..4def0f1b 100644 --- a/Test/Bv/Shift.lean +++ b/Test/Bv/Shift.lean @@ -26,9 +26,8 @@ set_option trace.bv true in theorem shift_unit_5 {x y z : BitVec 16} : (x <<< y) <<< z = (x <<< z) <<< y := by bv_decide --- This demonstrates we correctly abstract shifts of arbitrary width as atoms instead of giving up. set_option trace.bv true in -theorem shift_unit_6 {x y : BitVec 64} : (x >>> y) + y = y + (x >>> y) := by +theorem shift_unit_6 {x y z : BitVec 16} : (x >>> y) >>> z = (x >>> z) >>> y := by bv_decide set_option trace.bv true in