diff --git a/CMakeLists.txt b/CMakeLists.txt
index 015cbddee302..498d562d3dc4 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -59,7 +59,7 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     ExternalProject_add(cadical
       PREFIX cadical
       GIT_REPOSITORY https://github.com/arminbiere/cadical
-      GIT_TAG rel-2.1.2
+      GIT_TAG rel-2.2.0
       CONFIGURE_COMMAND ""
       BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk
         CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
diff --git a/src/Lean/Elab/Tactic/BVDecide/External.lean b/src/Lean/Elab/Tactic/BVDecide/External.lean
index 75485afe3ca3..ceffb15e12ee 100644
--- a/src/Lean/Elab/Tactic/BVDecide/External.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/External.lean
@@ -162,6 +162,11 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
     -/
     "--unsat",
     /-
+    Ensure we don't produce proofs with BVA as our LRAT checker doesn't understand them yet.
+    See: https://github.com/arminbiere/cadical/issues/134
+    -/
+    "--no-factor",
+    /-
     Bitwuzla sets this option and it does improve performance practically:
     https://github.com/bitwuzla/bitwuzla/blob/0e81e616af4d4421729884f01928b194c3536c76/src/sat/cadical.cpp#L34
     -/
diff --git a/src/cadical.mk b/src/cadical.mk
index 81d6d684ced1..635fbe04e143 100644
--- a/src/cadical.mk
+++ b/src/cadical.mk
@@ -3,5 +3,8 @@ CXX ?= c++
 %.o: src/%.cpp
 	$(CXX) -std=c++11 -O3 -DNDEBUG -DNBUILD $(CXXFLAGS) -c $< -o $@
 
-../../cadical$(CMAKE_EXECUTABLE_SUFFIX): $(patsubst src/%.cpp,%.o,$(shell ls src/*.cpp | grep -v mobical))
+%.o: src/%.c
+	$(CC) -O3 -DNDEBUG -DNBUILD $(CFLAGS) -c $< -o $@
+
+../../cadical$(CMAKE_EXECUTABLE_SUFFIX): $(patsubst src/%.cpp,%.o,$(shell ls src/*.cpp | grep -v mobical)) $(patsubst src/%.c,%.o,$(shell ls src/*.c))
 	$(CXX) -o $@ $^ $(LDFLAGS)
diff --git a/tests/lean/run/bv_counterexample.lean b/tests/lean/run/bv_counterexample.lean
index c3081bd7eaa8..b56714cfc908 100644
--- a/tests/lean/run/bv_counterexample.lean
+++ b/tests/lean/run/bv_counterexample.lean
@@ -76,8 +76,8 @@ example (x y : BitVec 32) (a : Bool) (h : x < y) : (x = y) ↔ a := by
 error: The prover found a potentially spurious counterexample:
 - The following potentially relevant hypotheses could not be used: [h]
 Consider the following assignment:
-x = 4294967295#32
-y = 2147483647#32
+x = 0#32
+y = 2147483648#32
 -/
 #guard_msgs in
 example (x y : BitVec 32) (h : x.toNat = y.toNat) : x = y := by
@@ -89,8 +89,8 @@ def zeros (w : Nat) : BitVec w := 0#w
 error: The prover found a potentially spurious counterexample:
 - It abstracted the following unsupported expressions as opaque variables: [zeros 32]
 Consider the following assignment:
-x = 4294967295#32
-zeros 32 = 4294967295#32
+x = 2147483648#32
+zeros 32 = 2147483648#32
 -/
 #guard_msgs in
 example (x : BitVec 32) (h : x = zeros 32) : x = 0 := by
@@ -101,9 +101,9 @@ error: The prover found a potentially spurious counterexample:
 - It abstracted the following unsupported expressions as opaque variables: [zeros 32]
 - The following potentially relevant hypotheses could not be used: [h1]
 Consider the following assignment:
-x = 4294967295#32
-zeros 32 = 4294967295#32
-y = 4294967295#32
+x = 0#32
+zeros 32 = 0#32
+y = 2147483648#32
 -/
 #guard_msgs in
 example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 := by
@@ -111,7 +111,7 @@ example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 :
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-x = 3#2
+x = 0#2
 -/
 #guard_msgs in
 example (x : BitVec 2) : (bif x.ult 1#2 then 1#2 else 2#2) == 3#2 := by
diff --git a/tests/lean/run/bv_sint.lean b/tests/lean/run/bv_sint.lean
index 9968c29ec6c9..2317b7ffc1ac 100644
--- a/tests/lean/run/bv_sint.lean
+++ b/tests/lean/run/bv_sint.lean
@@ -6,8 +6,8 @@ example (a b c : Int8) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a = -1
-b = -1
+a = 0
+b = 0
 -/
 #guard_msgs in
 example (a b : Int8) : a + b > a := by
@@ -21,8 +21,8 @@ example (a b c : Int16) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a = -1
-b = -1
+a = 0
+b = 0
 -/
 #guard_msgs in
 example (a b : Int16) : a + b > a := by
@@ -36,8 +36,8 @@ example (a b c : Int32) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a = -1
-b = -1
+a = 0
+b = 0
 -/
 #guard_msgs in
 example (a b : Int32) : a + b > a := by
@@ -51,8 +51,8 @@ example (a b c : Int64) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a = -1
-b = -1
+a = 0
+b = 0
 -/
 #guard_msgs in
 example (a b : Int64) : a + b > a := by
diff --git a/tests/lean/run/bv_uint.lean b/tests/lean/run/bv_uint.lean
index d37bca07849a..702331bdafc9 100644
--- a/tests/lean/run/bv_uint.lean
+++ b/tests/lean/run/bv_uint.lean
@@ -6,8 +6,8 @@ example (a b c : UInt8) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a = 255
-b = 255
+a = 0
+b = 0
 -/
 #guard_msgs in
 example (a b : UInt8) : a + b > a := by
@@ -21,8 +21,8 @@ example (a b c : UInt16) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a = 65535
-b = 65535
+a = 0
+b = 0
 -/
 #guard_msgs in
 example (a b : UInt16) : a + b > a := by
@@ -36,8 +36,8 @@ example (a b c : UInt32) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a = 4294967295
-b = 4294967295
+a = 0
+b = 0
 -/
 #guard_msgs in
 example (a b : UInt32) : a + b > a := by
@@ -51,8 +51,8 @@ example (a b c : UInt64) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a = 18446744073709551615
-b = 18446744073709551615
+a = 0
+b = 0
 -/
 #guard_msgs in
 example (a b : UInt64) : a + b > a := by
diff --git a/tests/lean/run/bv_unused.lean b/tests/lean/run/bv_unused.lean
index a6ccc7c35453..b4f44b4dbc6d 100644
--- a/tests/lean/run/bv_unused.lean
+++ b/tests/lean/run/bv_unused.lean
@@ -4,7 +4,7 @@ open BitVec
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-y = 18446744073709551615#64
+y = 18446744071562067968#64
 -/
 #guard_msgs in
 example {y : BitVec 64} : zeroExtend 32 y = 0 := by