Commits · 3ff6d8bbb89bf9994fb3f67fd117467e5c0d26ff · LARA / inox

Jul 17, 2010
- re-configured sbt to use 2.8.0.final · 3ff6d8bb
  Philippe Suter authored 14 years ago
  
  3ff6d8bb
Jul 16, 2010
- foo · 32894a9e
  Viktor Kuncak authored 14 years ago
  
  32894a9e
- forgot to uncomment example · 1fc14043
  Viktor Kuncak authored 14 years ago
  
  1fc14043
- more examples and a bug · c2f832d1
  Viktor Kuncak authored 14 years ago
  
  c2f832d1
- munch demo · b4ad80f9
  Ruzica Piskac authored 14 years ago
  
  b4ad80f9
- added MUNCH files · bba45435
  Ruzica Piskac authored 14 years ago
  
  bba45435
Jul 13, 2010
- ExprCompr soundness · abe37834
  Viktor Kuncak authored 14 years ago
  
  abe37834
- added XP flag · 14a918e4
  Philippe Suter authored 14 years ago
  
  14a918e4
- fixed expr · 1f21b230
  Viktor Kuncak authored 14 years ago
  
  1f21b230
- corrected postcondition of isSorted · c6795423
  Swen Jacobs authored 14 years ago
  
  c6795423
- expr · 727b1065
  Viktor Kuncak authored 14 years ago
  
  727b1065
- added/uncommented postconditions in MergeSort.scala and QuickSort.scala,\n... · d6b502c5
  Swen Jacobs authored 14 years ago
  
  added/uncommented postconditions in MergeSort.scala and QuickSort.scala,\n added range restrictions as postcondition of isSorted in BinarySearchTree.scala
  d6b502c5
Jul 12, 2010
- -.- · b6ecd84a
  Robin Steiger authored 14 years ago
  
  b6ecd84a
- Sorry, I ran the wrong command. Still, one examples does not work... · 8842a679
  Robin Steiger authored 14 years ago
  
  8842a679
- has no effect · 9c076b11
  Philippe Suter authored 14 years ago
  
  9c076b11
- Regression tests, they were working at rev 1137 but they break now.. · 7ba98f5b
  Robin Steiger authored 14 years ago
  
  7ba98f5b
- removed debugging info · 0280a1ef
  Philippe Suter authored 14 years ago
  
  0280a1ef
- reverted Or generated in PM trans. · 220def15
  Philippe Suter authored 14 years ago
  
  220def15
- No commit message · 3356211a
  Philippe Suter authored 14 years ago
  
  No commit message
  3356211a
- added check for right order of lets. · 63ece372
  Philippe Suter authored 14 years ago
  
  63ece372
- BAPA (without Unifier) now relaxes the formula only until AFTER negation. · 1eb1c9ae
  Robin Steiger authored 14 years ago
  
  1eb1c9ae
- Fixed small compilation problem. · 02bc0066
  Robin Steiger authored 14 years ago
  
  02bc0066
- Inferred (dis)equalities on element variables and other changes. · d64511f2
  Robin Steiger authored 14 years ago
  
  d64511f2
- Two non-trivial bug fixes in pure scala (in pulloutAndKeepLets and inlineFunctionsAndContracts). · fdc3b193
  Robin Steiger authored 14 years ago
  
  InsertSort.sort can now be verified.
  fdc3b193
- Changelist: · 8679204a
  Utkarsh Upadhyay authored 14 years ago
  
  1. Added isUnsat to Extensions.scala 2. Added a few more conditions to BinarySearchTree.scala 3. Made calls to underlying solvers (involving double negation, etc) from the unifier 4. Fixed a minor bug in Expression Parsing in Main.scala
  8679204a
- Thanks to Swen's isSorted function, contains can be successfully verified. · 9ff7ddd1
  Utkarsh Upadhyay authored 14 years ago
  
  9ff7ddd1
- No commit message · af0a468d
  Philippe Suter authored 14 years ago
  
  No commit message
  af0a468d
- moved list of extensions to, well, Extensions · 9b9c91dc
  Philippe Suter authored 14 years ago
  
  9b9c91dc
- updated testcases · 287dc3d4
  Swen Jacobs authored 14 years ago
  
  287dc3d4
- one less bug · 019b1fad
  Philippe Suter authored 14 years ago
  
  019b1fad
- forgot the sources :D · fb3de75a
  Philippe Suter authored 14 years ago
  
  fb3de75a
- support for multisets extraction · 7e9ef789
  Philippe Suter authored 14 years ago
  
  7e9ef789
- added sortedness for insert in BinaryTree · 294b1b9f
  Swen Jacobs authored 14 years ago
  
  294b1b9f
- removed searchAndReplace as it has been copied to the funcheck library. · 0d28512e
  Robin Steiger authored 14 years ago
  
  0d28512e
Jul 11, 2010
- using axioms to unroll seems to work well with Z3 · 37531013
  Philippe Suter authored 14 years ago
  
  37531013
- summary · 5ac4a64b
  Philippe Suter authored 14 years ago
  
  5ac4a64b
- No commit message · 627ac060
  Philippe Suter authored 14 years ago
  
  No commit message
  627ac060
- now with NAryOperator extractor · c17a3ee1
  Philippe Suter authored 14 years ago
  
  c17a3ee1
- added trait Terminal to trees as suggested by Robin · 4d54f3bc
  Philippe Suter authored 14 years ago
  
  4d54f3bc
- Moved mkInfiniteTree example to demo file. · 6a0d337c
  Robin Steiger authored 14 years ago
  
  6a0d337c