Commits · 47a164276e08a0f4906b03acd24114a13e55209d · LARA / inox

May 26, 2015
- Fix soundness bug for smt-cvc4-cex/proof · 47a16427
  Manos Koukoutos authored 9 years ago
  
  47a16427
- out file in SMTLIBSolver can be a lazy Option · 89b437a7
  Manos Koukoutos authored 9 years ago
  
  89b437a7
- We don't need to duplicate FunDef's when generating VCs · a7ffa7c6
  Manos Koukoutos authored 9 years ago
  
  a7ffa7c6
- fix codegen evaluator for Modulo · 673f4fae
  Regis Blanc authored 9 years ago
  
  673f4fae
- unit testing default evaluator for division semantics · b9b1de59
  Regis Blanc authored 9 years ago
  
  b9b1de59
- xlang correctly handles short circuit with side effects · 2485477f
  Regis Blanc authored 9 years ago
  
  2485477f
- Print program after xlang transformation in debug · 32bdcd0a
  Regis Blanc authored 9 years ago
  
  32bdcd0a
- One line at most, 35 chars at most · dd789a3f
  Etienne Kneuss authored 9 years ago
  
  dd789a3f
May 22, 2015
- No need to change this · c5998b04
  Manos Koukoutos authored 9 years ago
  
  c5998b04
- Fix issue with extraction of case objects on top-level · 1298b62b
  Manos Koukoutos authored 9 years ago
  
  1298b62b
- Limit size of VC info in verif report · 06995588
  Etienne Kneuss authored 9 years ago
  
  06995588
- Better spec for find · c23d1da1
  Etienne Kneuss authored 9 years ago
  
  c23d1da1
- Fix repair script · 2939be54
  Etienne Kneuss authored 9 years ago
  
  2939be54
May 21, 2015
- HeapSort -> Heaps in repair testcases · a989d2cb
  Manos Koukoutos authored 9 years ago
  
  a989d2cb
- Crop preconditions when printing · 00b29af5
  Manos Koukoutos authored 9 years ago
  
  00b29af5
- Add lib files to watcher · 8a4501e3
  Manos Koukoutos authored 9 years ago
  
  8a4501e3
- Fix identation · 8a87ef1c
  Manos Koukoutos authored 9 years ago
  
  8a87ef1c
- Refactor boolean decorations, add ==> · 12116bae
  Manos Koukoutos authored 10 years ago
  
  12116bae
May 20, 2015
- math-like testcases · 3ad63474
  Regis Blanc authored 9 years ago
  
  3ad63474
- update readme with new structure of testcases · df0b3c86
  Regis Blanc authored 9 years ago
  
  df0b3c86
- some datastructure benchmark are actually algorithms · 8b01cfea
  Regis Blanc authored 9 years ago
  
  8b01cfea
- pldi2011 testcases moved to proper directory · 64c3a07c
  Regis Blanc authored 9 years ago
  
  64c3a07c
- compiler subtestcases · a0ac2ba6
  Regis Blanc authored 9 years ago
  
  a0ac2ba6
- reorgainze sas2011 benchmarks · b7dbed4d
  Regis Blanc authored 9 years ago
  
  b7dbed4d
- reorganize verification testcases · 1c8958e4
  Regis Blanc authored 9 years ago
  
  1c8958e4
- clean up more tests · e38c4579
  Regis Blanc authored 9 years ago
  
  e38c4579
- clean up some scala2013 testcases · 1b279a5d
  Regis Blanc authored 9 years ago
  
  1b279a5d
May 19, 2015
- clean up some redundant testcases · e586e6b6
  Regis Blanc authored 9 years ago
  
  e586e6b6
- correct implementation of div and mod in fairz3 · 36a4edc8
  Regis Blanc authored 9 years ago
  
  36a4edc8
- simpler encoding of division · b5f4f128
  Regis Blanc authored 9 years ago
  
  b5f4f128
- Add Implies to TransformerWithPC · b8f50cc5
  Manos Koukoutos authored 9 years ago
  
  b8f50cc5
- Simplify traverse a little · 7252b1a9
  Manos Koukoutos authored 9 years ago
  
  7252b1a9
- Remove unused annotations · 72b2374f
  Manos Koukoutos authored 9 years ago
  
  72b2374f
- List.apply should be Scala-executable. Fix leon.math not being @library · 549ec0e3
  Etienne Kneuss authored 9 years ago
  
  549ec0e3
May 18, 2015
- Mention compilation to bytecode · 7dd92914
  Etienne Kneuss authored 9 years ago
  
  7dd92914
- Fix compatibility with Scalac · bec7014b
  Etienne Kneuss authored 9 years ago
  
  bec7014b
May 13, 2015
- Out shouldn't be a var in SMTLIBSolver, and some aesthetics · 978a08ca
  Manos Koukoutos authored 9 years ago
  
  978a08ca
- Explicitly shutdown() solver factories when they are no longer used · 55da0652
  Etienne Kneuss authored 9 years ago
  
  Limitations: - Test suites about Fairz3 need full refactoring to shutdown - No shutdown in termination checkers for now.
  55da0652
- This benchmark actually needs a fix in non-smt solvers · d790e38a
  Etienne Kneuss authored 9 years ago
  
  d790e38a
- Fix VC numbering, options, and solver names. · 34123995
  Etienne Kneuss authored 9 years ago
  
  34123995