diff --git a/HumanEvalLean/HumanEval0.lean b/HumanEvalLean/HumanEval0.lean
index 29d904d..f577533 100644
--- a/HumanEvalLean/HumanEval0.lean
+++ b/HumanEvalLean/HumanEval0.lean
@@ -33,13 +33,13 @@ def hasCloseElements (xs : Array Rat) (threshold : Rat) : Bool := Id.run do
 ## Tests
 -/
 
-example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.3 = true := by native_decide
-example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.05 = false := by native_decide
-example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.95 = true := by native_decide
-example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.8 = false := by native_decide
-example : hasCloseElements #[1.0, 2.0, 3.0, 4.0, 5.0, 2.0] 0.1 = true := by native_decide
-example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 1.0 = true := by native_decide
-example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 0.5 = false := by native_decide
+example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.3 = true := by cbv
+example : hasCloseElements #[1.0, 2.0, 3.9, 4.0, 5.0, 2.2] 0.05 = false := by cbv
+example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.95 = true := by cbv
+example : hasCloseElements #[1.0, 2.0, 5.9, 4.0, 5.0] 0.8 = false := by cbv
+example : hasCloseElements #[1.0, 2.0, 3.0, 4.0, 5.0, 2.0] 0.1 = true := by cbv
+example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 1.0 = true := by cbv
+example : hasCloseElements #[1.1, 2.2, 3.1, 4.1, 5.1] 0.5 = false := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval106.lean b/HumanEvalLean/HumanEval106.lean
index ada1b2b..05e4c57 100644
--- a/HumanEvalLean/HumanEval106.lean
+++ b/HumanEvalLean/HumanEval106.lean
@@ -38,10 +38,10 @@ def f (n : Nat) : List Nat := Id.run do
 ### Tests
 -/
 
-example : f 5 = [1, 2, 6, 24, 15] := by native_decide
-example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by native_decide
-example : f 1 = [1] := by native_decide
-example : f 3 = [1, 2, 6] := by native_decide
+example : f 5 = [1, 2, 6, 24, 15] := by cbv
+example : f 7 = [1, 2, 6, 24, 15, 720, 28] := by cbv
+example : f 1 = [1] := by cbv
+example : f 3 = [1, 2, 6] := by cbv
 
 /-!
 ### Verification
@@ -134,10 +134,10 @@ def f' (n : Nat) : Array Nat := Id.run do
 ### Tests
 -/
 
-example : f' 5 = #[1, 2, 6, 24, 15] := by native_decide
-example : f' 7 = #[1, 2, 6, 24, 15, 720, 28] := by native_decide
-example : f' 1 = #[1] := by native_decide
-example : f' 3 = #[1, 2, 6] := by native_decide
+example : f' 5 = #[1, 2, 6, 24, 15] := by cbv
+example : f' 7 = #[1, 2, 6, 24, 15, 720, 28] := by cbv
+example : f' 1 = #[1] := by cbv
+example : f' 3 = #[1, 2, 6] := by cbv
 
 /-!
 ### Verification
@@ -204,10 +204,10 @@ def f'' (n : Nat) : Array Nat := Id.run do
 ### Tests
 -/
 
-example : f'' 5 = #[1, 2, 6, 24, 15] := by native_decide
-example : f'' 7 = #[1, 2, 6, 24, 15, 720, 28] := by native_decide
-example : f'' 1 = #[1] := by native_decide
-example : f'' 3 = #[1, 2, 6] := by native_decide
+example : f'' 5 = #[1, 2, 6, 24, 15] := by cbv
+example : f'' 7 = #[1, 2, 6, 24, 15, 720, 28] := by cbv
+example : f'' 1 = #[1] := by cbv
+example : f'' 3 = #[1, 2, 6] := by cbv
 
 /-!
 ### Verification
diff --git a/HumanEvalLean/HumanEval115.lean b/HumanEvalLean/HumanEval115.lean
index 6e0072e..5a003fd 100644
--- a/HumanEvalLean/HumanEval115.lean
+++ b/HumanEvalLean/HumanEval115.lean
@@ -16,11 +16,11 @@ def maxFill (grid : Vector (Vector Nat n) m) (capacity : Nat) : Nat :=
 # Tests
 -/
 
