diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 49ab85e95c7675d852057bf448ccec5742d100c2..46b37eaf622de6ba1645d69143e69df52577b373 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -211,9 +211,16 @@ object Main {
     import verification.AnalysisPhase
     import repair.RepairPhase
 
+    val pipeSanityCheck : Pipeline[Program, Program] = 
+      if(!settings.xlang)
+        xlang.NoXlangFeaturesChecking
+      else
+        NoopPhase()
+
     val pipeBegin : Pipeline[List[String],Program] =
       ExtractionPhase andThen
-      PreprocessingPhase
+      PreprocessingPhase andThen
+      pipeSanityCheck
 
     val pipeProcess: Pipeline[Program, Any] = {
       if (settings.synthesis) {
diff --git a/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2bc7d702e24bf12a8cbec0dd6791fa68ae4460ae
--- /dev/null
+++ b/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
@@ -0,0 +1,51 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package xlang
+
+import purescala.Common._
+import purescala.TypeTrees._
+import purescala.Trees._
+import purescala.Definitions._
+import purescala.Constructors._
+
+import purescala.TreeOps.exists
+import xlang.Trees._
+
+object NoXlangFeaturesChecking extends UnitPhase[Program] {
+
+  val name = "no-xlang"
+  val description = "Ensure and enforce that no xlang features are used"
+
+  private def isXlangExpr(expr: Expr): Boolean = expr match {
+
+    case Block(_, _) => true
+
+    case Assignment(_, _) => true
+
+    case While(_, _) => true
+
+    case Epsilon(_, _) => true
+
+    case EpsilonVariable(_, _) => true
+
+    case LetVar(_, _, _) => true
+
+    case Waypoint(_, _, _) => true
+
+    case ArrayUpdate(_, _, _) => true 
+
+    case _ => false
+
+  }
+
+  override def apply(ctx: LeonContext, pgm: Program): Unit = {
+    pgm.definedFunctions.foreach(fd => {
+      if(exists(isXlangExpr)(fd.fullBody)) {
+        ctx.reporter.fatalError(fd.fullBody.getPos, "Expr is using xlang features")
+      }
+    })
+  }
+
+}
+
diff --git a/src/test/resources/regression/verification/purescala/error/Asserts.scala b/src/test/resources/regression/verification/purescala/error/Asserts.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e19e8f2826c83e0944ce8f4f5547d2125b5c93bc
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/error/Asserts.scala
@@ -0,0 +1,16 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang._
+
+object Asserts {
+
+  def assert1(i: BigInt): BigInt = { // we might define assert like so
+    require(i >= 0)
+    i
+  }
+
+  def sum(to: BigInt): BigInt = {
+    assert1(to)
+    to
+  }
+}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 71148aa5df64c13fd3e2cc05140d45409f69093a..b4f119ad8a04e8d850b145712def292b702a7fd5 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -23,8 +23,9 @@ class PureScalaVerificationRegression extends LeonTestSuite {
   private case class Output(report : VerificationReport, reporter : Reporter)
 
   private def mkPipeline : Pipeline[List[String], VerificationReport] =
-    ExtractionPhase     andThen
-    PreprocessingPhase  andThen
+    ExtractionPhase                andThen
+    PreprocessingPhase             andThen
+    xlang.NoXlangFeaturesChecking  andThen
     AnalysisPhase
 
   private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {