diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 0b998ad30a988b0723564923d7dcea89e1fae436..3e8f6560570f5e1048582f587a3b2e4d5dcbda53 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -26,7 +26,8 @@ class FunCheckPlugin(val global: Global) extends Plugin {
     "  -P:funcheck:unrolling=[0,1,2]  Unrolling depth for recursive functions" + "\n" + 
     "  -P:funcheck:noaxioms           Don't generate forall axioms for recursive functions" + "\n" + 
     "  -P:funcheck:tolerant           Silently extracts non-pure function bodies as ''unknown''" + "\n" +
-    "  -P:funcheck:quiet              No info and warning messages from the extensions"
+    "  -P:funcheck:quiet              No info and warning messages from the extensions" + "\n" +
+    "  -P:funcheck:XP                 Enable weird transformations and other bug-producing features"
   )
 
   /** Processes the command-line options. */
@@ -41,6 +42,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
         case "quiet"      =>                     purescala.Settings.quietExtensions = true
         case "nodefaults" =>                     purescala.Settings.runDefaultExtensions = false
         case "noaxioms"   =>                     purescala.Settings.noForallAxioms = true
+        case "XP"         =>                     purescala.Settings.experimental = true
         case s if s.startsWith("unrolling=") =>  purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
         case s if s.startsWith("functions=") =>  purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
         case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 1bd8fac0354ac09e2790fefe0239fd0c274bc8fd..b0e2bcab58fd6b97de3c104f5aaf0586ed6fe0e2 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -2,6 +2,7 @@ package purescala
 
 // typically these settings can be changed through some command-line switch.
 object Settings {
+  var experimental : Boolean = false
   var showIDs: Boolean = false
   var quietExtensions: Boolean = false
   var functionsToAnalyse: Set[String] = Set.empty
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index a4405a67cb926b4eb2a75c15d62c0b0f8049f6af..fbe596910f2977c7c2906cc89b393e6cb2aba6e3 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -654,7 +654,7 @@ object Trees {
       }
     }
 
-    def unapply(pm : MatchExpr) : Option[MatchExpr] = pm match {
+    def unapply(pm : MatchExpr) : Option[MatchExpr] = if(!Settings.experimental) None else (pm match {
       case MatchExpr(scrutinee, cases) if cases.forall(_.isInstanceOf[SimpleCase]) => {
         val allPatterns = cases.map(_.pattern)
         Settings.reporter.info("This might be a complete pattern-matching expression:")
@@ -663,7 +663,7 @@ object Trees {
         None
       }
       case _ => None
-    }
+    })
   }
 
   // we use this when debugging our tree transformations...
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index eb25332cc46f52973855e91f045448e6c2cb6441..c828fcd5ebb364d309b5b69f6bf478b0bd46f304 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -139,7 +139,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
     }
 
     // universally quantifies all functions !
-    if(!Settings.noForallAxioms) {
+    if(Settings.experimental && !Settings.noForallAxioms) {
       for(funDef <- program.definedFunctions) if(funDef.hasImplementation && program.isRecursive(funDef) && funDef.args.size > 0) {
         funDef.body.get match {
           case SimplePatternMatching(scrutinee,_,infos) if (