-example : maxFill #v[#v[0,0,1,0], #v[0,1,0,0], #v[1,1,1,1]]              1 = 6 := by native_decide
-example : maxFill #v[#v[0,0,1,1], #v[0,0,0,0], #v[1,1,1,1], #v[0,1,1,1]] 2 = 5 := by native_decide
-example : maxFill #v[#v[0,0,0],   #v[0,0,0]]                             5 = 0 := by native_decide
-example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]]                           2 = 4 := by native_decide
-example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]]                           9 = 2 := by native_decide
+example : maxFill #v[#v[0,0,1,0], #v[0,1,0,0], #v[1,1,1,1]]              1 = 6 := by cbv
+example : maxFill #v[#v[0,0,1,1], #v[0,0,0,0], #v[1,1,1,1], #v[0,1,1,1]] 2 = 5 := by cbv
+example : maxFill #v[#v[0,0,0],   #v[0,0,0]]                             5 = 0 := by cbv
+example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]]                           2 = 4 := by cbv
+example : maxFill #v[#v[1,1,1,1], #v[1,1,1,1]]                           9 = 2 := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval12.lean b/HumanEvalLean/HumanEval12.lean
index 84a8192..a3cbbbe 100644
--- a/HumanEvalLean/HumanEval12.lean
+++ b/HumanEvalLean/HumanEval12.lean
@@ -37,9 +37,9 @@ def longest? (xs : List String) : Option String :=
 ## Tests
 -/
 
-example : longest? [] = none := by native_decide
-example : longest? ["x", "y", "z"] = some "x" := by native_decide
-example : longest? ["x", "yyy", "zzzz", "www", "kkkk", "abc"] = some "zzzz" := by native_decide
+example : longest? [] = none := by cbv
+example : longest? ["x", "y", "z"] = some "x" := by cbv
+example : longest? ["x", "yyy", "zzzz", "www", "kkkk", "abc"] = some "zzzz" := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval122.lean b/HumanEvalLean/HumanEval122.lean
index 2daf409..254ada5 100644
--- a/HumanEvalLean/HumanEval122.lean
+++ b/HumanEvalLean/HumanEval122.lean
@@ -25,11 +25,11 @@ def addElements (xs : Array Int) (k : Nat) : Int :=
 ## Tests
 -/
 
-example : addElements #[1,-2,-3,41,57,76,87,88,99] 3 = -4 := by native_decide
-example : addElements #[111,121,3,4000,5,6] 2 = 0 := by native_decide
-example : addElements #[11,21,3,90,5,6,7,8,9] 4 = 125 := by native_decide
-example : addElements #[111,21,3,4000,5,6,7,8,9] 4 = 24 := by native_decide
-example : addElements #[1] 1 = 1 := by native_decide
+example : addElements #[1,-2,-3,41,57,76,87,88,99] 3 = -4 := by cbv
+example : addElements #[111,121,3,4000,5,6] 2 = 0 := by cbv
+example : addElements #[11,21,3,90,5,6,7,8,9] 4 = 125 := by cbv
+example : addElements #[111,21,3,4000,5,6,7,8,9] 4 = 24 := by cbv
+example : addElements #[1] 1 = 1 := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval128.lean b/HumanEvalLean/HumanEval128.lean
index 6bf2dfd..27ce647 100644
--- a/HumanEvalLean/HumanEval128.lean
+++ b/HumanEvalLean/HumanEval128.lean
@@ -68,14 +68,14 @@ def prodSigns (arr : List Int) : Option Int := do
 ## Tests
 -/
 
-example : prodSigns [1, 2, 2, -4] = some (-9) := by native_decide
-example : prodSigns [0, 1] = some 0 := by native_decide
-example : prodSigns [] = none := by native_decide
-example : prodSigns [1, 1, 1, 2, 3, -1, 1] = some (-10) := by native_decide
-example : prodSigns [2, 4, 1, 2, -1, -1, 9] = some 20 := by native_decide
-example : prodSigns [-1, 1, -1, 1] = some 4 := by native_decide
-example : prodSigns [-1, 1, 1, 1] = some (-4) := by native_decide
-example : prodSigns [-1, 1, 1, 0] = some 0 := by native_decide
+example : prodSigns [1, 2, 2, -4] = some (-9) := by cbv
+example : prodSigns [0, 1] = some 0 := by cbv
+example : prodSigns [] = none := by cbv
+example : prodSigns [1, 1, 1, 2, 3, -1, 1] = some (-10) := by cbv
+example : prodSigns [2, 4, 1, 2, -1, -1, 9] = some 20 := by cbv
+example : prodSigns [-1, 1, -1, 1] = some 4 := by cbv
+example : prodSigns [-1, 1, 1, 1] = some (-4) := by cbv
+example : prodSigns [-1, 1, 1, 0] = some 0 := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval13.lean b/HumanEvalLean/HumanEval13.lean
index 9493d31..60c503f 100644
--- a/HumanEvalLean/HumanEval13.lean
+++ b/HumanEvalLean/HumanEval13.lean
@@ -8,10 +8,10 @@ There is nothing to implement: The standard library provides `Int.gcd` out of th
 ## Tests
 -/
 
