From 49bd402359ecc4f0240b6dd849560585542981ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 24 Sep 2024 10:38:17 +0200
Subject: [PATCH] release

---
 Leanwuzla.lean | 11 +++++------
 lean-toolchain |  2 +-
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/Leanwuzla.lean b/Leanwuzla.lean
index 0a534da..fb948b4 100644
--- a/Leanwuzla.lean
+++ b/Leanwuzla.lean
@@ -145,7 +145,7 @@ def smtQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (tim
         throwError s!"The external prover produced unexpected output, stdout:\n{stdout}stderr:\n{stderr}"
 
 def bitwuzla (reflectionResult : ReflectionResult) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
-    MetaM UnsatProver.Result := do
+    MetaM (Except CounterExample UnsatProver.Result) := do
   let smt := toSMT reflectionResult.bvExpr atomsAssignment
   trace[Meta.Tactic.bv] s!"Encoded as SMT: {smt}"
   let res ←
@@ -161,14 +161,13 @@ def bitwuzla (reflectionResult : ReflectionResult) (atomsAssignment : Std.HashMa
   | .sat .. => throwError "Bitwuzla found a counter example"
   | .unsat => throwError "Bitwuzla thinks it's right but can't trust the wuzla!"
 
-def bvBitwuzla (g : MVarId) : MetaM Result := do
-  let ⟨g?, simpTrace⟩ ← Normalize.bvNormalize g
-  let some g := g? | return ⟨simpTrace, none⟩
+def bvBitwuzla (g : MVarId) : MetaM Unit := do
+  let ⟨g?, _⟩ ← Normalize.bvNormalize g
+  let some g := g? | return ()
   let unsatProver : UnsatProver := fun reflectionResult atomsAssignment => do
     withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
       bitwuzla reflectionResult atomsAssignment
-  let lratCert ← closeWithBVReflection g unsatProver
-  return ⟨simpTrace, some lratCert⟩
+  discard <| closeWithBVReflection g unsatProver
 
 
 @[tactic bvBitwuzla]
diff --git a/lean-toolchain b/lean-toolchain
index dcca6df..98d327e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-lean4
+leanprover/lean4:nightly-2024-09-24