• Sylvain Dailler's avatar
    Fixing bv theory after changes to theory bv.why. · 43657109
    Sylvain Dailler authored
    The former realization of bv used a bit of sign as the less significant
    bit which should be the most significant. It did not raise problems
    because to_int and to_uint were not linked by an axiom in the .why. Now,
    it is the case, so we rewrote function twos_complement and made some
    straightforward changes to the existing realization (surprisingly proofs
    are the same).
    43657109
Name
Last commit
Last update
..
bool Loading commit data...
bv Loading commit data...
floating_point Loading commit data...
ieee_float Loading commit data...
int Loading commit data...
list Loading commit data...
map Loading commit data...
number Loading commit data...
option Loading commit data...
real Loading commit data...
seq Loading commit data...
set Loading commit data...
.gitignore Loading commit data...
BuiltIn.v Loading commit data...
HighOrd.v Loading commit data...