Boogie:

* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).

Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.

1 files changed, 0 insertions, 72 deletions

diff --git a/Test/dafny0/Tree.dfy b/Test/dafny0/Tree.dfy
deleted file mode 100644
index 58124171..00000000
--- a/Test/dafny0/Tree.dfy
+++ /dev/null
@@ -1,72 +0,0 @@
-// ------------------ generic list, non-generic tree

-

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

-

-datatype Tree {

-  Node(int, List<Tree>);

-}

-

-static function Inc(t: Tree): Tree

-  decreases t;

-{

-  match t

-  case Node(n, children) => #Tree.Node(n+1, ForestInc(children))

-}

-

-static function ForestInc(forest: List<Tree>): List<Tree>

-  decreases forest;

-{

-  match forest

-  case Nil => forest

-  case Cons(tree, tail) => #List.Cons(Inc(tree), ForestInc(tail))

-}

-

-// ------------------ generic list, generic tree (but GInc defined only for GTree<int>

-

-datatype GTree<T> {

-  Node(T, List<GTree<T>>);

-}

-

-static function GInc(t: GTree<int>): GTree<int>

-  decreases t;

-{

-  match t

-  case Node(n, children) => #GTree.Node(n+1, GForestInc(children))

-}

-

-static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>

-  decreases forest;

-{

-  match forest

-  case Nil => forest

-  case Cons(tree, tail) => #List.Cons(GInc(tree), GForestInc(tail))

-}

-

-// ------------------ non-generic structures

-

-datatype TreeList {

-  Nil;

-  Cons(OneTree, TreeList);

-}

-

-datatype OneTree {

-  Node(int, TreeList);

-}

-

-static function XInc(t: OneTree): OneTree

-  decreases t;

-{

-  match t

-  case Node(n, children) => #OneTree.Node(n+1, XForestInc(children))

-}

-

-static function XForestInc(forest: TreeList): TreeList

-  decreases forest;

-{

-  match forest

-  case Nil => forest

-  case Cons(tree, tail) => #TreeList.Cons(XInc(tree), XForestInc(tail))

-}