Skip to content
Snippets Groups Projects
  • Regis Blanc's avatar
    2bb7a742
    Int becomes bitvector · 2bb7a742
    Regis Blanc authored
    Leon now matches Scala semantics of Int as 32 bits bit-vectors.
    This commits modifies the semantics of IntLiteral to be treated
    as 32 bits integer everywhere (solver, evaluator, ...).
    
    Introduces a new literal type, InfiniteIntegerLiteral, representing
    a natural integer. The front-end maps the use of BigInt to these
    new trees, and the solver properly handles them as mathematical
    integers.
    
    The behaviour of many regression tests changes due to this new
    semantics. In particular many of them now timeout because they
    are no longer proving properties over mathematical integers. This
    commit updates the tests to reflect this new semantics.
    2bb7a742
    History
    Int becomes bitvector
    Regis Blanc authored
    Leon now matches Scala semantics of Int as 32 bits bit-vectors.
    This commits modifies the semantics of IntLiteral to be treated
    as 32 bits integer everywhere (solver, evaluator, ...).
    
    Introduces a new literal type, InfiniteIntegerLiteral, representing
    a natural integer. The front-end maps the use of BigInt to these
    new trees, and the solver properly handles them as mathematical
    integers.
    
    The behaviour of many regression tests changes due to this new
    semantics. In particular many of them now timeout because they
    are no longer proving properties over mathematical integers. This
    commit updates the tests to reflect this new semantics.