From 0303b6369e31896966e6ecbad8a89780e270912e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 5 Jun 2014 14:47:00 +0200
Subject: [PATCH] Fix annotation for Oracle
---
library/lang/synthesis/Oracle.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/library/lang/synthesis/Oracle.scala b/library/lang/synthesis/Oracle.scala
index cc0af6415..34867e3f9 100644
--- a/library/lang/synthesis/Oracle.scala
+++ b/library/lang/synthesis/Oracle.scala
@@ -8,7 +8,7 @@ import leon.lang._
import scala.annotation._
@implicitNotFound("No Oracle available for this source of non-determinism, please provide an implicit arg <: Oracle[T]")
-@verified
+@library
abstract class Oracle[T] {
def head: T = this match {
case Node(_, h, _) => h
--
GitLab