From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,da7583a21995901b,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.136.71 with SMTP id py7mr1465945pbb.4.1344868027866;
        Mon, 13 Aug 2012 07:27:07 -0700 (PDT)
Path: 
 c10ni111226pbw.0!nntp.google.com!news2.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
From: Ben Hocking <benjaminhocking@gmail.com>
Newsgroups: comp.lang.ada
Subject: Using .rlu files in SPARK Ada
Date: Mon, 13 Aug 2012 07:00:59 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <bbdd7647-8a13-41e1-9db7-b6842c22db0e@googlegroups.com>
NNTP-Posting-Host: 8.25.3.17
Mime-Version: 1.0
X-Trace: posting.google.com 1344868023 769 127.0.0.1 (13 Aug 2012 14:27:03
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 13 Aug 2012 14:27:03 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=8.25.3.17;
 posting-account=hKGsDAoAAAC9HB_9misjykjawYQeT_yf
User-Agent: G2/1.0
Content-Type: text/plain; charset=ISO-8859-1
Date: 2012-08-13T07:00:59-07:00
List-Id: <comp.lang.ada>

I'm trying to satisfy all of the Verification Conditions that SPARK Ada generates in some code of mine.

I've been unable to satisfy the following check statement:
   a2 := x3 - x1;
   b := y3 - y1;
   --# check b < a2 -> (b rem a2 = b);

It generates the following VC:
y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = y3 - y1

In my .rlu file (which I know is being read because other rules are being applied, and I see it mentioned in my .slg file), I have:
small_rem: y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = (y3 - y1) may_be_deduced_from [y3 - y1 < x3 - x1].

(Note that I originally had:
small_rem: x rem y = x may_be_deduced_from [x < y].

However, in an effort to rule out any possible source of confusion, I expanded it to exactly what I was seeing in the .siv file.)

Am I doing something incorrectly, or is there some limitation of SPARK here?