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. 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
We now (with 0.88.0) get:
File "bug.mlw", line 3, characters 13-23:
unbound symbol 'BV8.to_uint'
Also, now that I summoned the pros, would anyone know why I can't prove the
following lemmas?
theory Cvc4
use import mach.int.Int
use bv.BV8
use bv.BV64
use bv.BVConverter_8_64 as BVC
lemma bv8_to_bv64_low:
forall x i. 0 <= i < 8 -> BV64.nth (BVC.toBig x) i = BV8.nth x i
lemma bv8_to_bv64_high:
forall x i. 8 <= i < 64 -> BV64.nth (BVC.toBig x) i = false
end
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.
Thanks,
Julien
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
