Commits · 45496c70d7b90d4da5cda0aa21b862de01f4929a · LARA / inox · GitLab

Snippets Groups Projects

May 01, 2016
- Attempt at reducing native-z3 parallelism during tests · 45496c70
  Nicolas Voirol authored 8 years ago
  
  45496c70
- Fixed total model extraction in QuantificationManager · 87c04766
  Nicolas Voirol authored 8 years ago
  
  87c04766
- Moved InputCoverageSuite over to smt-z3 · f1e1bd36
  Nicolas Voirol authored 8 years ago
  
  f1e1bd36
- Added support to cover and, or. · 8a87948a
  Mikaël Mayer authored 8 years ago
  
  MatchExpr considered as IfExpr.
  8a87948a
- Better exception mechanism for Input coverage. · d0ff6838
  Mikaël Mayer authored 8 years ago
  
  d0ff6838
- Ignored flaky test · afbf74df
  Nicolas Voirol authored 8 years ago
  
  afbf74df
- Updated scalaz3-unix to latest · 4606c1a1
  Nicolas Voirol authored 8 years ago
  
  4606c1a1
- Documentation for path and evaluator · ee30114e
  Nicolas Voirol authored 8 years ago
  
  ee30114e
- synchronized evaluator invariant cache & small fix in codegen · 622632df
  Nicolas Voirol authored 8 years ago
  
  622632df
- Re-enabled AbstractEvaluator test and reset TerminationSuite to smt-z3 · e04ac67a
  Nicolas Voirol authored 8 years ago
  
  e04ac67a
- 1. Broader equivalence classes for lambdas · a73533f1
  Nicolas Voirol authored 8 years ago
  
  2. Evaluation of invariants caches result for valid forall-invariant interactions
  a73533f1
- Moved termination regression back to fairz3 · ab0fb4f5
  Nicolas Voirol authored 8 years ago
  
  ab0fb4f5
- Increased the timeout for InputCoverage to pass all the tests. · 15d5efb9
  Mikaël Mayer authored 8 years ago
  
  15d5efb9
- Leon now works again on Windows. · da6264d0
  Mikaël Mayer authored 8 years ago
  
  da6264d0
- Evaluates lambda applications by default. · 61804194
  Mikaël Mayer authored 8 years ago
  
  61804194
- Added varargs to methods in Leon + doc. · 13a5f4e4
  Mikaël Mayer authored 8 years ago
  
  13a5f4e4
- Now deterministic eval by default check if the model is ground, else evaluate it. · b4a11d0a
  Mikaël Mayer authored 8 years ago
  
  b4a11d0a
- Fixed the UnrollingSolver.scala evaluation. · 4882f9c7
  Mikaël Mayer authored 8 years ago
  
  4882f9c7
- removed printlns · 8631fadd
  Mikaël Mayer authored 8 years ago
  
  8631fadd
- Corrected typo in Focus.scala · fea65b24
  Mikaël Mayer authored 8 years ago
  
  Corrected bug in isValue Corrected evaluation in Evaluator (partition already evaluated)
  fea65b24
- Fixed the abstract evaluator suite. · afe9ddcb
  Mikaël Mayer authored 8 years ago
  
  afe9ddcb
- Temporarily disabled abstractevaluator test · df9e5f57
  Nicolas Voirol authored 8 years ago
  
  df9e5f57
- Latest scalaz3 again · d66b813a
  Nicolas Voirol authored 8 years ago
  
  d66b813a
- More structural size termination · bb580e51
  Nicolas Voirol authored 8 years ago
  
  bb580e51
- Small fix to termination checker for int32 termination · b293a63b
  Nicolas Voirol authored 8 years ago
  
  b293a63b
- Update to latest ScalaZ3 (with null model.eval checking) · 602569b4
  Nicolas Voirol authored 8 years ago
  
  602569b4
- Absolute value function for int32 types (termination) · bbbc470b
  Nicolas Voirol authored 8 years ago
  
  bbbc470b
- Small fix to termination checker for NoGuarantee cases · 064fa2a0
  Nicolas Voirol authored 8 years ago
  
  064fa2a0
- Fixed abstract evaluator & updated ScalaZ3 jar · 3dfd69be
  Nicolas Voirol authored 8 years ago
  
  3dfd69be
- Reduced the AbstractEvaluator's overhead by simplifying some expressions in the pattern matching. · d6837f0b
  Mikaël Mayer authored 8 years ago
  
  d6837f0b
- Fixed bug missing AsInstanceOf during AbstractEvaluator. · 6876a0df
  Mikaël Mayer authored 8 years ago
  
  6876a0df
- fix issue with nested functions updating mutable param · 2db018ed
  Regis Blanc authored 8 years ago
  
  2db018ed
- oups, should have been invalid · 9b3b6b39
  Regis Blanc authored 8 years ago
  
  9b3b6b39
- regression test for new extern behaviour · ac55292e
  Regis Blanc authored 8 years ago
  
  ac55292e
- println already defined somehow · 2454d614
  Regis Blanc authored 8 years ago
  
  2454d614
- working guess number example · 4c7edb7e
  Regis Blanc authored 8 years ago
  
  4c7edb7e
- extern never extracts the body · a5b1437b
  Regis Blanc authored 8 years ago
  
  a5b1437b
- while loops with distinguishable names · e301e6fa
  Regis Blanc authored 8 years ago
  
  e301e6fa
- Corrected 3 bugs in AbstractEvaluator.scala · 508c8049
  Mikaël Mayer authored 8 years ago
  
  * FunctionInvocation now considers abstract parameters * Applications on lambdas are now handled * Pattern matching now considers abstract parameters
  508c8049
- interactive leon program · 4039f20e
  Regis Blanc authored 8 years ago
  
  4039f20e