Home My Page Projects The Why platform
Summary Activity Forums Tracker Lists Tasks Docs News SCM Files

[#12151] [jessie] incorrect order of translation between types and lemmata

Date:
2011-02-24 10:51
Priority:
3
State:
Open
Submitted by:
Virgile Prevosto (virgile)
Assigned to:
Nobody (None)
Hardware:
none
Product:
none
Operating System:
none
Component:
none
Version:
none
Severity:
none
Resolution:
none
URL:
Summary:
[jessie] incorrect order of translation between types and lemmata

Detailed description
The following jessie file:
# IntModel = bounded
# InvariantPolicy = Arguments
# SeparationPolicy = Regions
# AnnotationPolicy = None
# AbstractDomain = Pol

type foo = 0..1

lemma disjoint :
(\forall foo x;
(! ((x == (0 :> foo)) && (x == (1 :> foo)))))

is translated as a why file where the goal disjoint comes before the axioms on foo_of_integer and integer_of_foo that are necessary for proving it.

No Comments Have Been Posted

Attachments:
Size Name Date By Download
1 KiBbar.why2011-02-24 10:51virgilebar.why
Field Old Value Date By
File Added2109: bar.why2011-02-24 10:51virgile