Commits · 29d0c69f3926258971aee1a3ef3345bf93bbff4a · LARA / inox

Feb 01, 2011
- the demos · 3bc05f77
  Philippe Suter authored 14 years ago
  
  3bc05f77
Jan 25, 2011
- Required modifications to testcases for submission · ed3bd975
  Ali Sinan Köksal authored 14 years ago
  
  ed3bd975
Jan 21, 2011
- why CAV cannot find counterexample · 3cd0ea59
  Viktor Kuncak authored 14 years ago
  
  3cd0ea59
Jan 12, 2011
- laid the groundwork for new instantiator · be10ccd3
  Philippe Suter authored 14 years ago
  
  be10ccd3
Nov 25, 2010
- examples · e814ee48
  Ali Sinan Köksal authored 14 years ago
  
  e814ee48
Nov 19, 2010
- modification to some examples · 93593073
  Ali Sinan Köksal authored 14 years ago
  
  93593073
- Size equivalence, concat and reverse proofs in ListWithSize · c5f704eb
  Ali Sinan Köksal authored 14 years ago
  
  c5f704eb
- Some modification to examples and some evaluation summary · f7d66ba4
  Ali Sinan Köksal authored 14 years ago
  
  f7d66ba4
Nov 18, 2010
- inductive proof for size of append. · 5fb6c7d6
  Ali Sinan Köksal authored 14 years ago
  
  5fb6c7d6
- Inductive tactic performs induction on first argument with abstract type.... · c8bd0066
  Ali Sinan Köksal authored 14 years ago
  c8bd0066
- An implementation of InductionTactic and its example use in ListWithSize · 4cc65ae3
  Ali Sinan Köksal authored 14 years ago
  
  4cc65ae3
Nov 16, 2010
- apparently induction works if we refer to the boolean value of recursive... · 9eefa5c6
  Viktor Kuncak authored 14 years ago
  9eefa5c6
- nilAppend works · 053d9f0b
  Viktor Kuncak authored 14 years ago
  
  053d9f0b
Oct 25, 2010
- minor · 37a24609
  Viktor Kuncak authored 14 years ago
  
  37a24609
- drunk function in lists example set · cc6344e8
  Viktor Kuncak authored 14 years ago
  
  cc6344e8
- redblack with size · b95e12e9
  Viktor Kuncak authored 14 years ago
  
  b95e12e9
Oct 14, 2010
- --newPM still crashes for some examples. Getting there, though :( · ecf009f8
  Philippe Suter authored 14 years ago
  
  ecf009f8
Oct 07, 2010
- more new better · 1508a8e5
  Philippe Suter authored 14 years ago
  
  1508a8e5
- playing with induction · 2f1d9ea4
  Viktor Kuncak authored 14 years ago
  
  2f1d9ea4
Aug 16, 2010
- more examples in here · f7399f63
  Philippe Suter authored 14 years ago
  
  f7399f63
Jul 11, 2010
- using axioms to unroll seems to work well with Z3 · 37531013
  Philippe Suter authored 14 years ago
  
  37531013
Jul 09, 2010
- there was actually a bug in Z3Solver too. Works now ! · dd284219
  Philippe Suter authored 15 years ago
  
  dd284219
Jul 08, 2010
- the bug wrt. to unrolling is in the Lets!!! let me fix it once I've slept. · 5307ed36
  Philippe Suter authored 15 years ago
  
  5307ed36