From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 29 Mar 2021 11:12:07 +0200 Subject: replacing omega with lia in some file --- backend/ValueDomain.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'backend/ValueDomain.v') diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 0f895040..5a7cfc12 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -15,6 +15,7 @@ Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice. Require Import Compopts AST. Require Import Values Memory Globalenvs Builtins Events. Require Import Registers RTL. +Require Import Lia. (** The abstract domains for value analysis *) @@ -2822,8 +2823,8 @@ Proof. generalize (Int.unsigned_range_2 j); intros RANGE. assert (Int.unsigned j <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } - exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. - unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. + exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD. + unfold Int.modu. rewrite Int.unsigned_repr. lia. lia. } intros until y. intros HX HY. -- cgit