-example : Int.gcd 3 7 = 1 := by native_decide
-example : Int.gcd 10 15 = 5 := by native_decide
-example : Int.gcd 49 14 = 7 := by native_decide
-example : Int.gcd 144 60 = 12 := by native_decide
+example : Int.gcd 3 7 = 1 := by cbv
+example : Int.gcd 10 15 = 5 := by cbv
+example : Int.gcd 49 14 = 7 := by cbv
+example : Int.gcd 144 60 = 12 := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval133.lean b/HumanEvalLean/HumanEval133.lean
index 13a04d4..be04ec9 100644
--- a/HumanEvalLean/HumanEval133.lean
+++ b/HumanEvalLean/HumanEval133.lean
@@ -5,18 +5,18 @@ def sumSquares (xs : List Rat) : Int :=
 
 /-! ## Tests -/
 
-example : sumSquares [1, 2, 3] = 14 := by native_decide
-example : sumSquares [1.0, 2, 3] = 14 := by native_decide
-example : sumSquares [1, 3, 5, 7] = 84 := by native_decide
-example : sumSquares [1.4, 4.2, 0] = 29 := by native_decide
-example : sumSquares [-2.4, 1, 1] = 6 := by native_decide
-example : sumSquares [100, 1, 15, 2] = 10230 := by native_decide
-example : sumSquares [10000, 10000] = 200000000 := by native_decide
-example : sumSquares [-1.4, 4.6, 6.3] = 75 := by native_decide
-example : sumSquares [-1.4, 17.9, 18.9, 19.9] = 1086 := by native_decide
-example : sumSquares [0] = 0 := by native_decide
-example : sumSquares [-1] = 1 := by native_decide
-example : sumSquares [-1, 1, 0] = 2 := by native_decide
+example : sumSquares [1, 2, 3] = 14 := by cbv
+example : sumSquares [1.0, 2, 3] = 14 := by cbv
+example : sumSquares [1, 3, 5, 7] = 84 := by cbv
+example : sumSquares [1.4, 4.2, 0] = 29 := by cbv
+example : sumSquares [-2.4, 1, 1] = 6 := by cbv
+example : sumSquares [100, 1, 15, 2] = 10230 := by cbv
+example : sumSquares [10000, 10000] = 200000000 := by cbv
+example : sumSquares [-1.4, 4.6, 6.3] = 75 := by cbv
+example : sumSquares [-1.4, 17.9, 18.9, 19.9] = 1086 := by cbv
+example : sumSquares [0] = 0 := by cbv
+example : sumSquares [-1] = 1 := by cbv
+example : sumSquares [-1, 1, 0] = 2 := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval139.lean b/HumanEvalLean/HumanEval139.lean
index cd3c345..9ad68b8 100644
--- a/HumanEvalLean/HumanEval139.lean
+++ b/HumanEvalLean/HumanEval139.lean
@@ -45,10 +45,10 @@ theorem special_factorial_func_correct {n : Nat} :
     apply this <;> simp [Nat.factorial, Nat.brazilianFactorial]
   intros; fun_induction special_factorial.go <;> grind [Nat.factorial, Nat.brazilianFactorial]
 
-theorem test1 : special_factorial 4 = 288 := by native_decide
-theorem test2 : special_factorial 5 = 34560 := by native_decide
-theorem test3 : special_factorial 7 = 125411328000 := by native_decide
-theorem test4 : special_factorial 1 = 1 := by native_decide
+theorem test1 : special_factorial 4 = 288 := by cbv
+theorem test2 : special_factorial 5 = 34560 := by cbv
+theorem test3 : special_factorial 7 = 125411328000 := by cbv
+theorem test4 : special_factorial 1 = 1 := by cbv
 
 /-!
 ## Prompt
diff --git a/HumanEvalLean/HumanEval2.lean b/HumanEvalLean/HumanEval2.lean
index 0ce6da3..3badb2d 100644
--- a/HumanEvalLean/HumanEval2.lean
+++ b/HumanEvalLean/HumanEval2.lean
@@ -13,9 +13,9 @@ def truncateNumber (x : Rat) : Rat :=
 ## Tests
 -/
 
