Commits · a46a21c4c37ed3e6f662944e239ab60afde751ca · LARA / inox · GitLab

Snippets Groups Projects

May 02, 2016
- Disabled buffered log for NativeZ3 regression (tests are sequential · a46a21c4
  Nicolas Voirol authored 8 years ago
  
  anyway)
  a46a21c4
- Merge pull request #205 from MikaelMayer/master · df965290
  Mikaël Mayer authored 8 years ago
  
  Fixed ExprOps.isValue for covariant/contravariant function types.
  df965290
May 01, 2016
- Fixing a bug in smtlib encoding of adts · 7f1fa38e
  Ravi authored 8 years ago
  
  7f1fa38e
- Fixing a bug in the SMTLIB encoding of ADTs · 22075d6f
  Ravi authored 8 years ago
  
  22075d6f
- io directory for tests · 37bc9723
  Regis Blanc authored 8 years ago
  
  37bc9723
- 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