Skip to content

Commit be5b58a

Browse files
committed
chore: add another example where omega takes ~1.2s
1 parent 33e872b commit be5b58a

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

tests/bench/omega/omega11.lean

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
theorem t
2+
(a b : BitVec 64)
3+
(an bn : Nat)
4+
(han : an > 0)
5+
(hbn : bn > 0)
6+
(ha : a.toNat + an ≤ 18446744073709551616)
7+
(hb : b.toNat + bn ≤ 18446744073709551616)
8+
(hsep : a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn) :
9+
((¬b - a ≤ a + BitVec.ofNat 64 an - 1#64 - a ∧ ¬b + BitVec.ofNat 64 bn - 1#64 - a ≤ a + BitVec.ofNat 64 an - 1#64 - a) ∧ ¬a - b ≤ b + BitVec.ofNat 64 bn - 1#64 - b) ∧ ¬a + BitVec.ofNat 64 an - 1#64 - b ≤ b + BitVec.ofNat 64 bn - 1#64 - b := by
10+
bv_omega

0 commit comments

Comments
 (0)