-example : truncateNumber (7/2) = 1/2 := by native_decide
-example : truncateNumber (133/100) = 33/100 := by native_decide
-example : truncateNumber (123456/1000) = 456/1000 := by native_decide
+example : truncateNumber (7/2) = 1/2 := by cbv
+example : truncateNumber (133/100) = 33/100 := by cbv
+example : truncateNumber (123456/1000) = 456/1000 := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval22.lean b/HumanEvalLean/HumanEval22.lean
index cbcd720..fdefe3d 100644
--- a/HumanEvalLean/HumanEval22.lean
+++ b/HumanEvalLean/HumanEval22.lean
@@ -30,9 +30,9 @@ def filterIntegers (xs : Array Any): Array Int :=
 
 /-! ## Tests -/
 
-example : filterIntegers #[] = #[] := by native_decide
-example : filterIntegers #[.int 4, .float 23.2, .int 9, .string "adasd"] = #[4, 9] := by native_decide
-example : filterIntegers #[.int 3, .string "c", .int 3, .int 3, .string "a", .string "b"] = #[3, 3, 3] := by native_decide
+example : filterIntegers #[] = #[] := by cbv
+example : filterIntegers #[.int 4, .float 23.2, .int 9, .string "adasd"] = #[4, 9] := by cbv
+example : filterIntegers #[.int 3, .string "c", .int 3, .int 3, .string "a", .string "b"] = #[3, 3, 3] := by cbv
 
 /-! ## Verification -/
 
diff --git a/HumanEvalLean/HumanEval24.lean b/HumanEvalLean/HumanEval24.lean
index 4c9a51d..a53229f 100644
--- a/HumanEvalLean/HumanEval24.lean
+++ b/HumanEvalLean/HumanEval24.lean
@@ -19,11 +19,11 @@ where
       | i + 2 => exact Nat.lt_of_lt_of_le (Nat.lt_mul_self_iff.2 (by omega)) (Nat.not_lt.1 h)
     omega
 
-example : largestDivisor 3 = 1 := by native_decide
-example : largestDivisor 7 = 1 := by native_decide
-example : largestDivisor 10 = 5 := by native_decide
-example : largestDivisor 100 = 50 := by native_decide
-example : largestDivisor 49 = 7 := by native_decide
+example : largestDivisor 3 = 1 := by cbv
+example : largestDivisor 7 = 1 := by cbv
+example : largestDivisor 10 = 5 := by cbv
+example : largestDivisor 100 = 50 := by cbv
+example : largestDivisor 49 = 7 := by cbv
 
 inductive LargestDivisorSpec (n : Nat) : Nat → Prop
   | one : (∀ j, 2 ≤ j → j * j ≤ n → n % j ≠ 0) → LargestDivisorSpec n 1
diff --git a/HumanEvalLean/HumanEval25.lean b/HumanEvalLean/HumanEval25.lean
index da96e86..ab095b1 100644
--- a/HumanEvalLean/HumanEval25.lean
+++ b/HumanEvalLean/HumanEval25.lean
@@ -27,16 +27,16 @@ def factorize (x : Nat) : Array Nat :=
 
 /-! ## Tests -/
 
-example : factorize 2 = #[2] := by native_decide
-example : factorize 4 = #[2, 2] := by native_decide
-example : factorize 8 = #[2, 2, 2] := by native_decide
-example : factorize 25 = #[5, 5] := by native_decide
-example : factorize 70 = #[2, 5, 7] := by native_decide
-example : factorize 57 = #[3, 19] := by native_decide
-example : factorize 3249 = #[3, 3, 19, 19] := by native_decide
-example : factorize 185193 = #[3, 3, 3, 19, 19, 19] := by native_decide
-example : factorize 20577 = #[3, 19, 19, 19] := by native_decide
-example : factorize 18 = #[2, 3, 3] := by native_decide
+example : factorize 2 = #[2] := by cbv
+example : factorize 4 = #[2, 2] := by cbv
+example : factorize 8 = #[2, 2, 2] := by cbv
+example : factorize 25 = #[5, 5] := by cbv
+example : factorize 70 = #[2, 5, 7] := by cbv
+example : factorize 57 = #[3, 19] := by cbv
+example : factorize 3249 = #[3, 3, 19, 19] := by cbv
+example : factorize 185193 = #[3, 3, 3, 19, 19, 19] := by cbv
+example : factorize 20577 = #[3, 19, 19, 19] := by cbv
+example : factorize 18 = #[2, 3, 3] := by cbv
 
 /-! ## Verification -/
 
diff --git a/HumanEvalLean/HumanEval26.lean b/HumanEvalLean/HumanEval26.lean
index e49545e..d4afc2f 100644
--- a/HumanEvalLean/HumanEval26.lean
+++ b/HumanEvalLean/HumanEval26.lean
@@ -17,9 +17,9 @@ def removeDuplicates (xs : Array Int) : Array Int :=
 
 /-! ## Tests -/
 
