diff --git a/testcases/NonDeterministicList.scala b/testcases/NonDeterministicList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c766956ed6a862108190880c553ebfd915133184
--- /dev/null
+++ b/testcases/NonDeterministicList.scala
@@ -0,0 +1,53 @@
+import leon.Utils._
+
+object NonDeterminism {
+
+  abstract class IntList
+  case class Cons(h: Int, tail: IntList) extends IntList
+  case class Nil() extends IntList
+
+  def insert(l: IntList, el: Int): IntList = Cons(el, l)
+  def remove(l: IntList, el: Int): IntList = l match {
+    case Cons(x, xs) => 
+      if(x < el) Cons(x, remove(xs, x)) 
+      else if(x == el) remove(xs, x) 
+      else  xs
+    case Nil() => Nil()
+  }
+
+  def content(l: IntList) : Set[Int] = l match {
+    case Nil() => Set.empty[Int]
+    case Cons(x, xs) => Set(x) ++ content(xs)
+  }
+
+  def nonDeterministicExecution(): Boolean = {
+
+    var list: IntList = Cons(42, Nil())
+    var error: Boolean = false
+
+    val b1 = epsilon((x: Boolean) => true)
+    val n1 = epsilon((x: Int) => true)
+    if(b1)
+      list = insert(list, n1)
+    else {
+      list = remove(list, n1)
+      if(content(list).contains(n1)) {
+        error = true
+      }
+    }
+
+    val b2 = epsilon((x: Boolean) => true)
+    val n2 = epsilon((x: Int) => true)
+    if(b2)
+      list = insert(list, n2)
+    else {
+      list = remove(list, n2)
+      if(content(list).contains(n2)) {
+        error = true
+      }
+    }
+
+    !error
+  } holds
+
+}
diff --git a/testcases/SecondsToTime.scala b/testcases/SecondsToTime.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6969991c2aa40aa1b6d28c6bc73bf898d2a04fe0
--- /dev/null
+++ b/testcases/SecondsToTime.scala
@@ -0,0 +1,39 @@
+
+object SecondsToTime {
+
+  def propSum(t: Int, h: Int, m: Int, s: Int) : Boolean = h * 3600 + m * 60 + s == t
+  def prop(t: Int, h: Int, m: Int, s: Int) : Boolean = propSum(t, h, m, s) && m >= 0 && m < 60 && s >= 0 && s < 60 
+
+  def secondsToTime(total : Int) = {
+    require(total >= 0)
+      rec(total, total, 0, 0)
+  } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) }) 
+
+  def secondsToTime2(total : Int) = {
+    require(total >= 0)
+      rec2(total, total, 0, 0)
+  } ensuring(_ match { case (h,m,s) => prop(total, h, m, s) }) 
+
+  def rec(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+    require(propSum(total, h, m, r) && m >= 0 && h >= 0 && r >= 0 && m < 60 && (m == 0 || r + m * 60 < 3600))
+
+    if(r >= 3600) {
+      rec(total, r - 3600, h + 1, m)
+    } else if(r >= 60) {
+      rec(total, r - 60, h, m + 1)
+    } else {
+      (h, m, r)
+    }
+  } ensuring(_ match { case(h,m,s) => prop(total, h, m, s) }) 
+
+  def rec2(total : Int, r : Int, h : Int, m : Int) : (Int, Int, Int) = {
+    require(propSum(total, h, m, r) && m >= 0 && h >= 0 && r >= 0 && m < 60)
+    if(r >= 60 && m == 59) {
+      rec2(total, r - 60, h + 1, 0)
+    } else if(r >= 60) {
+      rec2(total, r - 60, h, m + 1)
+    } else {
+      (h, m, r)
+    }
+  } ensuring(_ match { case(h,m,s) => prop(total, h, m, s) }) 
+}
diff --git a/testcases/graph/MST/MSTMap.scala b/testcases/graph/MST/MSTMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..71e894754638fc5a3c44162e2be8ba87e17ca510
--- /dev/null
+++ b/testcases/graph/MST/MSTMap.scala
@@ -0,0 +1,273 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+object MSTMap {
+
+  case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
+
+  /*
+   -----------------------------------------------------------------------------
+   MST TESTS Map
+   -----------------------------------------------------------------------------
+   */
+
+  // Kruskal's algorithm. Straightforward imperative implementation
+  def mst(g : Graph) : Map[(Int,Int), Int] = {
+    require(invariant(g) && isUndirected(g) && isConnected(g) &&
+  g.nVertices <= 3)
+    
+    var uf_map = Map.empty[Int, Int] //map to represent parent
+    //relationship to model union find
+
+    var spanningTree = Map.empty[(Int,Int), Int]
+    var alreadyTested = Map.empty[(Int, Int), Int]
+    
+    (while(!isConnected(spanningTree, g.nVertices)) {
+      val next_edge = getSmallestEdge(g.nVertices, g.edges, alreadyTested)
+      
+      val p1 = uFind(next_edge._1, uf_map)
+      val p2 = uFind(next_edge._2, uf_map)
+      if(p1  != p2) {
+	// Edge doesn't create a cycle -> add it to the current
+	// spanning tree (or actually forest)
+	spanningTree = spanningTree.updated((next_edge._1, next_edge._2), next_edge._3)
+	spanningTree = spanningTree.updated((next_edge._2, next_edge._1), next_edge._3)
+	uf_map = union(p1, p2, uf_map)
+      }
+
+      alreadyTested = alreadyTested.updated((next_edge._1, next_edge._2), 1)
+      alreadyTested = alreadyTested.updated((next_edge._2,
+					     next_edge._1), 1)
+    }) invariant(isAcyclic(spanningTree, g.nVertices))
+
+    spanningTree
+  } ensuring(x => isAcyclic(x, g.nVertices) && isConnected(x, g.nVertices))
+  // We only verify that the edge set returned corresponds to some
+  // spanning tree, but not that it is of minimal weight.
+
+  
+  // Here, we always take the smallest edge regardless whether it
+  // creates a cycle or not,
+  // Leon loops
+  def mstBogus(g : Graph) : Map[(Int,Int), Int] = {
+    require(invariant(g) && isUndirected(g) && isConnected(g) &&
+  g.nVertices <= 4)
+    
+    var edges = g.edges
+    var spanningTree = Map.empty[(Int,Int), Int]
+    var alreadyTested = Map.empty[(Int, Int), Int]
+    
+    (while(!isConnected(spanningTree, g.nVertices)) {
+      val next_edge = getSmallestEdge(g.nVertices, edges, alreadyTested)
+
+      // add edge to spanning tree, don't care whether it creates a
+      // cycle or not
+      spanningTree = spanningTree.updated((next_edge._1, next_edge._2), next_edge._3)
+      spanningTree = spanningTree.updated((next_edge._2, next_edge._1), next_edge._3)
+
+      alreadyTested = alreadyTested.updated((next_edge._1, next_edge._2), 1)
+      alreadyTested = alreadyTested.updated((next_edge._2,
+					     next_edge._1), 1)
+    }) invariant(isAcyclic(spanningTree, g.nVertices))
+
+    spanningTree
+  } ensuring(x => isAcyclic(x, g.nVertices) && isConnected(x, g.nVertices))
+
+  
+  /*
+   -----------------------------------------------------------------------------
+   GRAPH FUNCTIONS
+   -----------------------------------------------------------------------------
+   */
+  
+
+  def invariant(g : Graph) = {
+    def noSelfLoops(i : Int) : Boolean = {
+      if(i >= g.nVertices) true
+      else if(g.edges.isDefinedAt(i,i))
+	false
+      else
+	noSelfLoops(i+1)
+    }
+    
+    g.nVertices >= 0 && noSelfLoops(0)
+  }
+  
+  /**
+   Tests, if g is undirected, that is if for every edge (i,j) there is
+   also and edge (j,i)
+   Ignoring weights for the moment
+   */
+  def isUndirected(g: Graph) : Boolean = {
+    require(invariant(g))
+
+    val edgeSet = g.edges
+    var res = true
+    var i = 0
+    while(i < g.nVertices && res) {
+      var j = 0
+      while(j < g.nVertices && res) {
+	res = !edgeSet.isDefinedAt(i,j) || edgeSet.isDefinedAt(j,i)
+	
+	 //If weights should considered
+	 if(res && edgeSet.isDefinedAt(i,j))
+	   res = edgeSet(i,j) == edgeSet(j,i)
+	   
+	j += 1
+      }
+      i += 1
+    }
+
+    res
+  }
+
+  /*
+   * Returns the smallest edge in "edges" but not in "forbidden"
+   * Returns (-1,-1,-1) if there are no more edges.
+   */
+  def getSmallestEdge(nVertices : Int, edges : Map[(Int,Int), Int],
+		      forbidden : Map[(Int,Int), Int]) : (Int, Int, Int)
+  = {
+    require (nVertices >= 0)
+
+    /*
+     In the very specific context of MST, it could be useful to
+     somehow express that "edges"\"forbidden" is non-empty such that
+     it this function would always return a valid edge, however, this
+     property is not easily expressible in Leon.
+     */
+    
+    var i = 0
+    val big = 100000000
+    var res = (-1,-1,big)
+      
+      while(i < nVertices) {
+	var j = 0
+	while(j < nVertices) {
+	  // leon doesnt recognize "shortcut optimizations", e.g. if
+          // both if statements were merged to one using &&, it finds
+          // a counter example
+	  if(edges.isDefinedAt(i,j) && !forbidden.isDefinedAt(i,j)) {
+	    if(edges(i,j) < res._3)
+	      res = (i,j, edges(i,j))
+	  }
+	  j += 1
+	}
+	i += 1
+      }
+
+    if(res == (-1,-1,big))
+      (-1,-1,-1)
+    else
+      res
+  }
+
+  def isSpanningTree(g : Graph) : Boolean = {
+    require(invariant(g) && isUndirected(g))
+    isConnected(g) && isAcyclic(g.edges, g.nVertices)
+  }
+
+   def isConnected(g : Graph) :  Boolean = {
+     require(g.nVertices >= 0 && isUndirected(g))
+     isConnected(g.edges, g.nVertices)
+   }
+  
+  def isConnected(edges : Map[(Int,Int), Int], nVertices : Int) :  Boolean = {
+    require(nVertices >= 0)
+    val uf = calculateUF(edges, nVertices)._1
+
+    val p = uFind(0, uf)
+    var i = 1
+
+    var ret = true
+    while(i < nVertices && ret) {
+      if(uFind(i, uf) != p)
+	ret = false    // 0, i are not connected
+      i += 1
+    }
+
+    ret
+  }
+
+  /*
+   * Tests, whether the subgraph induced by edges is cycle-free.
+   */
+  def isAcyclic(edges : Map[(Int,Int), Int], nVertices : Int) : Boolean = {
+    require(nVertices >= 0 && isUndirected(Graph(nVertices, edges)))
+    !calculateUF(edges, nVertices)._2
+  }
+
+  /*
+   * Does union-find on edgeSet.
+   * Returns the union-find tree and a boolean set to true if a cycle was found
+   */
+  def calculateUF(edgeSet : Map[(Int,Int), Int], nVertices : Int) :
+  (Map[Int, Int], Boolean)= {
+    require(nVertices >= 0)
+    
+    var i = 0
+    var uf = Map.empty[Int, Int]
+    var cycle = false
+    var edges = edgeSet
+    while(i < nVertices) {
+      var j = 0
+      while(j < nVertices) {
+	if(edges.isDefinedAt((i,j))) {
+	  if(edges(i, j) != -1) {
+	    val p1 = uFind(i, uf)
+	    val p2 = uFind(j, uf)
+	    if(p1 == p2)
+	      cycle = true
+	    else
+	      uf = union(p1, p2, uf)
+
+	    //"remove" twin edge
+	    edges = edges.updated((j,i), -1)
+	  }	   
+	}
+	j += 1
+      }
+      i += 1
+    }
+
+    (uf, cycle)
+  }
+  
+  /* *************************************
+   Union find
+   *************************************** */
+  def uFind(e : Int, s : Map[Int, Int]) : Int = {
+    if(!s.isDefinedAt(e)) e
+    else if(s(e) == e) e
+    else uFind(s(e), s)
+  }
+
+  def union(e1 : Int, e2 : Int, s : Map[Int,Int]) : Map[Int, Int] = {
+    // naive union
+    val p1 = uFind(e1,s)
+    val p2 = uFind(e2, s)
+    
+    if(p1 != p2)
+      //naive union
+      s.updated(p1, p2) //only union if theiy are really in different trees
+    else
+      s
+  }
+
+
+  // fsc -d classes -classpath
+  // ../../leon-2.0/target/scala-2.9.1-1/classes MST.scala
+  //   scala -classpath classes MST  
+  def main(args: Array[String]) {
+    val edges = Map((1,0) -> 10, (0,1) -> 10, (1,2) -> 12, (2,1) ->
+  12, (0,2) -> 18, (2,0) -> 18, (3,1) -> 20, (1,3) -> 20)
+
+    val g = Graph(4, edges)
+
+    println(mst(g)); //works
+    println(mstBogus(g)); // crashes because postcondition doensn't hold
+  }
+  
+}
diff --git a/testcases/graph/MST/SpanningTree.scala b/testcases/graph/MST/SpanningTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..862842e08f180736e9f8ffd7f2caa7d62113ae09
--- /dev/null
+++ b/testcases/graph/MST/SpanningTree.scala
@@ -0,0 +1,208 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+object SpanningTree {
+  case class Graph(nVertices : Int, edges : Set[(Int,Int)])
+
+  // Kruskal on unweighted graphs (thus not spanning tree of minimum weight)
+  def getSpanningTree(g : Graph) : Set[(Int, Int)] = {
+    require(invariant(g) && isUndirected(g) && isConnected(g.edges,
+							   g.nVertices) && g.nVertices <= 3)
+
+    var uf_map = Map.empty[Int, Int] //map to represent parent
+    //relationship to model union find
+    
+    var spanningSet = Set.empty[(Int,Int)]
+    var remainingEdges = g.edges
+    
+    (while(!isConnected(spanningSet, g.nVertices)) {
+      val next_edge = epsilon( (i : (Int, Int)) =>
+	remainingEdges.contains(i) )
+
+      val p1 = uFind(next_edge._1, uf_map)
+      val p2 = uFind(next_edge._2, uf_map)
+      if(p1  != p2) {
+	spanningSet = spanningSet ++ Set(next_edge) ++
+	Set((next_edge._2, next_edge._1))
+
+	uf_map = union(p1, p2, uf_map)
+      }
+      
+      remainingEdges = remainingEdges -- Set(next_edge) -- Set((next_edge._2, next_edge._1))
+
+    }) invariant(isAcyclic(spanningSet, g.nVertices))
+
+    spanningSet
+  } ensuring(x => isAcyclic(x, g.nVertices))
+  
+  def getSpanningTreeBogus(g : Graph) : Set[(Int, Int)] = {
+    require(invariant(g) && isUndirected(g) && isConnected(g.edges,
+				       		   g.nVertices) && g.nVertices <= 4)
+
+    var spanningSet = Set.empty[(Int,Int)]
+    var remainingEdges = g.edges
+    
+    (while(!isConnected(spanningSet, g.nVertices)) {
+      val next_edge = epsilon( (i : (Int, Int)) => remainingEdges.contains(i) )
+      remainingEdges = remainingEdges -- Set(next_edge) -- Set((next_edge._2, next_edge._1))
+
+      spanningSet = spanningSet ++ Set(next_edge) ++ Set((next_edge._2, next_edge._1))
+    }) invariant(isAcyclic(spanningSet, g.nVertices))
+
+    spanningSet
+  } ensuring(x => isAcyclic(x, g.nVertices))
+
+  
+  def invariant(g : Graph) = {
+    def noSelfLoops(i : Int) : Boolean = {
+      if(i >= g.nVertices) true
+      else if(g.edges.contains(i,i))
+	false
+      else
+	noSelfLoops(i+1)
+    }
+    
+    g.nVertices >= 0 // && noSelfLoops(0)
+  }
+
+  /*
+   Smarter version of doing it?
+   */
+  def isUndirected(g : Graph) : Boolean = {
+    def isUndirected0(s : Set[(Int, Int)]) : Boolean= {
+      if(s == Set.empty[(Int,Int)]) true
+      else {
+	val e = epsilon( (p : (Int,Int)) => s.contains(p) )
+	if(g.edges.contains(e))
+	  isUndirected0(s -- Set(e))
+	else
+	  false
+      }
+    }
+
+    isUndirected0(g.edges)
+  }
+
+  /*
+   * Tests, whether the subgraph induced by edges is cycle-free.
+   */
+  def isAcyclic(edges : Set[(Int,Int)], nVertices : Int) : Boolean = {
+    require(nVertices >= 0 && isUndirected(Graph(nVertices, edges)))
+    !calculateUF(edges, nVertices)._2
+  }
+  
+  /*
+   * Does union-find on edgeSet.
+   * Returns the union-find tree and a boolean set to true if a cycle was found
+   */
+  def calculateUF(edgeSet : Set[(Int,Int)], nVertices : Int) :
+  (Map[Int, Int], Boolean)= {
+    require(nVertices >= 0)
+    
+    var i = 0
+    var uf = Map.empty[Int, Int]
+    var cycle = false
+    var edges = edgeSet
+    while(i < nVertices) {
+      var j = 0
+      while(j < i) {
+	if(edges.contains((i,j))) {
+	    val p1 = uFind(i, uf)
+	    val p2 = uFind(j, uf)
+	    if(p1 == p2)
+	      cycle = true
+	    else
+	      uf = union(p1, p2, uf)
+	}
+      
+	j += 1
+      }
+      i += 1
+    }
+
+    (uf, cycle)
+  }
+
+  def isConnected(edges : Set[(Int,Int)], nVertices : Int) :  Boolean
+  = {
+    require(nVertices >= 0)
+    val uf = calculateUF(edges, nVertices)._1
+
+    val p = uFind(0, uf)
+    var i = 1
+
+    var ret = true
+    while(i < nVertices && ret) {
+      if(uFind(i, uf) != p)
+	ret = false    // 0, i are not connected
+      i += 1
+    }
+
+    ret
+  }
+
+  /*
+   * Does union-find on edgeSet.
+   * Returns the union-find tree and a boolean set to true if a cycle was found
+   */
+  def calculateUF(edgeSet : Map[(Int,Int), Int], nVertices : Int) :
+  (Map[Int, Int], Boolean)= {
+    require(nVertices >= 0)
+    
+    var i = 0
+    var uf = Map.empty[Int, Int]
+    var cycle = false
+    var edges = edgeSet
+    while(i < nVertices) {
+      var j = 0
+      while(j < nVertices) {
+	if(edges.isDefinedAt((i,j))) {
+	  if(edges(i, j) != -1) {
+	    val p1 = uFind(i, uf)
+	    val p2 = uFind(j, uf)
+	    if(p1 == p2)
+	      cycle = true
+	    else
+	      uf = union(p1, p2, uf)
+
+	    //"remove" twin edge
+	    edges = edges.updated((j,i), -1)
+	  }	   
+	}
+	j += 1
+      }
+      i += 1
+    }
+
+    (uf, cycle)
+  }
+
+  /* *************************************
+   Union find
+   *************************************** */
+  def uFind(e : Int, s : Map[Int, Int]) : Int = {
+    if(!s.isDefinedAt(e)) e
+    else if(s(e) == e) e
+    else uFind(s(e), s)
+  }
+
+  def union(e1 : Int, e2 : Int, s : Map[Int,Int]) : Map[Int, Int] = {
+    // naive union
+    val p1 = uFind(e1,s)
+    val p2 = uFind(e2, s)
+    
+    if(p1 != p2)
+      //naive union
+      s.updated(p1, p2) //only union if theiy are really in different trees
+    else
+      s
+  }
+
+  def testUndirected() : Boolean = {
+    val e = Set.empty[(Int, Int)] ++ Set((1,2)) ++ Set((2,1)) ++ Set((1,3))
+    isUndirected(Graph(4, e))
+  } holds
+  
+}
diff --git a/testcases/graph/SetIteration.scala b/testcases/graph/SetIteration.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8730d4abcd727a469eb7ec6384c82637127db43e
--- /dev/null
+++ b/testcases/graph/SetIteration.scala
@@ -0,0 +1,78 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+/** Examples of iteration over set elements using 'epsilon'.
+ *
+ * First we implement a test for containment. This can easily be verified
+ * correct by Leon — because the post-condition can be specified concisely in
+ * concepts Leon understands.
+ * 
+ * Next we implement a test for wether all values are at least some minimum,
+ * and try to prove that (∀x. x≥5) → (∀x. x≥2). Leon fails to prove this,
+ * despite proving an equivalent formulation using linked lists instead of sets
+ * (SimpleInduction.scala).
+ * 
+ * Finally, we implement a method to find the cardinality of a set. Leon can
+ * prove things with this on concrete sets, as seen in sizeTest1(), but not on
+ * arbitrary sets, as in sizeTest2().
+ */
+object SetIteration {
+  def iterateContains(set: Set[Int], v : Int) : Boolean ={
+    if (set == Set.empty[Int])
+      false
+    else {
+      val elt = epsilon( (i : Int) => set.contains(i) )
+      if (elt==v)
+        true
+      else
+        iterateContains(set -- Set(elt), v)
+    }
+  } ensuring (_ == set.contains(v))
+  
+  def contTest(set : Set[Int], v : Int) : Boolean = {
+    set.contains(v) == iterateContains(set, v)
+  } holds
+  
+  
+  def iterateMinVal(set: Set[Int], v : Int) : Boolean ={
+    if (set == Set.empty[Int])
+      true
+    else {
+      val elt = epsilon( (i : Int) => set.contains(i) )
+      if (elt >= v)
+        iterateMinVal(set -- Set(elt), v)
+      else
+        false
+    }
+  }
+  
+  def sizeMinVal(set : Set[Int]) : Boolean = {
+    !iterateMinVal(set, 5) || iterateMinVal(set, 2)
+  } holds       // proof fails
+  
+  
+  def iterateSize(set: Set[Int]) : Int ={
+    if (set == Set.empty[Int])
+      0
+    else {
+      val elt = epsilon( (i : Int) => set.contains(i) )
+      1 + iterateSize(set -- Set(elt))
+    }
+  }ensuring (_ >= 0)
+  
+  def sizeTest1() : Boolean = {
+    iterateSize(Set.empty)+3 == iterateSize(Set(4,8,22))
+  } holds
+  def sizeTestFalse(set : Set[Int]) : Boolean = {
+    val size1 = iterateSize(set)
+    val size2 = iterateSize(set ++ Set(32))
+    size1+1 == size2
+  } holds       // gives correct counter example: set=Set(32)
+  def sizeTest2(set : Set[Int]) : Boolean = {
+    val size1 = iterateSize(set)
+    val size2 = iterateSize(set ++ Set(32))
+    size1+1 == size2 || size1 == size2
+  } holds       // proof fails
+}
diff --git a/testcases/graph/SimpleInduction.scala b/testcases/graph/SimpleInduction.scala
new file mode 100644
index 0000000000000000000000000000000000000000..50f9109797c1ce3e9c733605f01eb7aa19df4993
--- /dev/null
+++ b/testcases/graph/SimpleInduction.scala
@@ -0,0 +1,49 @@
+import leon.Utils._
+import leon.Annotations._
+
+/** A simple example of inductive proofs.
+ * 
+ * These require use of the @induct attribute. See SetIteration.scala for a
+ * conceptually similar example where Leon cannot use inductive reasoning.
+ */
+object SimpleInduction {
+  // a simple linked list
+  abstract class SimpleList
+  case class SimpleItem(v : Int, next : SimpleList) extends SimpleList
+  case class SimpleEnd() extends SimpleList
+  
+  // true if all elements have value at least x
+  def eltsAtLeast(list : SimpleList, x : Int) : Boolean =
+    list match {
+      case SimpleItem(v, next) => v >= x && eltsAtLeast(next, x)
+      case SimpleEnd() => true
+    }
+  
+  @induct
+  def simpleProposition(list : SimpleList) : Boolean = {
+    !eltsAtLeast(list, 5) || eltsAtLeast(list, 2)
+  } holds
+  
+  @induct
+  def noAction(list : SimpleList) : SimpleList = {
+    require(eltsAtLeast(list, 5))
+    list
+  } ensuring (eltsAtLeast(list, 2))
+  
+  
+  // A more explicit version of the above to more clearly illustrate where
+  // inductive reasoning is required.
+  
+  // try to prove that x≥a → x≥b for each element
+  def inductiveStep(list : SimpleList, a : Int, b : Int) : Boolean =
+    list match {
+      case SimpleItem(v, next) => (!(v >= a) || v >= b) && inductiveStep(next, a, b)
+      case SimpleEnd() => true
+    }
+  
+  // another encoding of simpleProposition
+  @induct
+  def inductiveProof(list : SimpleList) : Boolean = {
+    inductiveStep(list, 5, 2)
+  } holds
+}
diff --git a/testcases/graph/SortedNDList.scala b/testcases/graph/SortedNDList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f7bef6ff38048f6c2d63b4f406c0b0effed39d93
--- /dev/null
+++ b/testcases/graph/SortedNDList.scala
@@ -0,0 +1,105 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+/** Tests for SortedNDList
+ */
+object SortedNDList {
+  /** A list containing node, dist pairs.
+   *
+   * Sorted by distance, nearest first. Distance must be non-negative. Node
+   * values must be unique and non-negative.
+   */
+  abstract class SortedNDList
+  case class ListNode(val node : Int, val dist : Int, var next : SortedNDList) extends SortedNDList
+  case class ListEnd() extends SortedNDList
+  
+  /** List invariant (see description above) */
+  @induct
+  def sndInvariant(list : SortedNDList) : Boolean = {
+    // Most conditions are commented out. Leon cannot even check adding or
+    // removing an element satisfies the invariant in this case!
+    def invRec(list : SortedNDList/*, elts : Set[Int], minDist : Int, len : Int*/) : Boolean =
+      list match {
+        case ListNode(n,d,next) =>
+          if (d >= 0/*minDist*/ && n >= 0 /*&& !elts.contains(n)*/)
+            invRec(next/*,elts++Set(n),d, len + 1*/)
+          else
+            false
+        case ListEnd() => true //len <= 3
+      }
+    
+    invRec(list/*, Set.empty, 0, 0*/)
+  }
+  
+  /** Simple test function: does adding an element at the start of the list
+   * maintain the invariant? */
+  @induct def addStart(list : SortedNDList, node:Int, dist:Int) : SortedNDList ={
+    require (sndInvariant(list) && node>=0 && dist>=0)
+    ListNode(node,dist,list)
+  } ensuring(sndInvariant(_))   // Leon cannot verify this even when all the invariant does is check that node and dist are non-negative!
+  
+  /* Further tests fail, if run.
+  
+  /** Look for node in list and remove, if it exists. */
+  @induct
+  def removeFromList(list : SortedNDList, node : Int) : SortedNDList ={
+    // something about this times out
+    require(sndInvariant(list))
+    
+    //println("removeFromList: "+list)
+    
+    list match  {
+      case ListNode(n,d,next) =>
+        if (n == node)
+          // drop current node and continue search:
+          removeFromList(next, node)
+        else
+          ListNode(n,d,removeFromList(next, node))
+      case ListEnd() => list
+    }
+  } ensuring(sndInvariant(_))   // something about this generates an error: is the precondition not checked for _all_ elements or something?
+  
+  /** Return true if list contains node */
+  @induct
+  def listContains(list : SortedNDList, node : Int) : Boolean ={
+    // something to do with this times out
+    require(sndInvariant(list))
+    list match {
+      case ListNode(n,d,next) =>
+        if (node == n) true
+        else listContains(next, node)
+      case ListEnd() => false
+    }
+  }
+  
+  /** Add a new node to the list, such that list remains sorted by distance.
+   * Assume node is not already in list. */
+  @induct
+  def addSorted(list : SortedNDList, node : Int, dist : Int) : SortedNDList = {
+    // something to do with this times out
+    require(sndInvariant(list) && !listContains(list, node) && node >= 0 && dist >= 0)
+    
+    list match {
+      case ListNode(n,d,next) =>
+        if (d > dist)        // insert here
+          ListNode(node, dist, list)
+        else
+          ListNode(n,d, addSorted(next, node, dist))
+      case ListEnd() => // insert at end
+        ListNode(node, dist, list)
+    }
+  } ensuring (sndInvariant(_))  // something to do with this times out
+  
+  /** Update node with distance minimum of dist and current value. Add if not
+   * in list, and maintain sorted order. */
+  @induct
+  def updateDistInList(list : SortedNDList, node : Int, dist : Int) : SortedNDList = {
+    require(sndInvariant(list) && node >= 0 && dist >= 0)
+    
+    val listRemoved = removeFromList(list, node)
+    addSorted(listRemoved, node, dist)
+  } ensuring(sndInvariant(_))
+  */
+}
diff --git a/testcases/graph/Subgraph.scala b/testcases/graph/Subgraph.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d7f245da07cc7683c861f900434bffd1f1c6193d
--- /dev/null
+++ b/testcases/graph/Subgraph.scala
@@ -0,0 +1,268 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+object Subgraph {
+  /** Graph representation.
+   *
+   * A graph has vertices 0, 1, ..., nVertices-1.
+   *
+   * Vertices is a singly linked list with length nVertices, corresponding in
+   * order to the vertices 0, 1, ..., nVertices.
+   * 
+   * Each vertex has a list of edges, representing edges from that vertex to
+   * the edge's toVertex field. This must not include the vertex itself. The
+   * representation is for directed graphs.
+   * 
+   * Example:
+   *
+   * Graph(3,
+   *   VertexItem(
+   *     VertexItem(
+   *       VertexItem(VertexEnd(),
+   *         EdgeItem(EdgeItem(EdgeEnd(), 1), 0)),
+   *       EdgeEnd()),
+   *     EdgeItem(EdgeEnd(), 2))
+   * )
+   *
+   * represents a graph with vertices 0, 1 and 2 with edges (2,0), (2,1) and (0,2).
+   */
+  case class Graph(nVertices : Int, vertices : Vertices)
+  sealed abstract class Vertices
+  case class VertexItem(next : Vertices, edges : Edges) extends Vertices
+  case class VertexEnd() extends Vertices
+  sealed abstract class Edges
+  case class EdgeItem(next : Edges, toVertex : Int, weight : Int) extends Edges
+  case class EdgeEnd() extends Edges
+
+  /*
+   -----------------------------------------------------------------------------
+   SUBGRAPH TESTS
+   -----------------------------------------------------------------------------
+   */
+
+  /*
+   Empty graph is a subgraph of any other graph
+   Works.
+   */  
+  def emptyGraph(g : Graph) : Boolean = {
+    require(invariant(g))
+    val empty = Graph(0, VertexEnd())
+    isSubGraph(empty, g)
+  } holds
+
+  /*
+   Graph with a single vertex is a subgraph of any other graph
+   Finds counter example (empty graph) quickly
+   */
+  def singleGraphSubsetOfAnotherGraph(g : Graph) : Boolean = {
+    require(invariant(g))
+    val single = Graph(1, VertexItem(VertexEnd(), EdgeEnd()))
+    isSubGraph(single, g)
+  } holds
+
+  /*
+  // Leon times out
+  def subGraphIsReflexive(g : Graph) : Boolean = {
+    require(invariant(g) && g.nVertices <= 3)
+    isSubGraph(g,g)
+  } holds
+  */
+
+  /*
+  // Leon times out
+   def isSubGraphIsAntiSymmetric(g1 : Graph, g2 : Graph) : Boolean = {
+    require(invariant(g1) && invariant(g2)) // && g1.nVertices <= 3 && g2.nVertices <= 3)
+    !(isSubGraph(g1, g2) && isSubGraph(g2, g1)) || (g1 == g2)
+  } holds
+  */
+  
+  /*
+   isSubGraphBogus does not check that g1 has equal or fewer
+   vertices than g2 (i.e. that the vertex set of g1 is a subset of
+   those of g2)
+   
+   Finds counter example often quickly, but needs sometimes more than 30s
+   */
+  def subGraphIsAntiSymmetricBogus(g1 : Graph, g2 : Graph) : Boolean = {
+    require(invariant(g1) && invariant(g2))
+    !(isSubGraphBogus(g1, g2) && isSubGraphBogus(g2, g1)) || (g1 == g2)
+  } holds
+   
+  /*
+   isSubGraphBogus2: The weights are ignored
+   
+   Leon times out.
+   */
+  /*
+   def subGraphIsAntiSymmetricBogus2(g1 : Graph, g2 : Graph) : Boolean = {
+   require(invariant(g1) && invariant(g2)) // && g1.nVertices <= 3 && g2.nVertices <= 3)
+   !(isSubGraphBogus2(g1, g2) && isSubGraphBogus2(g2, g1)) || (g1 == g2)
+   } holds
+  */
+
+  /*
+   -----------------------------------------------------------------------------
+   GRAPH FUNCTIONS
+   -----------------------------------------------------------------------------
+   */
+  
+  /* Helper function (for conditions). */
+  def lenVertexList(vertices : Vertices) : Int = vertices match {
+    case VertexEnd() => 0
+    case VertexItem(next, _) => 1+lenVertexList(next)
+  }
+
+  /* * Return true if and only if the graph representation is valid.
+   *
+   * Checks:
+   *  nVertices >= 0
+   *  length of vertex list is nVertices,
+   *  there is no edge from a vertex to itself (no self-loops),
+   *  there is not more than one edge from any vertex to any other,
+   *  there are no edges to invalid vertices.
+   * */
+   def invariant(g : Graph) : Boolean = {
+   
+   // Leon bug(?): cannot access g.nVertices from within this function:
+     def recEdges(edge : Edges, alreadyFound : Set[Int]) : Boolean = edge match {
+       case EdgeEnd() => true
+       case EdgeItem(next, toVertex, w) =>{
+	 0 <= toVertex && toVertex < g.nVertices &&
+	 !alreadyFound.contains(toVertex) &&
+	 recEdges(next, alreadyFound++Set(toVertex))
+       }
+     }
+     
+     def recVertices(i : Int, vertex : Vertices) : Boolean = vertex match {
+       case VertexEnd() =>
+	 i == g.nVertices      // list should only be null if length is correct
+       case VertexItem(next,edges) =>
+	 if (i >= g.nVertices)
+           false
+	 else
+           recEdges(edges, Set(i)) && recVertices(i+1, next)
+     }
+     
+     g.nVertices >= 0 && recVertices(0, g.vertices)
+   }
+
+  
+  /*
+   * Returns the edges of a graph as a map 
+   */
+  def getEdges(g : Graph) : Map[(Int, Int), Int] = {
+    require(invariant(g))
+    
+    def recEdges(from : Int, edge : Edges, acc : Map[(Int,Int), Int]) : Map[(Int, Int), Int] = edge match {
+      case EdgeEnd() => acc
+      case EdgeItem(next,toVertex,w) =>
+	recEdges(from, next, acc.updated((from,toVertex), w))
+    }
+    
+    def recVertices(i : Int, vertex : Vertices, acc : Map[(Int,Int), Int])
+    : Map[(Int, Int), Int] = vertex match {
+      case VertexEnd() =>  acc
+      case VertexItem(next,edges) => {
+	val a = recEdges(i, edges, acc)
+	recVertices(i + 1, next, a)
+      }
+    }
+
+    recVertices(0, g.vertices, Map.empty[(Int,Int), Int])
+  }
+
+  /*
+   * Tests if g1 is a subgraph of g2.
+   * We iterate over all edges in g1 and test if they also exist in g2
+   */
+  def isSubGraph(g1 : Graph, g2 : Graph) : Boolean = {
+    require(invariant(g1) && invariant(g2))
+
+    val edges2 = getEdges(g2)
+
+    def recEdges(from : Int, edge : Edges, acc : Boolean) : Boolean = {
+      if(!acc) false //fail fast
+      else {
+	edge match {
+	  case EdgeEnd() => acc
+	  case EdgeItem(next,toVertex,w) => {
+	    if(edges2.isDefinedAt(from, toVertex)) {
+	      if(edges2(from, toVertex) != w)
+		false
+	      else
+		acc
+	    }
+	      else false
+	  }
+	}
+      }
+    }
+    
+    def recVertices(i : Int, vertex : Vertices, acc : Boolean) : Boolean = vertex match {
+      case VertexEnd () => acc
+      case VertexItem(next,edges) => {
+	val b  = recEdges(i, edges, acc)
+	recVertices(i + 1, next, b)
+      }
+    }
+
+    if(g1.nVertices > g2.nVertices) // Vertex set needs to be a subset
+      false
+    else
+      recVertices(0, g1.vertices, true)
+  }
+
+  /*
+   Tests if g1 is a subgraph of g2.
+   Bogus version 1: number of vertices needs to be taken in account
+   */
+  def isSubGraphBogus(g1 : Graph, g2 : Graph) : Boolean = {
+    require(invariant(g1) && invariant(g2))
+
+    val edges2 = getEdges(g2)
+
+    def recEdges(from : Int, edge : Edges, acc : Boolean) : Boolean = edge match {
+      case EdgeEnd() => acc
+      case EdgeItem(next,toVertex,_) => acc && edges2.isDefinedAt(from, toVertex)
+    }
+    
+    def recVertices(i : Int, vertex : Vertices, acc : Boolean) : Boolean = vertex match {
+      case VertexEnd () => acc
+      case VertexItem(next,edges) => {
+	val b  = recEdges(i, edges, acc)
+	recVertices(i + 1, next, b)
+      }
+    }
+
+    recVertices(0, g1.vertices, true)
+  }
+
+  /*
+   Bogus version 2: weights of edges also need to be considered
+   */
+  def isSubGraphBogus2(g1 : Graph, g2 : Graph) : Boolean = {
+    require(invariant(g1) && invariant(g2))
+
+    val edges2 = getEdges(g2)
+
+    def recEdges(from : Int, edge : Edges, acc : Boolean) : Boolean = edge match {
+      case EdgeEnd() => acc
+      case EdgeItem(next,toVertex,_) => acc && edges2.isDefinedAt(from, toVertex)
+    }
+    
+    def recVertices(i : Int, vertex : Vertices, acc : Boolean) : Boolean = vertex match {
+      case VertexEnd () => acc
+      case VertexItem(next,edges) => {
+	val b  = recEdges(i, edges, acc)
+	recVertices(i + 1, next, b)
+      }
+    }
+
+    if(g1.nVertices > g2.nVertices) // Vertex set needs to be a subset
+      false
+    else
+      recVertices(0, g1.vertices, true)
+  }
+}
diff --git a/testcases/graph/SubgraphMap.scala b/testcases/graph/SubgraphMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..15029853287f495c1a175ed71b65610e9a83f990
--- /dev/null
+++ b/testcases/graph/SubgraphMap.scala
@@ -0,0 +1,104 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+object SubgraphSet {
+  case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
+  
+  /*
+   -----------------------------------------------------------------------------
+   SUBGRAPH TESTS
+   -----------------------------------------------------------------------------
+   */
+
+  /*
+   Empty graph is a subgraph of any other graph
+   Works.
+   */
+  def empty(g : Graph) : Boolean = {
+    require(invariant(g))
+    val empty = Graph(0, Map.empty[(Int, Int), Int])
+    isSubGraph(empty, g)
+  } holds
+
+  /*
+   Graph with a single vertex is a subgraph of any other graph
+   Finds counter example (empty graph) quickly
+   */
+  def singleGraphSubsetOfAnotherGraph(g : Graph) : Boolean = {
+    require(invariant(g))
+    val single = Graph(1, Map.empty[(Int, Int), Int])
+    isSubGraph(single, g)
+  } holds
+
+  // Leon proves it quickly
+  def subGraphIsReflexive(g : Graph) : Boolean = {
+    require(invariant(g) && g.nVertices <=3)
+    isSubGraph(g,g)
+  } holds
+  
+  // Leon proves it within a few seconds (bounds!)
+  def isSubGraphIsAntiSymmetric(g1 : Graph, g2 : Graph) : Boolean = {
+    require(invariant(g1) && invariant(g2) && g1.nVertices <= 5 && g2.nVertices <= 5)
+    !(isSubGraph(g1, g2) && isSubGraph(g2, g1)) || isEqual(g1, g2)
+  } holds
+
+  // Leon proves it within reasonable times (bounds!)
+  def equalsIsSymmetric(g1 : Graph, g2 : Graph) : Boolean = {
+    require(invariant(g1) && invariant(g2) && g1.nVertices <= 5 && g2.nVertices <= 5)
+    isEqual(g1,g2) == isEqual(g2, g1)
+  } holds
+
+  
+  /*
+   -----------------------------------------------------------------------------
+   GRAPH FUNCTIONS
+   -----------------------------------------------------------------------------
+   */
+
+    // This rather weak invariant is good enough for our purposes here
+  def invariant(g : Graph) = g.nVertices >= 0
+  
+  def isSubGraph(x : Graph, y : Graph) : Boolean = {
+    require(invariant(x) && invariant(y))
+    
+    var ret : Boolean = (x.nVertices <= y.nVertices)
+      if (ret){
+	var i = 0
+	while(i<x.nVertices) {
+          var j = 0;
+          while(j < x.nVertices) {
+            ret &&= !x.edges.isDefinedAt((i,j)) || y.edges.isDefinedAt((i,j))
+
+	    if(x.edges.isDefinedAt((i,j)) && y.edges.isDefinedAt((i,j)))
+	      ret &&= (x.edges(i,j) == y.edges(i,j))
+		
+		j += 1
+          }
+          i += 1
+	}
+      }
+    ret
+  }
+
+  def isEqual(x : Graph, y : Graph) : Boolean = {
+    var ret = (x.nVertices == y.nVertices)
+      var i = 0
+    while(i<x.nVertices && ret) {
+      var j = 0
+      while(j < y.nVertices && ret) {
+	
+        ret &&= (!x.edges.isDefinedAt((i,j)) ||
+		 y.edges.isDefinedAt((i,j))) && (!y.edges.isDefinedAt((i,j)) ||
+						 x.edges.isDefinedAt((i,j)))
+	if(x.edges.isDefinedAt((i,j)) && y.edges.isDefinedAt((i,j))) 
+	  ret &&= (x.edges(i,j) == y.edges(i,j))
+	    j += 1
+	
+      }
+      i += 1
+    }
+    ret   
+  }  
+}
diff --git a/testcases/graph/TreeEquivalence.scala b/testcases/graph/TreeEquivalence.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ea1be52ef5581cfa91a7381a844da83f3c4cbe3e
--- /dev/null
+++ b/testcases/graph/TreeEquivalence.scala
@@ -0,0 +1,291 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+object TreeEquivalence {
+  /** Graph representation.
+   *
+   * A graph has vertices 0, 1, ..., nVertices-1.
+   *
+   * Vertices is a singly linked list with length nVertices, corresponding in
+   * order to the vertices 0, 1, ..., nVertices.
+   * 
+   * Each vertex has a list of edges, representing edges from that vertex to
+   * the edge's toVertex field. This must not include the vertex itself. The
+   * representation is for directed graphs.
+   * 
+   * Example:
+   *
+   * Graph(3,
+   *   VertexItem(
+   *     VertexItem(
+   *       VertexItem(VertexEnd(),
+   *         EdgeItem(EdgeItem(EdgeEnd(), 1), 0)),
+   *       EdgeEnd()),
+   *     EdgeItem(EdgeEnd(), 2))
+   * )
+   *
+   * represents a graph with vertices 0, 1 and 2 with edges (2,0), (2,1) and (0,2).
+   */
+  case class Graph(nVertices : Int, vertices : Vertices)
+  sealed abstract class Vertices
+  case class VertexItem(next : Vertices, edges : Edges) extends Vertices
+  case class VertexEnd() extends Vertices
+  sealed abstract class Edges
+  case class EdgeItem(next : Edges, toVertex : Int, weight : Int) extends Edges
+  case class EdgeEnd() extends Edges
+
+
+  /*
+   -----------------------------------------------------------------------------
+   TREE EQUIVALENCE TESTS
+   -----------------------------------------------------------------------------
+   */
+
+  
+  /*
+   Try to prove that a spanning tree has (g.nVertices - 1) edges
+   This is true for undirected graphs, but here we don't enforce the
+   condition.
+   
+   Finds a counter-example sometimes after quite some time.
+   */
+  /*
+  def treeEquivalence(g:Graph) : Boolean = {
+    require(invariant(g) && isConnected(g) && g.nVertices > 0 && g.nVertices <=3)
+    (!isSpanningTree(g) || ((getNumberOfEdges(g) == g.nVertices - 1)))
+  } holds
+  */
+  
+  
+  /*
+   Try to prove that every connected graph has (g.nVertices - 1) edges
+   
+   Finds counter example quickly (empty graph). No options
+   */
+  def connectedGraph(g:Graph) : Boolean = {
+    require(invariant(g) && isConnected(g))
+    (getNumberOfEdges(g) == g.nVertices - 1)
+  } holds
+
+
+  /*
+   * - Trying to prove that every connected, non-empty graph has
+   (g.nVertices - 1) edges
+   * - Since we left out some isUndirected condtion it finds a counter example
+   *   sometimes (depends on the upper bound of
+   *   g.nVertices, the larger the more time it needs to find a
+   *   counter example)
+   */
+  def nonEmptyConnectedGraph(g:Graph) : Boolean = {
+    require(invariant(g) && isConnected(g) && g.nVertices > 0 &&
+	    g.nVertices < 4)
+    (getNumberOfEdges(g) == g.nVertices - 1)
+  } holds
+
+  
+  /*
+   -----------------------------------------------------------------------------
+   GRAPH FUNCTIONS
+   -----------------------------------------------------------------------------
+   */
+  
+  /* Helper function (for conditions). */
+  def lenVertexList(vertices : Vertices) : Int = vertices match {
+    case VertexEnd() => 0
+    case VertexItem(next, _) => 1+lenVertexList(next)
+  }
+
+  /* * Return true if and only if the graph representation is valid.
+   *
+   * Checks:
+   *  nVertices >= 0
+   *  length of vertex list is nVertices,
+   *  there is no edge from a vertex to itself (no self-loops),
+   *  there is not more than one edge from any vertex to any other,
+   *  there are no edges to invalid vertices.
+   * */
+  def invariant(g : Graph) : Boolean = {
+    
+    def recEdges(edge : Edges, alreadyFound : Set[Int]) : Boolean = edge match {
+      case EdgeEnd() => true
+      case EdgeItem(next, toVertex, w) =>{
+	0 <= toVertex && toVertex < g.nVertices &&
+	!alreadyFound.contains(toVertex) &&
+	recEdges(next, alreadyFound++Set(toVertex))
+      }
+    }
+    
+    def recVertices(i : Int, vertex : Vertices) : Boolean = vertex match {
+      case VertexEnd() =>
+	i == g.nVertices      // list should only be null if length is correct
+      case VertexItem(next,edges) =>
+	if (i >= g.nVertices)
+          false
+	else
+          recEdges(edges, Set(i)) && recVertices(i+1, next)
+    }
+    
+    g.nVertices >= 0 && recVertices(0, g.vertices)
+  }
+
+  
+  /*
+   * Returns the edges of a graph as a map 
+   */
+  def getEdges(g : Graph) : Map[(Int, Int), Int] = {
+    require(invariant(g))
+    
+    def recEdges(from : Int, edge : Edges, acc : Map[(Int,Int), Int]) : Map[(Int, Int), Int] = edge match {
+      case EdgeEnd() => acc
+      case EdgeItem(next,toVertex,w) =>
+	recEdges(from, next, acc.updated((from,toVertex), w))
+    }
+    
+    def recVertices(i : Int, vertex : Vertices, acc : Map[(Int,Int), Int])
+    : Map[(Int, Int), Int] = vertex match {
+      case VertexEnd() =>  acc
+      case VertexItem(next,edges) => {
+	val a = recEdges(i, edges, acc)
+	recVertices(i + 1, next, a)
+      }
+    }
+
+    recVertices(0, g.vertices, Map.empty[(Int,Int), Int])
+  }
+
+  /*
+   Counts the number of edges in a graph
+   */
+  def getNumberOfEdges(g : Graph) : Int = {
+    require(invariant(g))
+
+    def recEdges(from : Int, edge : Edges, acc : Int) : Int = edge
+    match {
+      case EdgeEnd() => acc
+      case EdgeItem(next,toVertex,_) => recEdges(from, next, acc + 1)
+    }
+    
+    def recVertices(i : Int, vertex : Vertices, acc : Int)
+    : Int = vertex match {
+      case VertexEnd () => acc
+      case VertexItem(next,edges) => {
+	val e = recEdges(i, edges, acc)
+	recVertices(i + 1, next, e)
+      }
+    }
+
+    recVertices(0, g.vertices, 0)
+  }
+
+
+  /*
+   * Tests whether a given edge set forms a spanning tree using
+   union - find
+   */
+  def isSpanningTree(g : Graph) : Boolean = {
+    require(invariant(g))
+    isConnected(g) && isAcyclic(g)
+  }
+
+  def isConnected(g : Graph) : Boolean = {
+    require(invariant(g))
+    isConnected(getEdges(g), g.nVertices)
+  }
+
+  def isConnected(edges : Map[(Int,Int), Int], nVertices : Int) :
+  Boolean = {
+    require(nVertices >= 0)
+    val uf = calculateUF(edges, nVertices)._1
+
+    val p = uFind(0, uf)
+    var i = 1
+
+    var ret = true
+    while(i < nVertices && ret) {
+      if(uFind(i, uf) != p)
+	ret = false    // 0, i are not connected
+      i += 1
+    }
+
+    ret
+  }
+
+  /*
+   * Tests, whether g is cycle-free
+   */
+  def isAcyclic(g : Graph) : Boolean = {
+    require(invariant(g))
+    !calculateUF(getEdges(g),g.nVertices)._2
+  }
+
+  /*
+   * Tests, whether the subgraph induced by edges is cycle-free.
+   * If directed==true, the edge set is interpreted as directed edges
+   * i.e. a->b and b->a are considered as two distinct edges.
+   */
+  def isAcyclic(edges : Map[(Int,Int), Int], nVertices : Int) : Boolean = {
+    require(nVertices >= 0)
+    !calculateUF(edges, nVertices)._2
+  }
+
+
+  /*
+   * Does union-find on edgeSet.
+   * Returns the union-find tree and a boolean set to true if a cycle was found
+   */
+  def calculateUF(edgeSet : Map[(Int,Int), Int], nVertices : Int) :
+  (Map[Int, Int], Boolean)= {
+    require(nVertices >= 0)
+    
+    var i = 0
+    var uf = Map.empty[Int, Int]
+    var cycle = false
+    var edges = edgeSet
+    while(i < nVertices) {
+      var j = 0
+      while(j < nVertices) {
+	if(edges.isDefinedAt((i,j))) {
+	  if(edges(i, j) != -1) {
+	    val p1 = uFind(i, uf)
+	    val p2 = uFind(j, uf)
+	    if(p1 == p2)
+	      cycle = true
+	    else
+	      uf = union(p1, p2, uf)
+
+	    //"remove" twin edge
+	    edges = edges.updated((j,i), -1)
+	  }	   
+	}
+	j += 1
+      }
+      i += 1
+    }
+
+    (uf, cycle)
+  }
+  
+
+  /* *************************************
+   Union find
+   *************************************** */
+  def uFind(e : Int, s : Map[Int, Int]) : Int = {
+    if(!s.isDefinedAt(e)) e
+    else if(s(e) == e) e
+    else uFind(s(e), s)
+  }
+
+  def union(e1 : Int, e2 : Int, s : Map[Int,Int]) : Map[Int, Int] = {
+    // naive union
+    val p1 = uFind(e1,s)
+    val p2 = uFind(e2, s)
+    
+    if(p1 != p2)
+      //naive union
+      s.updated(p1, p2) //only union if theiy are really in different trees
+    else
+      s
+  }
+}
diff --git a/testcases/graph/TreeEquivalenceMap.scala b/testcases/graph/TreeEquivalenceMap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..599557f7f11abde533dcb99f0b6ffe8168b4bb71
--- /dev/null
+++ b/testcases/graph/TreeEquivalenceMap.scala
@@ -0,0 +1,208 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+object TreeEquivalenceSet {
+  /*
+   -----------------------------------------------------------------------------
+   TREE EQUIVALENCE TESTS ON SET REPRESENTATION
+   -----------------------------------------------------------------------------
+   */
+  
+  /*
+   Try to prove that a spanning tree has (g.nVertices - 1) edges
+   
+   Leon loops
+   */
+  /*
+  def treeEquivalence(g:Graph) : Boolean = {
+    require(invariant(g) && isUndirected(g) && g.nVertices > 0 && g.nVertices <= 3)
+    (!isSpanningTree(g) || ((getNumberOfEdges(g) == g.nVertices - 1)))
+  } holds
+  */
+  
+  /*
+   Try to prove that every connected graph has (g.nVertices - 1) edges
+   
+   Finds counter example with out of range edges (--noLuckyTests)
+   */
+  def connectedGraph(g:Graph) : Boolean = {
+    require(invariant(g) && isConnected(g) && isUndirected(g))
+    (getNumberOfEdges(g) == g.nVertices - 1)
+  } holds
+
+  
+  /*
+   Trying to prove that every connected, non-empty graph has (g.nVertices - 1) edges
+   
+   Leon loops
+   */
+  /*
+  def nonEmptyConnectedGraph(g:Graph) : Boolean = {
+    require(invariant(g) && isConnected(g) && isUndirected(g) && g.nVertices > 0 &&
+	    g.nVertices <= 3)
+    (getNumberOfEdges(g) == g.nVertices - 1)
+  } holds
+  */
+  
+  /*
+   -----------------------------------------------------------------------------
+   GRAPH FUNCTIONS
+   -----------------------------------------------------------------------------
+   */
+
+  case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
+
+  def invariant(g : Graph) = {
+    def noSelfLoops(i : Int) : Boolean = {
+      if(i >= g.nVertices) true
+      else if(g.edges.isDefinedAt(i,i))
+	false
+      else
+	noSelfLoops(i+1)
+    }
+    
+    g.nVertices >= 0 && noSelfLoops(0)
+  }
+
+  /**
+   Tests, if g is undirected, that is if for every edge (i,j) there is
+   also and edge (j,i)
+   Ignoring weights for the moment
+   */
+
+  def isUndirected(g: Graph) : Boolean = {
+    require(invariant(g))
+
+    val edgeSet = g.edges
+    var res = true
+    var i = 0
+    while(i < g.nVertices && res) {
+      var j = 0
+      while(j < g.nVertices && res) {
+	res = !edgeSet.isDefinedAt(i,j) || edgeSet.isDefinedAt(j,i)
+	
+	//If weights should considered
+	if(res && edgeSet.isDefinedAt(i,j))
+	  res = edgeSet(i,j) == edgeSet(j,i)
+	
+	j += 1
+      }
+      i += 1
+    }
+
+    res
+  }
+  
+  /*
+   Leon doesn't support size operators, so we need to count edges explicitely...
+   
+   Note that the upper bound on x can not be proven using this graph
+   representation since leon will then pick some out of range edges
+   */
+  def getNumberOfEdges(g : Graph) : Int = {
+    require(invariant(g))
+
+    var i = 0
+    var cnt = 0
+    (while(i < g.nVertices) {
+      var j = 0
+      (while(j < g.nVertices) {
+	if(g.edges.isDefinedAt(i,j))
+	  cnt += 1
+	j += 1
+      }) invariant(cnt >= 0) //&& cnt <= g.nVertices * g.nVertices)
+      i += 1
+    }) invariant(cnt >= 0)  //&& cnt  <= g.nVertices * g.nVertices)
+
+    cnt
+  } ensuring(x => x >= 0) //&& x  <= g.nVertices * g.nVertices)
+  
+  def isSpanningTree(g : Graph) : Boolean = {
+    require(invariant(g) && isUndirected(g))
+    isConnected(g) && isAcyclic(g.edges, g.nVertices)
+  }
+
+  def isConnected(g : Graph) :  Boolean = {
+    require(g.nVertices >= 0 && isUndirected(g))
+    val uf = calculateUF(g.edges, g.nVertices)._1
+
+    val p = uFind(0, uf)
+    var i = 1
+
+    var ret = true
+    while(i < g.nVertices && ret) {
+      if(uFind(i, uf) != p)
+	ret = false    // 0, i are not connected
+      i += 1
+    }
+
+    ret
+  }
+
+  /*
+   * Tests, whether the subgraph induced by edges is cycle-free.
+   */
+  def isAcyclic(edges : Map[(Int,Int), Int], nVertices : Int) : Boolean = {
+    require(nVertices >= 0 && isUndirected(Graph(nVertices, edges)))
+    !calculateUF(edges, nVertices)._2
+  }
+
+  /*
+   * Does union-find on edgeSet.
+   * Returns the union-find tree and a boolean set to true if a cycle was found
+   */
+  def calculateUF(edgeSet : Map[(Int,Int), Int], nVertices : Int) :
+  (Map[Int, Int], Boolean)= {
+    require(nVertices >= 0)
+    
+    var i = 0
+    var uf = Map.empty[Int, Int]
+    var cycle = false
+    var edges = edgeSet
+    while(i < nVertices) {
+      var j = 0
+      while(j < nVertices) {
+	if(edges.isDefinedAt((i,j))) {
+	  if(edges(i, j) != -1) {
+	    val p1 = uFind(i, uf)
+	    val p2 = uFind(j, uf)
+	    if(p1 == p2)
+	      cycle = true
+	    else
+	      uf = union(p1, p2, uf)
+
+	    //"remove" twin edge
+	    edges = edges.updated((j,i), -1)
+	  }	   
+	}
+	j += 1
+      }
+      i += 1
+    }
+
+    (uf, cycle)
+  }
+
+  /* *************************************
+   Union find
+   *************************************** */
+  def uFind(e : Int, s : Map[Int, Int]) : Int = {
+    if(!s.isDefinedAt(e)) e
+    else if(s(e) == e) e
+    else uFind(s(e), s)
+  }
+
+  def union(e1 : Int, e2 : Int, s : Map[Int,Int]) : Map[Int, Int] = {
+    // naive union
+    val p1 = uFind(e1,s)
+    val p2 = uFind(e2, s)
+    
+    if(p1 != p2)
+      //naive union
+      s.updated(p1, p2) //only union if theiy are really in different trees
+    else
+      s
+  }
+}
diff --git a/testcases/graph/dijkstras/DijkstrasSet.scala b/testcases/graph/dijkstras/DijkstrasSet.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f914864627909f182cfe06d5733ddd62af7a7f48
--- /dev/null
+++ b/testcases/graph/dijkstras/DijkstrasSet.scala
@@ -0,0 +1,154 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+/** Implementation of Dijkstra's algorithm. Iterates over vertex IDs, looking
+ * distances up in a map, to find the nearest unvisited node.
+ */
+object DijkstrasSet {
+  /***************************************************************************
+   * Graph representation and algorithms
+   **************************************************************************/
+  case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
+  
+  // TODO: disallow self edges?
+  def invariant(g : Graph) = g.nVertices >= 0
+  
+  // true if x & y have same number of nodes and y has all x's edges
+  def isSubGraph(x : Graph, y : Graph) : Boolean = {
+    require(invariant(x) && invariant(y))
+    
+    var ret : Boolean = (x.nVertices == y.nVertices)
+    if (ret){
+      var i = 0
+      while(i<x.nVertices) {
+        var j = 0;
+        while(j < x.nVertices) {
+          ret &&= !x.edges.isDefinedAt((i,j)) || y.edges.isDefinedAt((i,j))
+          j += 1
+        }
+        i += 1
+      }
+    }
+    ret
+  }
+  
+  // true if every edge has a weight of at least 0
+  def nonnegativeWeights(g : Graph) : Boolean = {
+    require(invariant(g))
+    
+    var ret : Boolean = true
+    var i = 0
+    while(i<g.nVertices) {
+      var j = 0;
+      while(j < g.nVertices) {
+        ret = if (g.edges.isDefinedAt((i,j))){
+          if (g.edges((i,j)) >= 0) ret
+          else false
+        } else ret
+        j += 1
+      }
+      i += 1
+    }
+    ret
+  }
+  
+  
+  /***************************************************************************
+   * Dijkstra's algorithm
+   **************************************************************************/
+  
+  def mapDefinedFor(map:Map[Int,Int], set:Set[Int]) : Boolean = {
+    if (set == Set.empty[Int])
+      true
+    else{
+      val i = epsilon( (i:Int) => set.contains(i) )
+      if (map.isDefinedAt(i))
+        mapDefinedFor(map, set -- Set(i))
+      else
+        false
+    }
+  }
+  
+  /** Find the unvisited node with lowest distance.
+   *
+   * @param visited List of visited nodes
+   * @param distances Map of nodes to distances. Should be defined for all
+   *  elements in toVisit.
+   * @return Best node, best distance, or (-1, Int.MaxValue) if no nodes.
+   */
+  def smallestUnvisited( nVertices:Int, visited:Set[Int], distances:Map[Int,Int] ) : (Int,Int) ={
+    require(mapDefinedFor(distances, visited))
+//     println("smallestUnvisited: "+nVertices+", "+visited+", "+distances)
+    var bestNode = -1
+    var bestDist = Int.MaxValue
+    var node = 0
+    while (node<nVertices){
+      if (!visited.contains(node) && distances(node)<bestDist){
+        bestNode = node
+        bestDist = distances(node)
+      }
+      node += 1
+    }
+//     println("result: "+bestNode, bestDist)
+    (bestNode, bestDist)
+  } ensuring (ret => (ret._1== -1 && ret._2==Int.MaxValue) ||
+    (0<=ret._1 && ret._1<nVertices && !visited.contains(ret._1) && distances(ret._1) == ret._2))
+  
+  
+  // common precondition: g is a valid graph and a and b are valid nodes
+  def bounds(g : Graph, a : Int, b : Int) : Boolean =
+    invariant(g) && 0 <= a && a < g.nVertices && 0 <= b && b < g.nVertices
+  
+  def min(a:Int, b:Int) = if (a<b) a else b
+  // Generate map of "inf" distances for each node. "Inf" is Int.MaxValue.
+  def infDistances(n:Int) : Map[Int,Int] ={
+    if (n < 0) Map.empty[Int,Int]
+    else infDistances(n-1).updated(n,Int.MaxValue)
+  }
+  
+  // find the shortest path from a to b in g, and return its distance
+  // return -1 if the two aren't connected
+  def shortestPath(g : Graph, a : Int, b : Int) : Int = {
+    require(bounds(g,a,b) && nonnegativeWeights(g))
+    
+    // We should always have at least some node if we haven't reached b (so
+    // long as b is in the graph and connected to a).
+    def spVisit (visited:Set[Int], distances:Map[Int,Int]) : Int = {
+      require(bounds(g,a,b))
+//       println("spVisit: "+visited+", "+distances)
+      
+      val (node,dist) = smallestUnvisited(g.nVertices, visited, distances)
+      if (node == b || node < 0)
+        dist
+      else {
+        var newDistances = distances
+        var n = 0
+        
+        (while (n < g.nVertices){
+          if (n != node && !visited.contains(n) && g.edges.isDefinedAt((node,n))){
+            newDistances = newDistances.updated(n,
+              min(newDistances(n), dist+g.edges((node,n))))
+          }
+          n = n + 1
+        }) invariant(/*TODO: and that all elements in newVisitable are defined in newDistances*/ n >= 0 && n <= g.nVertices)
+        
+        spVisit(visited ++ Set(node), newDistances)
+      }
+    }
+    
+    // We start from a, which has distance 0. All other nodes are unreachable.
+    spVisit(Set.empty, infDistances(g.nVertices).updated(a,0))
+  } // TODO ensuring (res => res >= -1 /*(if (isReachable(g,a,b)) res>=0 else res== -1)*/)
+  
+  def main(args: Array[String]) {
+    val spanningTreeE = Map((0,1) -> 1, (0,2) -> 2, (2,3) -> 5, (0,3) -> 10, (3,2) -> 0)
+    val spanningTree = Graph(4, spanningTreeE)
+    val singleGraph = Graph(1, Map.empty)
+    
+    println(spanningTree)
+    println("from 0 to 3 (should be 7): "+shortestPath(spanningTree,0,3))
+    println("from 3 to 1 (no path): "+shortestPath(spanningTree,3,1))
+  }
+}
diff --git a/testcases/graph/dijkstras/DijkstrasSetToVisit.scala b/testcases/graph/dijkstras/DijkstrasSetToVisit.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6b6cccec647e3d9be4b47e3483021753d48e8b87
--- /dev/null
+++ b/testcases/graph/dijkstras/DijkstrasSetToVisit.scala
@@ -0,0 +1,149 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+/** Implementation of Dijkstra's algorithm. Maintains a list of visitable
+ * vertices, and iterates over this, looking distances up in a map.
+ */
+object DijkstrasSetToVisit {
+  /***************************************************************************
+   * Graph representation and algorithms
+   **************************************************************************/
+  case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
+  
+  // TODO: disallow self edges?
+  def invariant(g : Graph) = g.nVertices >= 0
+  
+  // true if x & y have same number of nodes and y has all x's edges
+  def isSubGraph(x : Graph, y : Graph) : Boolean = {
+    require(invariant(x) && invariant(y))
+    
+    var ret : Boolean = (x.nVertices == y.nVertices)
+    if (ret){
+      var i = 0
+      while(i<x.nVertices) {
+        var j = 0;
+        while(j < x.nVertices) {
+          ret &&= !x.edges.isDefinedAt((i,j)) || y.edges.isDefinedAt((i,j))
+          j += 1
+        }
+        i += 1
+      }
+    }
+    ret
+  }
+  
+  // true if every edge has a weight of at least 0
+  def nonnegativeWeights(g : Graph) : Boolean = {
+    require(invariant(g))
+    
+    var ret : Boolean = true
+    var i = 0
+    while(i<g.nVertices) {
+      var j = 0;
+      while(j < g.nVertices) {
+        ret = if (g.edges.isDefinedAt((i,j))){
+          if (g.edges((i,j)) >= 0) ret
+          else false
+        } else ret
+        j += 1
+      }
+      i += 1
+    }
+    ret
+  }
+  
+  
+  /***************************************************************************
+   * Dijkstra's algorithm
+   **************************************************************************/
+  
+  /** Find the unvisited node with lowest distance.
+   *
+   * @param toVisit List of nodes to visit
+   * @param distances Map of nodes to distances. Should be defined for all
+   *  elements in toVisit.
+   * @param best Best node, distance so far, or -1, Int.MaxValue
+   * @return Best node, best distance, or best if no nodes.
+   */
+  def smallestUnvisited0( toVisit:Set[Int], distances:Map[Int,Int], best:(Int,Int) ) : (Int,Int) ={
+    if (toVisit == Set.empty[Int])
+      best
+    else{
+      val node = epsilon( (x:Int) => toVisit.contains(x) )
+      val dist = distances(node)
+      val next:(Int,Int) =
+        if (dist < best._2) (node,dist)
+      else best
+      smallestUnvisited0(toVisit -- Set(node), distances, next)
+    }
+  }
+  /** Find the unvisited node with lowest distance.
+   *
+   * @param toVisit List of nodes to visit
+   * @param distances Map of nodes to distances. Should be defined for all
+   *  elements in toVisit.
+   * @return Best node, best distance, or (-1, Int.MaxValue) if no nodes.
+   */
+  def smallestUnvisited( toVisit:Set[Int], distances:Map[Int,Int] ) : (Int,Int) ={
+    smallestUnvisited0(toVisit, distances, (-1, Int.MaxValue))
+  } ensuring (ret => (ret._1== -1 && ret._2==Int.MaxValue) || (toVisit.contains(ret._1) && distances(ret._1) == ret._2))
+  
+  
+  // common precondition: g is a valid graph and a and b are valid nodes
+  def bounds(g : Graph, a : Int, b : Int) : Boolean =
+    invariant(g) && 0 <= a && a < g.nVertices && 0 <= b && b < g.nVertices
+  
+  def min(a:Int, b:Int) = if (a<b) a else b
+  // Generate map of "inf" distances for each node. "Inf" is Int.MaxValue.
+  def infDistances(n:Int) : Map[Int,Int] ={
+    if (n < 0) Map.empty[Int,Int]
+    else infDistances(n-1).updated(n,Int.MaxValue)
+  }
+  
+  // find the shortest path from a to b in g, and return its distance
+  // return -1 if the two aren't connected
+  def shortestPath(g : Graph, a : Int, b : Int) : Int = {
+    require(bounds(g,a,b) && nonnegativeWeights(g))
+    
+    // We should always have at least some node if we haven't reached b (so
+    // long as b is in the graph and connected to a).
+    def spVisit (visited:Set[Int], toVisit:Set[Int], distances:Map[Int,Int]) : Int = {
+      require(bounds(g,a,b) && toVisit.contains(b))
+      
+      val (node,dist) = smallestUnvisited(toVisit, distances)
+      if (node == b || node < 0)
+        dist
+      else {
+        var newVisitable = toVisit
+        var newDistances = distances
+        var n = 0
+        
+        (while (n < g.nVertices){
+          if (n != node && !visited.contains(n) && g.edges.isDefinedAt((node,n))){
+            newVisitable = newVisitable++Set(n)
+            newDistances = newDistances.updated(n,
+              min(newDistances(n), dist+g.edges((node,n))))
+          }
+          n = n + 1
+        }) invariant(/*TODO: and that all elements in newVisitable are defined in newDistances*/ n >= 0 && n <= g.nVertices)
+        
+        spVisit(visited ++ Set(node), newVisitable, newDistances)
+      }
+    }
+    
+    // We start from a, which has distance 0. All other nodes are unreachable.
+    spVisit(Set.empty, Set(a), infDistances(g.nVertices).updated(a,0))
+  } // TODO ensuring (res => res >= -1 /*(if (isReachable(g,a,b)) res>=0 else res== -1)*/)
+  
+  def main(args: Array[String]) {
+    val spanningTreeE = Map((0,1) -> 1, (0,2) -> 2, (2,3) -> 5, (0,3) -> 10, (3,2) -> 0)
+    val spanningTree = Graph(4, spanningTreeE)
+    val singleGraph = Graph(1, Map.empty)
+    
+    println(spanningTree)
+    println("from 0 to 3 (should be 7): "+shortestPath(spanningTree,0,3))
+    println("from 3 to 1 (no path): "+shortestPath(spanningTree,3,1))
+  }
+}
diff --git a/testcases/graph/dijkstras/DijkstrasSortedList.scala b/testcases/graph/dijkstras/DijkstrasSortedList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8e586348d6eb1e5d4175a12b5cf27b0d4e3bc040
--- /dev/null
+++ b/testcases/graph/dijkstras/DijkstrasSortedList.scala
@@ -0,0 +1,236 @@
+import scala.collection.immutable._
+
+import leon.Annotations._
+import leon.Utils._
+
+/** Implementation of Dijkstra's algorithm.
+ *
+ * Complexity is a bit beyond what Leon can handle. See individual tests on
+ * SortedNDList.
+ */
+object DijkstrasSortedList {
+  /***************************************************************************
+   * Graph representation and algorithms
+   **************************************************************************/
+  case class Graph(nVertices : Int, edges : Map[(Int,Int), Int])
+  
+  // Disallow self edges? Not actually important since they can be ignored.
+  def invariant(g : Graph) = g.nVertices >= 0
+  
+  // true if x & y have same number of nodes and y has all x's edges
+  def isSubGraph(x : Graph, y : Graph) : Boolean = {
+    require(invariant(x) && invariant(y))
+    
+    var ret : Boolean = (x.nVertices == y.nVertices)
+    if (ret){
+      var i = 0
+      while(i<x.nVertices) {
+        var j = 0;
+        while(j < x.nVertices) {
+          if (i != j)
+            ret &&= !x.edges.isDefinedAt((i,j)) || y.edges.isDefinedAt((i,j))
+          j += 1
+        }
+        i += 1
+      }
+    }
+    ret
+  }
+  
+  // true if every edge has a weight of at least 0
+  def nonnegativeWeights(g : Graph) : Boolean = {
+    require(invariant(g))
+    
+    var ret : Boolean = true
+    var i = 0
+    while(i<g.nVertices) {
+      var j = 0;
+      while(j < g.nVertices) {
+        ret = if (i != j && g.edges.isDefinedAt((i,j))){
+          if (g.edges((i,j)) >= 0) ret
+          else false
+        } else ret
+        j += 1
+      }
+      i += 1
+    }
+    ret
+  }
+  
+  // true if b is reachable from a
+  def isReachable(g : Graph, a : Int, b : Int) : Boolean = {
+    require(invariant(g) && a >= 0 && a < g.nVertices && b >= 0 && b < g.nVertices)
+    
+    //TODO
+    false
+  }
+  
+  
+  /***************************************************************************
+   * Sorted list representation and algorithims
+   **************************************************************************/
+   
+  /** A list containing node, dist pairs.
+   *
+   * Sorted by distance, nearest first. Distance must be non-negative. Node
+   * values must be unique and non-negative.
+   */
+  abstract class SortedNDList
+  case class ListNode(val node : Int, val dist : Int, var next : SortedNDList) extends SortedNDList
+  case class ListEnd() extends SortedNDList
+  
+  /** List invariant (see description above) */
+  @induct
+  def sndInvariant(list : SortedNDList) : Boolean = {
+    // Most conditions are commented out. Leon cannot even check adding or
+    // removing an element satisfies the invariant in this case!
+    def invRec(list : SortedNDList/*, elts : Set[Int], minDist : Int, len : Int*/) : Boolean =
+      list match {
+        case ListNode(n,d,next) =>
+          if (d >= 0/*minDist*/ && n >= 0 /*&& !elts.contains(n)*/)
+            invRec(next/*,elts++Set(n),d, len + 1*/)
+          else
+            false
+        case ListEnd() => true //len <= 3
+      }
+    
+    invRec(list/*, Set.empty, 0, 0*/)
+  }
+  
+  /** Look for node in list and remove, if it exists. */
+  @induct
+  def removeFromList(list : SortedNDList, node : Int) : SortedNDList ={
+    // something about this times out
+    require(sndInvariant(list))
+    
+    //println("removeFromList: "+list)
+    
+    list match  {
+      case ListNode(n,d,next) =>
+        if (n == node)
+          // drop current node and continue search:
+          removeFromList(next, node)
+        else
+          ListNode(n,d,removeFromList(next, node))
+      case ListEnd() => list
+    }
+  } ensuring(sndInvariant(_))   // something about this generates an error: is the precondition not checked for _all_ elements or something?
+  
+  /** Return true if list contains node */
+  @induct
+  def listContains(list : SortedNDList, node : Int) : Boolean ={
+    // something to do with this times out
+    require(sndInvariant(list))
+    list match {
+      case ListNode(n,d,next) =>
+        if (node == n) true
+        else listContains(next, node)
+      case ListEnd() => false
+    }
+  }
+  
+  /** Add a new node to the list, such that list remains sorted by distance.
+   * Assume node is not already in list. */
+  @induct
+  def addSorted(list : SortedNDList, node : Int, dist : Int) : SortedNDList = {
+    // something to do with this times out
+    require(sndInvariant(list) && !listContains(list, node) && node >= 0 && dist >= 0)
+    
+    list match {
+      case ListNode(n,d,next) =>
+        if (d > dist)        // insert here
+          ListNode(node, dist, list)
+        else
+          ListNode(n,d, addSorted(next, node, dist))
+      case ListEnd() => // insert at end
+        ListNode(node, dist, list)
+    }
+  } ensuring (sndInvariant(_))  // something to do with this times out
+  
+  /** Update node with distance minimum of dist and current value. Add if not
+   * in list, and maintain sorted order. */
+  @induct
+  def updateDistInList(list : SortedNDList, node : Int, dist : Int) : SortedNDList = {
+    require(sndInvariant(list) && node >= 0 && dist >= 0)
+    
+    val listRemoved = removeFromList(list, node)
+    addSorted(listRemoved, node, dist)
+  } ensuring(sndInvariant(_))
+  
+   
+  /***************************************************************************
+   * Dijkstra's algorithm
+   **************************************************************************/
+  
+  def isNodeNotB(list : SortedNDList, b : Int) : Boolean =
+    list match {
+      case ListNode(n, _, _) => n!=b
+      case ListEnd() => false
+    }
+  
+  // common precondition: g is a valid graph and a and b are valid nodes
+  def bounds(g : Graph, a : Int, b : Int) : Boolean =
+    invariant(g) && 0 <= a && a < g.nVertices && 0 <= b && b < g.nVertices
+  
+  // find the shortest path from a to b in g, and return its distance
+  // return -1 if the two aren't connected
+  def shortestPath(g : Graph, a : Int, b : Int) : Int = {
+    require(bounds(g,a,b) && nonnegativeWeights(g))
+    
+    // We should always have at least some node if we haven't reached b (so
+    // long as b is in the graph and connected to a).
+    @induct
+    def spVisit (list : SortedNDList, visited : Set[Int]) : SortedNDList = {
+      require(bounds(g,a,b) && (!visited.contains(b) || listContains(list,b)) && sndInvariant(list))
+      /* TODO: also check that all list nodes are less than g.nVertices.
+       * We should check same invariant at function exit. But there's no point:
+       * it's too much for Leon to reason about at once!
+       */
+      
+      list match {
+        case ListNode(node, dist, next) if (node==b) =>
+          list
+        case ListNode(node, dist, next) =>
+          var n = 0
+          var tail : SortedNDList = next
+          
+          (while (n < g.nVertices){
+            if (n != node && !visited.contains(n) && g.edges.isDefinedAt((node,n)))
+              tail = updateDistInList(tail, n, dist+g.edges((node,n)))
+            n = n + 1
+          }) invariant(sndInvariant(list) && n >= 0 && n <= g.nVertices)
+          
+          spVisit (tail, visited ++ Set(node))
+        case ListEnd() =>
+          list
+      }
+    } ensuring(res => res match {
+      case ListEnd() => !isReachable(g,a,b)
+      case ListNode(node,_,_) => node==b
+    })
+    
+    // We start from a, which has distance 0. All other nodes implicitly have
+    // infinite distance.
+    val startingList : SortedNDList = ListNode(a, 0, ListEnd())
+    spVisit(startingList, Set.empty) match {
+      case ListNode(n, d, _) =>
+        //assert(n==b)
+        if (n != b)
+          -2    // Leon should prove this doesn't happen — what a way to do assert(false)
+        else
+          d
+      case ListEnd() =>
+        -1
+    }
+  } ensuring (res => res >= -1 /*(if (isReachable(g,a,b)) res>=0 else res== -1)*/)
+  
+  def main(args: Array[String]) {
+    val spanningTreeE = Map((0,1) -> 1, (0,2) -> 2, (2,3) -> 5, (0,3) -> 10, (3,2) -> 0)
+    val spanningTree = Graph(4, spanningTreeE)
+    val singleGraph = Graph(1, Map.empty)
+    
+    println(spanningTree)
+    println("from 0 to 3 (should be 7): "+shortestPath(spanningTree,0,3))
+    println("from 3 to 1 (no path): "+shortestPath(spanningTree,3,1))
+  }
+}