refactor: different closing semantics

Leanwuzla.lean

@@ -409,14 +409,10 @@ def evalLeanSat (g : MVarId) (cfg : TacticContext) : MetaM LeansatPerf := do
     | .error _ =>
       return .failure overallTime (← parseFailureTrace traces)
 
-private axiom benchAxiom (α : Prop) : α
-
 def bvCompare (g : MVarId) (solverPath : System.FilePath) (cfg : TacticContext) : MetaM Comparision := do
   let bitwuzlaPerf ← measure evalBitwuzla g solverPath
   let leansatPerf ← measure evalLeanSat g cfg
 
-  g.assign (mkApp (mkConst ``benchAxiom) (← g.getType))
-
   return { bitwuzlaPerf , leansatPerf }
 where
   withFreshTraceState {α : Type} (x : MetaM α) : MetaM α := do
@@ -436,8 +432,7 @@ where
       withOptions setTraceOptions <| withoutModifyingEnv <| withoutModifyingState <| withFreshTraceState do
         f g arg
     catch e =>
-      if (← Lean.isTracingEnabledFor `Meta.Tactic.bv) then
-        logError e.toMessageData
+      logError e.toMessageData
       return none
 
 @[tactic bvCompare]

Test/BVCompare.lean

@@ -10,23 +10,29 @@ variable (x y z : BitVec 32)
 
 example : x + y = y + x := by
   bv_compare
+  sorry
 
 example : x - 1 ≠ x := by
   bv_compare
+  sorry
 
 example : ∀ (x : BitVec 32), x.and 0#32 = 0#32 := by
   bv_compare
+  sorry
 
 example : ∀ (x x_1 : BitVec 16), BitVec.truncate 8 ((x_1.and 255#16).and x) = BitVec.truncate 8 (x_1.and x) := by
   bv_compare
+  sorry
 
 example : ∀ (x : BitVec 1), BitVec.ofBool (0#1 > x) = 0#1 := by
   bv_compare
+  sorry
 
 theorem extracted_1 (x y : BitVec 8) : x + y = x + x := by
   bv_compare
+  sorry
 
-set_option trace.Meta.Tactic.bv true
 set_option sat.timeout 1
 example (x y : BitVec 64) : x * y = y * x := by
   bv_compare
+  sorry