-example : removeDuplicates #[] = #[] := by native_decide
-example : removeDuplicates #[1, 2, 3, 4] = #[1, 2, 3, 4] := by native_decide
-example : removeDuplicates #[1, 2, 3, 2, 4, 3, 5] = #[1, 4, 5] := by native_decide
+example : removeDuplicates #[] = #[] := by cbv
+example : removeDuplicates #[1, 2, 3, 4] = #[1, 2, 3, 4] := by cbv
+example : removeDuplicates #[1, 2, 3, 2, 4, 3, 5] = #[1, 4, 5] := by cbv
 
 /-! ## Missing API -/
 
diff --git a/HumanEvalLean/HumanEval30.lean b/HumanEvalLean/HumanEval30.lean
index bdb30f6..a15afce 100644
--- a/HumanEvalLean/HumanEval30.lean
+++ b/HumanEvalLean/HumanEval30.lean
@@ -13,10 +13,10 @@ def getPositive (xs : Array Int): Array Int :=
 
 /-! ## Tests -/
 
-example : getPositive #[-1, -2, 4, 5, 6] = #[4, 5, 6] := by native_decide
-example : getPositive #[5, 3, -5, 2, 3, 3, 9, 0, 123, 1, -10] = #[5, 3, 2, 3, 3, 9, 123, 1] := by native_decide
-example : getPositive #[-1, -2] = #[] := by native_decide
-example : getPositive #[] = #[] := by native_decide
+example : getPositive #[-1, -2, 4, 5, 6] = #[4, 5, 6] := by cbv
+example : getPositive #[5, 3, -5, 2, 3, 3, 9, 0, 123, 1, -10] = #[5, 3, 2, 3, 3, 9, 123, 1] := by cbv
+example : getPositive #[-1, -2] = #[] := by cbv
+example : getPositive #[] = #[] := by cbv
 
 /-! ## Verification -/
 
diff --git a/HumanEvalLean/HumanEval4.lean b/HumanEvalLean/HumanEval4.lean
index fb293cf..5ef1e36 100644
--- a/HumanEvalLean/HumanEval4.lean
+++ b/HumanEvalLean/HumanEval4.lean
@@ -30,9 +30,9 @@ def meanAbsoluteDeviation (xs : Array Rat) : Rat :=
 
 /-! ## Tests -/
 
-example : meanAbsoluteDeviation #[(1 : Rat), 2, 3] = (2 : Rat) / 3 := by native_decide
-example : meanAbsoluteDeviation #[(1 : Rat), 2, 3, 4] = 1 := by native_decide
-example : meanAbsoluteDeviation #[(1 : Rat), 2, 3, 4, 5] = (6 : Rat) / 5 := by native_decide
+example : meanAbsoluteDeviation #[(1 : Rat), 2, 3] = (2 : Rat) / 3 := by cbv
+example : meanAbsoluteDeviation #[(1 : Rat), 2, 3, 4] = 1 := by cbv
+example : meanAbsoluteDeviation #[(1 : Rat), 2, 3, 4, 5] = (6 : Rat) / 5 := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval40.lean b/HumanEvalLean/HumanEval40.lean
index dab30ce..32d3302 100644
--- a/HumanEvalLean/HumanEval40.lean
+++ b/HumanEvalLean/HumanEval40.lean
@@ -28,15 +28,15 @@ public def triplesSumToZero (xs : Array Int) : Bool := Id.run do
 
 /-! ## Tests 1 -/
 
-example : triplesSumToZero #[1, 3, 5, 0] = false := by native_decide
-example : triplesSumToZero #[1, 3, 5, -1] = false := by native_decide
-example : triplesSumToZero #[1, 3, -2, 1] = true := by native_decide
-example : triplesSumToZero #[1, 2, 3, 7] = false := by native_decide
-example : triplesSumToZero #[1, 2, 5, 7] = false := by native_decide
-example : triplesSumToZero #[2, 4, -5, 3, 9, 7] = true := by native_decide
-example : triplesSumToZero #[1] = false := by native_decide
-example : triplesSumToZero #[1, 3, 5, -100] = false := by native_decide
-example : triplesSumToZero #[100, 3, 5, -100] = false := by native_decide
+example : triplesSumToZero #[1, 3, 5, 0] = false := by cbv
+example : triplesSumToZero #[1, 3, 5, -1] = false := by cbv
+example : triplesSumToZero #[1, 3, -2, 1] = true := by cbv
+example : triplesSumToZero #[1, 2, 3, 7] = false := by cbv
+example : triplesSumToZero #[1, 2, 5, 7] = false := by cbv
+example : triplesSumToZero #[2, 4, -5, 3, 9, 7] = true := by cbv
+example : triplesSumToZero #[1] = false := by cbv
+example : triplesSumToZero #[1, 3, 5, -100] = false := by cbv
+example : triplesSumToZero #[100, 3, 5, -100] = false := by cbv
 
 /-! ## Missing API -/
 
