diff --git a/WISHLIST b/WISHLIST
index ad101dd4e512f9986bfb0ede3d99cffca3bc3e65..f3f3f786da25cf432b4ef267afd279198996494b 100644
--- a/WISHLIST
+++ b/WISHLIST
@@ -5,6 +5,7 @@ PS: rewrite pattern-matching translator to use if-then-else
 PS: generate VCs for preconditions
 PS: generate VCs for pattern-matching
 PS: support multiple top-level objects, and use 'private' accessor to indicate what's part of the interface
+PS: support tuples (including natively in Z3)
 
 
 Wishes granted so far
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 826e99d2d18678fb61728961e69813b7024b206c..4a580fa236dc609220776d0b3106a2e6e1c40f7c 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -27,6 +27,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
     "  -P:funcheck:axioms             Generate simple forall axioms for recursive functions when possible" + "\n" + 
     "  -P:funcheck:tolerant           Silently extracts non-pure function bodies as ''unknown''" + "\n" +
     "  -P:funcheck:nobapa             Disable BAPA Z3 extension" + "\n" +
+    "  -P:funcheck:newPM              Use the new pattern-matching translator" + "\n" +
     "  -P:funcheck:quiet              No info and warning messages from the extensions" + "\n" +
     "  -P:funcheck:XP                 Enable weird transformations and other bug-producing features"
   )
@@ -44,6 +45,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
         case "nodefaults" =>                     purescala.Settings.runDefaultExtensions = false
         case "axioms"     =>                     purescala.Settings.noForallAxioms = false
         case "nobapa"     =>                     purescala.Settings.useBAPA = false
+        case "newPM"      =>                     purescala.Settings.useNewPatternMatchingTranslator = 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)): _*)
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 8be325547994522268aee17396920a8cb74963cb..51225d73fc7ff769bdd6348bf38955400fb6b515 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -13,4 +13,5 @@ object Settings {
   var noForallAxioms: Boolean = true
   var unrollingLevel: Int = 0
   var useBAPA: Boolean = true
+  var useNewPatternMatchingTranslator: Boolean = false
 }
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 25073c3244d50c104091f220f44ac0af68003d91..f85158b626694ff5cdf078349bc11b4d8c04aabc 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -9,7 +9,7 @@ import TypeTrees._
 
 import z3plugins.bapa.{BAPATheory, BAPATheoryEqc, BAPATheoryBubbles}
 
-class Z3Solver(reporter: Reporter) extends Solver(reporter) {
+class Z3Solver(reporter: Reporter) extends Solver(reporter) with Z3ModelReconstruction {
   import Settings.useBAPA
   val description = "Z3 Solver"
   override val shortDescription = "Z3"
@@ -23,7 +23,7 @@ class Z3Solver(reporter: Reporter) extends Solver(reporter) {
   // this is fixed
   private val z3cfg = new Z3Config(
     "MODEL" -> true,
-    "SOFT_TIMEOUT" -> 180000, // this one doesn't work apparently
+    "SOFT_TIMEOUT" -> 100,
     "TYPE_CHECK" -> true,
     "WELL_SORTED_CHECK" -> true
     )