From 3b9d73999dec903e518ec7757218af505ee54dd7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 4 Jun 2024 14:54:01 +0200
Subject: [PATCH] test: limit bit width of mul eval problems and add new
 successes

---
 Eval/bitvec_152.lean      | 2 +-
 Eval/bitvec_229.lean      | 2 +-
 Eval/bitvec_239.lean      | 2 +-
 Eval/bitvec_290__292.lean | 2 +-
 Eval/fail.txt             | 4 ----
 Eval/success.txt          | 4 ++++
 6 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Eval/bitvec_152.lean b/Eval/bitvec_152.lean
index f00278ef..6a1a647b 100644
--- 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
index c7edeefc..3ff497b1 100644
--- 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
index d054a38e..a17ef3f7 100644
--- 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
index 2bce4a9f..f43201ae 100644
--- 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
index 27a278a0..fd4ba185 100644
--- 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
index b73eea0a..895e568b 100644
--- 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