@@ -134,15 +134,15 @@ where
 
 /-! ## Tests 2 -/
 
-example : triplesSumToZero' #[1, 3, 5, 0] = false := by native_decide
-example : triplesSumToZero' #[1, 3, 5, -1] = false := by native_decide
-example : triplesSumToZero' #[1, 3, -2, 1] = true := by native_decide
-example : triplesSumToZero' #[1, 2, 3, 7] = false := by native_decide
-example : triplesSumToZero' #[1, 2, 5, 7] = false := by native_decide
-example : triplesSumToZero' #[2, 4, -5, 3, 9, 7] = true := by native_decide
-example : triplesSumToZero' #[1] = false := by native_decide
-example : triplesSumToZero' #[1, 3, 5, -100] = false := by native_decide
-example : triplesSumToZero' #[100, 3, 5, -100] = false := by native_decide
+example : triplesSumToZero' #[1, 3, 5, 0] = false := by cbv
+example : triplesSumToZero' #[1, 3, 5, -1] = false := by cbv
+example : triplesSumToZero' #[1, 3, -2, 1] = true := by cbv
+example : triplesSumToZero' #[1, 2, 3, 7] = false := by cbv
+example : triplesSumToZero' #[1, 2, 5, 7] = false := by cbv
+example : triplesSumToZero' #[2, 4, -5, 3, 9, 7] = true := by cbv
+example : triplesSumToZero' #[1] = false := by cbv
+example : triplesSumToZero' #[1, 3, 5, -100] = false := by cbv
+example : triplesSumToZero' #[100, 3, 5, -100] = false := by cbv
 
 /-! ## Verification 2 -/
 
diff --git a/HumanEvalLean/HumanEval45.lean b/HumanEvalLean/HumanEval45.lean
index 9581302..207563c 100644
--- a/HumanEvalLean/HumanEval45.lean
+++ b/HumanEvalLean/HumanEval45.lean
@@ -7,9 +7,9 @@ def triangleArea (a h : Rat) : Rat :=
 
 /-! ## Tests -/
 
-example : triangleArea 5 3 = 7.5 := by native_decide
-example : triangleArea 2 2 = 2.0 := by native_decide
-example : triangleArea 10 8 = 40.0 := by native_decide
+example : triangleArea 5 3 = 7.5 := by cbv
+example : triangleArea 2 2 = 2.0 := by cbv
+example : triangleArea 10 8 = 40.0 := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval46.lean b/HumanEvalLean/HumanEval46.lean
index e0b2337..43a1404 100644
--- a/HumanEvalLean/HumanEval46.lean
+++ b/HumanEvalLean/HumanEval46.lean
@@ -15,10 +15,10 @@ def fib4 (n : Nat) : Nat := Id.run do
 
 /-! ## Tests -/
 
-example : fib4 5 = 4 := by native_decide
-example : fib4 8 = 28 := by native_decide
-example : fib4 10 = 104 := by native_decide
-example : fib4 12 = 386 := by native_decide
+example : fib4 5 = 4 := by cbv
+example : fib4 8 = 28 := by cbv
+example : fib4 10 = 104 := by cbv
+example : fib4 12 = 386 := by cbv
 
 /-! ## Missing API -/
 
diff --git a/HumanEvalLean/HumanEval49.lean b/HumanEvalLean/HumanEval49.lean
index 7053e33..fe19ecb 100644
--- a/HumanEvalLean/HumanEval49.lean
+++ b/HumanEvalLean/HumanEval49.lean
@@ -9,13 +9,13 @@ def modp (n p : Nat) : Nat :=
 
 /-! ## Tests -/
 
-example : modp 3 5 = 3 := by native_decide
-example : modp 1101 101 = 2 := by native_decide
-example : modp 0 101 = 1 := by native_decide
-example : modp 3 11 = 8 := by native_decide
-example : modp 100 101 = 1 := by native_decide
-example : modp 30 5 = 4 := by native_decide
-example : modp 31 5 = 3 := by native_decide
+example : modp 3 5 = 3 := by cbv
+example : modp 1101 101 = 2 := by native_decide -- `cbv` reaches resource limits
+example : modp 0 101 = 1 := by cbv
+example : modp 3 11 = 8 := by cbv
+example : modp 100 101 = 1 := by cbv
+example : modp 30 5 = 4 := by cbv
+example : modp 31 5 = 3 := by cbv
 
 /-! ## Verification -/
 
