Commits · 619a6424e1c48f7191112b40a22962dc8a835ed9 · LARA / inox · GitLab

Snippets Groups Projects

May 29, 2015
- Update to latest scala-smtlib · 619a6424
  Manos Koukoutos authored 9 years ago
  
  619a6424
- re-introduce loop invariants positions · f7d54929
  Regis Blanc authored 9 years ago
  
  f7d54929
- fix while loop with complicated conditions · 7a512513
  Regis Blanc authored 9 years ago
  
  7a512513
- Restore tests for new solvers · 46cf4bc6
  Manos Koukoutos authored 9 years ago
  
  46cf4bc6
- doc: cross references in intro, for impatient. Typo fixed. · dec6efbc
  Viktor Kuncak authored 9 years ago
  
  dec6efbc
- Let's not discriminate against these two good integers · f7c8ffaa
  Etienne Kneuss authored 9 years ago
  
  f7c8ffaa
- Fixed code gen evaluator for lambdas · ff4fd365
  Nicolas Voirol authored 9 years ago
  
  ff4fd365
- Fixed some stuff up in termination · 76626ed9
  Nicolas Voirol authored 9 years ago
  
  76626ed9
May 27, 2015
- Matching on BigInts · ed7e2c05
  Etienne Kneuss authored 9 years ago
  
  ed7e2c05
- Maps/Sets have explicit types, remove Empty/NonemptySet/Map · 73ca139b
  Etienne Kneuss authored 9 years ago
  
  73ca139b
- Free the solver we get when checking if we are in SMT-quantified · 867e7f53
  Etienne Kneuss authored 9 years ago
  
  867e7f53
- Evaluator option --eval takes evaluator as argument · 4150a2a9
  Etienne Kneuss authored 9 years ago
  
  4150a2a9
- Fix · 773edd8e
  Etienne Kneuss authored 9 years ago
  
  773edd8e
- Strenghten List.find · 67bc0996
  Etienne Kneuss authored 9 years ago
  
  67bc0996
- Fix info being too large in precondition. · a05c87e5
  Etienne Kneuss authored 9 years ago
  
  a05c87e5
May 26, 2015
- Failed compilation during tests should spawn failing test · 08f4f6ba
  Manos Koukoutos authored 9 years ago
  
  08f4f6ba
- Kick the new z3 solver out of tests for now · a6566fa7
  Manos Koukoutos authored 9 years ago
  
  a6566fa7
- Change how postcond. are encoded in GroupedTactic · b3157364
  Manos Koukoutos authored 9 years ago
  
  b3157364
- Improvements in smtlib solvers · 0666b058
  Manos Koukoutos authored 9 years ago
  
  0666b058
- Portfolio should implement assertVC · 73ce19e6
  Manos Koukoutos authored 9 years ago
  
  73ce19e6
- Improve/add/correct testcases for new solvers · ee367ec7
  Manos Koukoutos authored 9 years ago
  
  ee367ec7
- Check unknown vcs before invalid · 7c4d4cf2
  Manos Koukoutos authored 9 years ago
  
  7c4d4cf2
- Don't crash if a test folder is missing · de35fc53
  Manos Koukoutos authored 9 years ago
  
  de35fc53
- Give 0 rather than -0 to solver · fcac8a89
  Manos Koukoutos authored 9 years ago
  
  fcac8a89
- 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