Commits · 549ec0e305ec6dc7ad8f6e17b062ac9f210a5ae0 · LARA / inox · GitLab

Snippets Groups Projects

May 19, 2015
- 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
May 12, 2015
- updated doc to remove the modulo limitation · 3d182d3d
  Viktor Kuncak authored 9 years ago
  
  3d182d3d
- correct BigInt division and remainder · 06ad7d4a
  Regis Blanc authored 9 years ago
  
  06ad7d4a
May 11, 2015
- New benchmarks with strings, justifications, etc.. · b0373d91
  Etienne Kneuss authored 9 years ago
  
  b0373d91
- No point in naming them Targets if they are Solvers. · 39403227
  Etienne Kneuss authored 9 years ago
  
  39403227
- Make sure we actually include NoXLangFeaturesChecking · 54515c0a
  Etienne Kneuss authored 9 years ago
  
  54515c0a
- Encode/Decode chars properly in SMT solvers · 30f322e6
  Etienne Kneuss authored 9 years ago
  
  30f322e6
- Some min/max functions in lib · 071f8c74
  Manos Koukoutos authored 9 years ago
  
  071f8c74
- If there is an error already, don't send commands · 4e9a690a
  Manos Koukoutos authored 9 years ago
  
  4e9a690a
- Fix identation · fbae1d2b
  Manos Koukoutos authored 9 years ago
  
  fbae1d2b
- Enrich/correct/make leon lib. compatible with Scala · f500a66b
  Manos Koukoutos authored 9 years ago
  
  f500a66b
- Some style · 961072ec
  Manos Koukoutos authored 9 years ago
  
  961072ec
- Fix TestCasesCompile package · 29e6b242
  Manos Koukoutos authored 9 years ago
  
  29e6b242
- foldr/ scanr signature consistent with Scala · 36241ec2
  Manos Koukoutos authored 9 years ago
  
  36241ec2
- MapUnion in SMTSolver (bad) · 383961f2
  Manos Koukoutos authored 9 years ago
  
  383961f2
- Catch some errors · 71e5bffc
  Manos Koukoutos authored 9 years ago
  
  71e5bffc
- Remove some code duplication · df563bc0
  Manos Koukoutos authored 9 years ago
  
  df563bc0
- TestCasesCompile should not be in LeonFunTests · 293b9f2c
  Manos Koukoutos authored 9 years ago
  
  293b9f2c
- Merge SMTLIBSolver with SMTLIBTarget · e3634bc8
  Manos Koukoutos authored 9 years ago
  
  e3634bc8
May 08, 2015
- testing bv division by zero with variables · e233402c
  Regis Blanc authored 9 years ago
  
  e233402c
May 07, 2015
- Explained how to build documentation using sphinx · 01d6d8d5
  Viktor Kuncak authored 9 years ago
  
  01d6d8d5
- Fix solver names for real this time · 8a8ec3ff
  Manos Koukoutos authored 9 years ago
  
  8a8ec3ff
- Improve unsupported handling in SMTLIB · 9f30d3ef
  Manos Koukoutos authored 9 years ago
  
  9f30d3ef
- Solver should not exit when encountering unsupported Tree · 4ae5ae4f
  Manos Koukoutos authored 9 years ago
  
  4ae5ae4f
- Correct name of smt-cvc4-proof · eac8e7f2
  Manos Koukoutos authored 9 years ago
  
  eac8e7f2
May 06, 2015
- Instantiate types in method calls as well · ffec223e
  Etienne Kneuss authored 9 years ago
  
  instantiateType needs to apply on MethodInvocation as well since it is used before MethodLifing
  ffec223e
- Fallback to whatever is available, fatal otherwise. · 2ff6b9b5
  Etienne Kneuss authored 9 years ago
  
  2ff6b9b5
- Allow functions returning Unit in codegen evaluator · 82e318bf
  Etienne Kneuss authored 9 years ago
  
  82e318bf
- Update readme with new preconditions · c191f46c
  Etienne Kneuss authored 9 years ago
  
  c191f46c
- generate vc for division by zero · 7d353945
  Regis Blanc authored 9 years ago
  
  7d353945
- Precise description of preconditions · a1f0bcda
  Etienne Kneuss authored 9 years ago
  
  a1f0bcda
- Too many successes on this one · 9661794c
  Etienne Kneuss authored 9 years ago
  
  9661794c
- Set/Map should be cases classes so that equality is consistent · 2316cb90
  Etienne Kneuss authored 9 years ago
  
  2316cb90
- Print types in pretty printer when asked to · c8997c5b
  Etienne Kneuss authored 9 years ago
  
  c8997c5b