diff --git a/HumanEvalLean/HumanEval51.lean b/HumanEvalLean/HumanEval51.lean
index ec6b9f4..b628a3c 100644
--- a/HumanEvalLean/HumanEval51.lean
+++ b/HumanEvalLean/HumanEval51.lean
@@ -18,11 +18,11 @@ def RemoveVowelsIff (solution : String → String) : Prop :=
 def removeVowels (s : String) : String :=
     String.ofList (s.toList.filter (· ∉ vowels))
 
-example : removeVowels "abcdef" = "bcdf" := by native_decide
-example : removeVowels "abcdef\nghijklm" = "bcdf\nghjklm" := by native_decide
-example : removeVowels "aaaaa" = "" := by native_decide
-example : removeVowels "aaBAA" = "B" := by native_decide
-example : removeVowels "zbcd" = "zbcd" := by native_decide
+example : removeVowels "abcdef" = "bcdf" := by cbv
+example : removeVowels "abcdef\nghijklm" = "bcdf\nghjklm" := by cbv
+example : removeVowels "aaaaa" = "" := by cbv
+example : removeVowels "aaBAA" = "B" := by cbv
+example : removeVowels "zbcd" = "zbcd" := by cbv
 
 theorem IsSubseq.length_le {s t : String} (hst : IsSubseq s t) :
     s.length ≤ t.length :=
diff --git a/HumanEvalLean/HumanEval59.lean b/HumanEvalLean/HumanEval59.lean
index b0bebbc..fb8188a 100644
--- a/HumanEvalLean/HumanEval59.lean
+++ b/HumanEvalLean/HumanEval59.lean
@@ -46,11 +46,11 @@ def largestPrimeFactor (n : Nat) : Nat := Id.run do
 
 /-! ## Tests -/
 
-example : largestPrimeFactor 15 = 5 := by native_decide
-example : largestPrimeFactor 27 = 3 := by native_decide
-example : largestPrimeFactor 63 = 7 := by native_decide
-example : largestPrimeFactor 330 = 11 := by native_decide
-example : largestPrimeFactor 13195 = 29 := by native_decide
+example : largestPrimeFactor 15 = 5 := by cbv
+example : largestPrimeFactor 27 = 3 := by cbv
+example : largestPrimeFactor 63 = 7 := by cbv
+example : largestPrimeFactor 330 = 11 := by native_decide -- `cbv` reaches resource limits
+example : largestPrimeFactor 13195 = 29 := by native_decide -- `cbv` reaches resource limits
 
 /-! ## Missing API -/
 
diff --git a/HumanEvalLean/HumanEval60.lean b/HumanEvalLean/HumanEval60.lean
index ea33c20..3054e9c 100644
--- a/HumanEvalLean/HumanEval60.lean
+++ b/HumanEvalLean/HumanEval60.lean
@@ -35,11 +35,11 @@ def sumToN' (n : Nat) : Nat :=
 
 /-! ## Tests 2 -/
 
-example : sumToN' 1 = 1 := by native_decide
-example : sumToN' 6 = 21 := by native_decide
-example : sumToN' 11 = 66 := by native_decide
-example : sumToN' 30 = 465 := by native_decide
-example : sumToN' 100 = 5050 := by native_decide
+example : sumToN' 1 = 1 := by cbv
+example : sumToN' 6 = 21 := by cbv
+example : sumToN' 11 = 66 := by cbv
+example : sumToN' 30 = 465 := by cbv
+example : sumToN' 100 = 5050 := by cbv
 
 /-! ## Verification 2 -/
 
diff --git a/HumanEvalLean/HumanEval63.lean b/HumanEvalLean/HumanEval63.lean
index c2dc135..4136387 100644
--- a/HumanEvalLean/HumanEval63.lean
+++ b/HumanEvalLean/HumanEval63.lean
@@ -19,13 +19,13 @@ def fibfib (n : Nat) : Nat := Id.run do
 
 /-! ## Tests -/
 
-example : fibfib 2 = 1 := by native_decide
-example : fibfib 1 = 0 := by native_decide
-example : fibfib 5 = 4 := by native_decide
-example : fibfib 8 = 24 := by native_decide
-example : fibfib 10 = 81 := by native_decide
-example : fibfib 12 = 274 := by native_decide
-example : fibfib 14 = 927 := by native_decide
+example : fibfib 2 = 1 := by cbv
+example : fibfib 1 = 0 := by cbv
+example : fibfib 5 = 4 := by cbv
+example : fibfib 8 = 24 := by cbv
+example : fibfib 10 = 81 := by cbv
+example : fibfib 12 = 274 := by cbv
+example : fibfib 14 = 927 := by cbv
 
 /-! ## Missing API -/
 
