diff --git a/Eval/fail.txt b/Eval/fail.txt
index d1712ed1..3007a693 100644
--- a/Eval/fail.txt
+++ b/Eval/fail.txt
@@ -1,9 +1,6 @@
-bitvec_160.lean
-bitvec_290__292.lean
 bitvec_AndOrXor_2443.lean
 bitvec_InstCombineShift__239.lean
 bitvec_InstCombineShift__279.lean
-bitvec_InstCombineShift__351.lean
 bitvec_InstCombineShift__422_1.lean
 bitvec_InstCombineShift__422_2.lean
 bitvec_InstCombineShift__440.lean
@@ -11,7 +8,6 @@ bitvec_InstCombineShift__458.lean
 bitvec_InstCombineShift__476.lean
 bitvec_InstCombineShift__497.lean
 bitvec_InstCombineShift__582.lean
-bitvec_InstCombineShift__724.lean
 g2008h02h16hSDivOverflow2_proof.lean
 g2008h02h23hMulSub_proof.lean
 gadd2_proof.lean
diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Mul.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Mul.lean
index 84c33782..d4a6ed7a 100644
--- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Mul.lean
+++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Mul.lean
@@ -63,7 +63,7 @@ theorem go_eq_eval_getLsb {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr
           rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := blastShiftLeftConst)]
           rw [hacc]
         . intros
-          simp only [blastShiftLeft_eq_eval_getLsb, BitVec.getLsb_shiftLeft]
+          simp only [blastShiftLeftConst_eq_eval_getLsb, BitVec.getLsb_shiftLeft]
           split
           . next hdiscr => simp [hdiscr]
           . next hidx hdiscr =>
diff --git a/Test/Eval.lean b/Test/Eval.lean
index d292b238..65c351ad 100644
--- a/Test/Eval.lean
+++ b/Test/Eval.lean
@@ -72,7 +72,6 @@ import Test.Eval.bitvec_AndOrXor_716
 import Test.Eval.bitvec_AndOrXor_794
 import Test.Eval.bitvec_AndOrXor_827
 import Test.Eval.bitvec_AndOrXor_887_2
-<<<<<<< HEAD
 import Test.Eval.g2004h02h23hShiftShiftOverflow_proof
 import Test.Eval.g2004h11h22hMissedhandhfold_proof
 import Test.Eval.g2008h07h08hSubAnd_proof
@@ -128,4 +127,7 @@ import Test.Eval.gunfoldhmaskedhmergehwithhconsthmaskhscalar_proof
 import Test.Eval.gxor2_proof
 import Test.Eval.gxorhofhor_proof
 import Test.Eval.bitvec_InstCombineShift__724
-import «Test.Eval.bitvec_InstCombineShift__497'''»
+import Test.Eval.bitvec_InstCombineShift__497_alt
+import Test.Eval.bitvec_160
+import Test.Eval.bitvec_290__292
+import Test.Eval.bitvec_InstCombineShift__351
diff --git a/Eval/bitvec_160.lean b/Test/Eval/bitvec_160.lean
similarity index 100%
rename from Eval/bitvec_160.lean
rename to Test/Eval/bitvec_160.lean
diff --git a/Eval/bitvec_290__292.lean b/Test/Eval/bitvec_290__292.lean
similarity index 100%
rename from Eval/bitvec_290__292.lean
rename to Test/Eval/bitvec_290__292.lean
diff --git a/Eval/bitvec_InstCombineShift__351.lean b/Test/Eval/bitvec_InstCombineShift__351.lean
similarity index 100%
rename from Eval/bitvec_InstCombineShift__351.lean
rename to Test/Eval/bitvec_InstCombineShift__351.lean
diff --git a/Test/Eval/bitvec_InstCombineShift__497'''.lean b/Test/Eval/bitvec_InstCombineShift__497_alt.lean
similarity index 100%
rename from Test/Eval/bitvec_InstCombineShift__497'''.lean
rename to Test/Eval/bitvec_InstCombineShift__497_alt.lean