Skip to content
Snippets Groups Projects
  1. Apr 15, 2015
  2. Mar 26, 2015
  3. Mar 18, 2015
  4. Mar 06, 2015
  5. Feb 24, 2015
  6. Feb 17, 2015
    • Regis Blanc's avatar
      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
  7. Feb 12, 2015
Loading