-
Jean-Christophe Filliâtre authored
fixes issue #57 a new theory relations.WellFounded is introduced for this purpose (and must be imported whenever one wants to make use of a custom relation for a variant) it defines, inductively, a notion of accessibility for a given predicate R (x is accessible whenever all elements smaller than x for R are alreay accessible) whenever one has to prove that a variant decreases, a new VC is also generated, to show that the old value of the variant is accessible for the order relation note: accessibility being defined inductively, proving well-foundedness is out of reach of SMT solvers; but at least this is sound now
4af9081d