chore: counter examples changed

Author: hargoniX

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.2.0-rc2
+      GIT_TAG rel-2.2.0
       CONFIGURE_COMMAND ""
       BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk
         CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}

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,17 +101,17 @@ 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
   bv_decide
 
 /--
 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

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

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

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