diff --git a/demo/AssociativeList.scala b/demo/AssociativeList.scala
index ed18a6bba8619fd38aa3d38d9fcea7808a5eedaf..dc56e8fd4eb2c28c216e7191990a31084c5ec89a 100644
--- a/demo/AssociativeList.scala
+++ b/demo/AssociativeList.scala
@@ -10,16 +10,16 @@ object AssociativeList {
   case class Cons(head: KeyValuePairAbs, tail: List) extends List
   case class Nil() extends List
 
-  sealed abstract class OptInt
-  case class Some(i: Int) extends OptInt
-  case class None() extends OptInt
+  sealed abstract class OptionInt
+  case class Some(i: Int) extends OptionInt
+  case class None() extends OptionInt
 
   def domain(l: List): Set[Int] = l match {
     case Nil() => Set.empty[Int]
     case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
   }
 
-  def find(l: List, e: Int): OptInt = l match {
+  def find(l: List, e: Int): OptionInt = l match {
     case Nil() => None()
     case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
   }
@@ -44,17 +44,7 @@ object AssociativeList {
   })
 
   @induct
-  def readOverWrite(l: List, e: KeyValuePairAbs, k: Int) : Boolean = (e match {
-    case KeyValuePair(key, value) =>
-      find(updateElem(l, e), k) == (if (k == key) Some(value) else find(l, k))
-  }) holds
-
-  // def prop0(e: Int): Boolean = (find(update(Nil(), Nil()), e) == find(Nil(), e)) holds
-
-  def main(args: Array[String]): Unit = {
-    val l = Cons(KeyValuePair(6, 1), Cons(KeyValuePair(5, 4), Cons(KeyValuePair(3, 2), Nil())))
-    val e = 0
-    println(find(update(Nil(), l), e))
-    println(find(l, e))
-  }
+  def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
+    find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
+  } holds
 }
diff --git a/demo/RedBlackTree.scala b/demo/RedBlackTree.scala
index bbcbe1adad631f0e57e9a373f2eb7a2a86ccbfca..76712bd2649087b2d5c0ec97fe468a2b17e0fb20 100644
--- a/demo/RedBlackTree.scala
+++ b/demo/RedBlackTree.scala
@@ -67,8 +67,7 @@ object RedBlackTree {
   } ensuring (res => content(res) == content(t) ++ Set(x) 
                    && size(t) <= size(res) && size(res) <= size(t) + 1
                    && redDescHaveBlackChildren(res)
-                   && blackBalanced(res)
-                   )
+                   && blackBalanced(res))
 
   def makeBlack(n: Tree): Tree = {
     require(redDescHaveBlackChildren(n) && blackBalanced(n))
diff --git a/src/purescala/AbstractZ3Solver.scala b/src/purescala/AbstractZ3Solver.scala
index 3f50e723cd758d48269add1bda4d8c0b06394410..37575e0a166fd5f5b3bf110b6650f4c6071c6e53 100644
--- a/src/purescala/AbstractZ3Solver.scala
+++ b/src/purescala/AbstractZ3Solver.scala
@@ -72,7 +72,7 @@ trait AbstractZ3Solver {
             //val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(p._2)).foldLeft(z3.mkTrue)((a, b) => a && b)
             val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(adtFieldSelectors(p._1.id)(term))).foldLeft(z3.mkTrue)((a, b) => a && b)
             val axiom = z3.mkForAll(0, List(pattern), fields.zipWithIndex.map{case (f, i) => (z3.mkIntSymbol(i), typeToSort(f.getType))}, constraint)
-            println("Asserting: " + axiom)
+            //println("Asserting: " + axiom)
             z3.assertCnstr(axiom)
           }
       }
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 41c649c340f7a747586962f84d46d92926b197fa..3fc21a5b0797394d29a09cbc5bcf779fcb69f6a4 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -13,7 +13,7 @@ import scala.collection.mutable.{Set => MutableSet}
 class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3Solver with Z3ModelReconstruction {
   assert(Settings.useFairInstantiator)
 
-  private final val UNKNOWNASSAT : Boolean = true
+  private final val UNKNOWNASSAT : Boolean = false
 
   val description = "Fair Z3 Solver"
   override val shortDescription = "Z3-f"
@@ -21,6 +21,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
   // this is fixed
   private val z3cfg = new Z3Config(
     "MODEL" -> true,
+    "MBQI" -> false,
     "SOFT_TIMEOUT" -> 100,
     "TYPE_CHECK" -> true,
     "WELL_SORTED_CHECK" -> true
@@ -229,7 +230,6 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
   def solveWithBounds(vc: Expr, fv: Boolean) : (Option[Boolean], Map[Identifier,Expr]) = {
     restartZ3
     boundValues
-    println(z3.check)
     decideWithModel(vc, fv)
   }
 
@@ -444,7 +444,6 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
         definitiveAnswer = None
         definitiveModel = Map.empty
         reporter.error("Max. number of iterations reached.")
-        println("Max. number of iterations reached.")
       }
     }
 
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 012a50039531e018f8d96d6887d03a9666e68e22..f1aceddd85ef07c9f98488738c5fd9cd67306d61 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -28,6 +28,7 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3S
   // this is fixed
   private val z3cfg = new Z3Config(
     "MODEL" -> true,
+    "MBQI" -> false,
     "SOFT_TIMEOUT" -> 100,
     "TYPE_CHECK" -> true,
     "WELL_SORTED_CHECK" -> true