On 15/10/2017 20:47, Julien Cretin wrote: > Hi club, > > I updated my Why3 from 0.87.3 to 0.88.0 today and had a few issues with > my existing theories. I got some unbound symbol 'BVC.to_uint_small' > errors where BVC is an alias for bv.BVConverter_8_64. I suspect this to > be due to the new quote character syntax in identifiers. I have the same > issue with BV8.to_uint and BV64.to_uint which are also defined using > t'int.
No, this is not due to the quote, this is the standard behavior of cloning in Why3. BV8 contains the following entry: clone export BV_Gen with type t = t, function to_uint = t'int, ... which means that the content of BV_gen is dumped into BV8, but all the occurrences of to_uint are substituted with t'int. > Consider the following theory (that I think used to work on 0.87.3): > > theory Bug > use bv.BV8 > lemma foo: BV8.to_uint BV8.zeros = 0 > end In other words, you should have used lemma foo: BV8.t'int BV8.zeros = 0 > The second lemma (high) is actually proved by CVC4 1.5. But I can't > prove the first with my provers (Alt-Ergo 1.30, CVC4 1.5, and Z3 4.5.0) > and I can't see why it is false. That does not necessarily mean that the first lemma is false (it would be false only if you were able to prove its negation). There are four possible cases: 1. the lemma is actually false, 2. the provers are not powerful enough to prove it, 3. the goal is incorrectly translated to the prover, 4. functions nth and toBig are underspecified. I have no idea which case it is. The statement seems sensible, so I doubt it is the first case, but it might be any of the three other cases. Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
