diff --git a/library/lang/synthesis/Oracle.scala b/library/lang/synthesis/Oracle.scala
index cc0af641559a83934fbc0e49f57bdf70c48ecf52..34867e3f9ebabfae32d6e9fd7d6238345247ed36 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