diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 46b37eaf622de6ba1645d69143e69df52577b373..dd177e7e20dab7ee8baafe06cb4a6f8b434f5df2 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -18,7 +18,7 @@ object Main {
       xlang.EpsilonElimination,
       xlang.ImperativeCodeElimination,
       purescala.FunctionClosure,
-      xlang.XlangAnalysisPhase,
+      xlang.XLangAnalysisPhase,
       synthesis.SynthesisPhase,
       termination.TerminationPhase,
       verification.AnalysisPhase,
@@ -207,13 +207,13 @@ object Main {
     import frontends.scalac.ExtractionPhase
     import synthesis.SynthesisPhase
     import termination.TerminationPhase
-    import xlang.XlangAnalysisPhase
+    import xlang.XLangAnalysisPhase
     import verification.AnalysisPhase
     import repair.RepairPhase
 
     val pipeSanityCheck : Pipeline[Program, Program] = 
       if(!settings.xlang)
-        xlang.NoXlangFeaturesChecking
+        xlang.NoXLangFeaturesChecking
       else
         NoopPhase()
 
@@ -230,7 +230,7 @@ object Main {
       } else if (settings.termination) {
         TerminationPhase
       } else if (settings.xlang) {
-        XlangAnalysisPhase
+        XLangAnalysisPhase
       } else if (settings.verify) {
         purescala.FunctionClosure andThen AnalysisPhase
       } else {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 1be1f99ab14d919c288ec89832681362685f6127..a7de9904e15713b9189655da47bbe79256430c3c 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -254,6 +254,17 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
         //Recall that Choose cannot mutate variables from the scope
         (c, (b2: Expr) => b2, Map())
       }
+
+      case i @ FunctionInvocation(fd, args) =>
+        //function invocation can have side effects so we should keep them as local
+        //val names.
+        val scope = (body: Expr) => {
+          Let(FreshIdentifier("tmp", fd.returnType),
+              i,
+              body)
+        }
+        (i, scope, Map())
+
       case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
       case n @ NAryOperator(args, recons) => {
         val (recArgs, scope, fun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
@@ -278,6 +289,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
         val (argVal, argScope, argFun) = toFunction(a)
         (recons(argVal).copiedFrom(u), argScope, argFun)
       }
+
       case (t: Terminal) => (t, (body: Expr) => body, Map())
 
 
diff --git a/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
similarity index 94%
rename from src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
rename to src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
index 2bc7d702e24bf12a8cbec0dd6791fa68ae4460ae..08425aada0b910f6e26ab11134884bf35a08455e 100644
--- a/src/main/scala/leon/xlang/NoXlangFeaturesChecking.scala
+++ b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
@@ -12,7 +12,7 @@ import purescala.Constructors._
 import purescala.TreeOps.exists
 import xlang.Trees._
 
-object NoXlangFeaturesChecking extends UnitPhase[Program] {
+object NoXLangFeaturesChecking extends UnitPhase[Program] {
 
   val name = "no-xlang"
   val description = "Ensure and enforce that no xlang features are used"
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
similarity index 98%
rename from src/main/scala/leon/xlang/XlangAnalysisPhase.scala
rename to src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 03c8d2e71c079afbeceaf76ef2e97eb4e3bb45e9..ff8e5a34cba848fcc1c1cbe8c4e1f13973d2bbf8 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -6,7 +6,7 @@ package xlang
 import leon.purescala.Definitions._
 import leon.verification._
 
-object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
+object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
 
   val name = "xlang analysis"
   val description = "apply analysis on xlang"
diff --git a/src/test/resources/regression/verification/xlang/invalid/Asserts.scala b/src/test/resources/regression/verification/xlang/invalid/Asserts.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e19e8f2826c83e0944ce8f4f5547d2125b5c93bc
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/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 b4f119ad8a04e8d850b145712def292b702a7fd5..0be138d6d679da509853bb893377291e3ca0c678 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -25,7 +25,7 @@ class PureScalaVerificationRegression extends LeonTestSuite {
   private def mkPipeline : Pipeline[List[String], VerificationReport] =
     ExtractionPhase                andThen
     PreprocessingPhase             andThen
-    xlang.NoXlangFeaturesChecking  andThen
+    xlang.NoXLangFeaturesChecking  andThen
     AnalysisPhase
 
   private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 680948c287021165fea09f9e9bc1915872d5a724..5569f6c570e072901f615621e02ea1bc5941f9d0 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -6,7 +6,7 @@ import leon._
 import leon.test._
 
 import leon.verification.VerificationReport
-import leon.xlang.XlangAnalysisPhase
+import leon.xlang.XLangAnalysisPhase
 import leon.frontends.scalac.ExtractionPhase
 import leon.utils.PreprocessingPhase
 
@@ -23,7 +23,7 @@ class XLangVerificationRegression extends LeonTestSuite {
   private def mkPipeline : Pipeline[List[String],VerificationReport] =
     ExtractionPhase     andThen
     PreprocessingPhase  andThen
-    XlangAnalysisPhase
+    XLangAnalysisPhase
 
   private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
     val fullName = file.getPath()