diff --git a/HumanEvalLean/HumanEval7.lean b/HumanEvalLean/HumanEval7.lean
index ce70897..7a99c03 100644
--- a/HumanEvalLean/HumanEval7.lean
+++ b/HumanEvalLean/HumanEval7.lean
@@ -4,10 +4,10 @@ def filterBySubstring (strings : Array String) (substring : String) : Array Stri
   -- Uses KMP string search!
   strings.filter (·.contains substring)
 
-example : filterBySubstring #[] "john" = #[] := by native_decide
-example : filterBySubstring #["xxx", "asd", "xxy", "john doe", "xxxAAA", "xxx"] "xxx" = #["xxx", "xxxAAA", "xxx"] := by native_decide
-example : filterBySubstring #["xxx", "asd", "aaaxxy", "john doe", "xxxAAA", "xxx"] "xx" = #["xxx", "aaaxxy", "xxxAAA", "xxx"] := by native_decide
-example : filterBySubstring #["grunt", "trumpet", "prune", "gruesome"] "run" = #["grunt", "prune"] := by native_decide
+example : filterBySubstring #[] "john" = #[] := by cbv
+example : filterBySubstring #["xxx", "asd", "xxy", "john doe", "xxxAAA", "xxx"] "xxx" = #["xxx", "xxxAAA", "xxx"] := by cbv
+example : filterBySubstring #["xxx", "asd", "aaaxxy", "john doe", "xxxAAA", "xxx"] "xx" = #["xxx", "aaaxxy", "xxxAAA", "xxx"] := by cbv
+example : filterBySubstring #["grunt", "trumpet", "prune", "gruesome"] "run" = #["grunt", "prune"] := by cbv
 
 open Classical in
 theorem filterBySubstring_eq {strings : Array String} {substring : String} :
diff --git a/HumanEvalLean/HumanEval76.lean b/HumanEvalLean/HumanEval76.lean
index 31caf2f..bf631b9 100644
--- a/HumanEvalLean/HumanEval76.lean
+++ b/HumanEvalLean/HumanEval76.lean
@@ -32,16 +32,16 @@ def isSimplePower (x n : Nat) : Bool :=
 ## Tests
 -/
 
-example : isSimplePower 16 2 = true := by native_decide
-example : isSimplePower 143214 16 = false := by native_decide
-example : isSimplePower 4 2 = true := by native_decide
-example : isSimplePower 9 3 = true := by native_decide
-example : isSimplePower 16 4 = true := by native_decide
-example : isSimplePower 24 2 = false := by native_decide
-example : isSimplePower 128 4 = false := by native_decide
-example : isSimplePower 12 6 = false := by native_decide
-example : isSimplePower 1 1 = true := by native_decide
-example : isSimplePower 1 12 = true := by native_decide
+example : isSimplePower 16 2 = true := by cbv
+example : isSimplePower 143214 16 = false := by cbv
+example : isSimplePower 4 2 = true := by cbv
+example : isSimplePower 9 3 = true := by cbv
+example : isSimplePower 16 4 = true := by cbv
+example : isSimplePower 24 2 = false := by cbv
+example : isSimplePower 128 4 = false := by cbv
+example : isSimplePower 12 6 = false := by cbv
+example : isSimplePower 1 1 = true := by cbv
+example : isSimplePower 1 12 = true := by cbv
 
 /-!
 ## Verification
diff --git a/HumanEvalLean/HumanEval77.lean b/HumanEvalLean/HumanEval77.lean
index 8eccd9b..5024c7d 100644
--- a/HumanEvalLean/HumanEval77.lean
+++ b/HumanEvalLean/HumanEval77.lean
@@ -19,14 +19,14 @@ def isCube (x : Int) : Bool :=
 
 /-! ## Tests -/
 
-example : isCube 1 = true := by native_decide
-example : isCube 2 = false := by native_decide
-example : isCube (-1) = true := by native_decide
-example : isCube 64 = true := by native_decide
-example : isCube 180 = false := by native_decide
-example : isCube 1000 = true := by native_decide
-example : isCube 0 = true := by native_decide
-example : isCube 1729 = false := by native_decide
+example : isCube 1 = true := by cbv
+example : isCube 2 = false := by cbv
+example : isCube (-1) = true := by cbv
+example : isCube 64 = true := by cbv
+example : isCube 180 = false := by cbv
+example : isCube 1000 = true := by native_decide -- `cbv` reaches resource limits
+example : isCube 0 = true := by cbv
+example : isCube 1729 = false := by native_decide -- `cbv` reaches resource limits
 
 /-! ## Missing API -/