File: bug_13227_6.v

package info (click to toggle)
coq-doc 8.16.1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: bookworm
  • size: 42,788 kB
  • sloc: ml: 219,673; sh: 4,035; python: 3,372; ansic: 2,529; makefile: 728; lisp: 279; javascript: 87; xml: 24; sed: 2
file content (16 lines) | stat: -rw-r--r-- 320 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
 
Require Import Lia ZArith.
Open Scope Z_scope.

Unset Lia Cache.

(* Expected time < 1.00s *)
Goal forall (x2 x3 x : Z)
     (H : 0 <= 1073741824 * x + x2 - 67146752)
     (H0 : 0 <= -8192 + x2)
     (H1 : 0 <= 34816 + - x2)
     (H2 : 0 <= -1073741824 * x - x2 + 1073741823),
  False.
Proof.
  intros.
  Time lia.
Qed.