test: limit bit width of mul eval problems and add new successes

leanprover · Jun 17, 2024 · 3b9d739 · 3b9d739
1 parent eb54447
commit 3b9d739
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 8 deletions.
diff --git a/Eval/bitvec_152.lean b/Eval/bitvec_152.lean
@@ -1,5 +1,5 @@
 import LeanSAT.Reflect.Tactics.BVDecide
 
 theorem bitvec_152 :
- ∀ (x : BitVec 64), x * -1 = 0 - x
+ ∀ (x : BitVec 8), x * -1 = 0 - x
 := by intros; bv_decide
diff --git a/Eval/bitvec_229.lean b/Eval/bitvec_229.lean
@@ -1,5 +1,5 @@
 import LeanSAT.Reflect.Tactics.BVDecide
 
 theorem bitvec_229 :
- ∀ (X C1 Op1 : BitVec 64), (X + C1) * Op1 = X * Op1 + C1 * Op1
+ ∀ (X C1 Op1 : BitVec 4), (X + C1) * Op1 = X * Op1 + C1 * Op1
 := by intros; bv_decide
diff --git a/Eval/bitvec_239.lean b/Eval/bitvec_239.lean
@@ -1,5 +1,5 @@
 import LeanSAT.Reflect.Tactics.BVDecide
 
 theorem bitvec_239 :
- ∀ (Y X : BitVec 64), (0 - X) * (0 - Y) = X * Y
+ ∀ (Y X : BitVec 8), (0 - X) * (0 - Y) = X * Y
 := by intros; bv_decide
diff --git a/Eval/bitvec_290__292.lean b/Eval/bitvec_290__292.lean
@@ -2,5 +2,5 @@ import LeanSAT.Reflect.Tactics.BVDecide
 open BitVec
 
 theorem bitvec_290__292 :
- ∀ (Y Op1 : BitVec 64), 1#64 <<< Y * Op1 = Op1 <<< Y
+ ∀ (Y Op1 : BitVec 8), 1#8 <<< Y * Op1 = Op1 <<< Y
 := by intros; bv_decide
diff --git a/Eval/fail.txt b/Eval/fail.txt
@@ -1,9 +1,5 @@
 WillOverflow.lean
-bitvec_152.lean
 bitvec_160.lean
-bitvec_229.lean
-bitvec_239.lean
-bitvec_283.lean
 bitvec_290__292.lean
 bitvec_AndOrXor_2443.lean
 bitvec_InstCombineShift__239.lean

diff --git a/Eval/success.txt b/Eval/success.txt
@@ -1,4 +1,8 @@
 Popcount.lean
+bitvec_152.lean
+bitvec_229.lean
+bitvec_239.lean
+bitvec_283.lean
 bitvec_AddSub_1043.lean
 bitvec_AddSub_1152.lean
 bitvec_AddSub_1156.lean