mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
25 lines
961 B
Lean4
25 lines
961 B
Lean4
import Std.Tactic.BVDecide
|
|
|
|
open BitVec
|
|
|
|
/--
|
|
error: The SAT solver timed out while solving the problem.
|
|
Consider increasing the timeout with the `timeout` config option.
|
|
If solving your problem relies inherently on using associativity or commutativity, consider enabling the `acNf` config option.
|
|
-/
|
|
#guard_msgs in
|
|
theorem timeout (x y z : BitVec 1024) : x - (y + z) = x - y - z := by
|
|
bv_decide (config := { timeout := 1 })
|
|
|
|
/--
|
|
error: None of the hypotheses are in the supported BitVec fragment after applying preprocessing.
|
|
There are three potential reasons for this:
|
|
1. If you are using custom BitVec constructs simplify them to built-in ones.
|
|
2. If your problem is using only built-in ones it might currently be out of reach.
|
|
Consider expressing it in terms of different operations that are better supported.
|
|
3. The original goal was reduced to False and is thus invalid.
|
|
-/
|
|
#guard_msgs in
|
|
theorem no_hyps (x y : Nat) : x * y = y * x := by
|
|
bv_decide
|