diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 644b91dd1a1088f725c65448a0542fa8d57639ad..99567a865bc09b8c3b154ae220d48d7fad5898fd 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -478,7 +478,7 @@ trait AbstractZ3Solver extends Z3Solver {
 
       case fb @ FiniteBag(elems, base) =>
         typeToSort(fb.getType)
-        toSMT(RawArrayValue(base, elems, InfiniteIntegerLiteral(0)))
+        rec(RawArrayValue(base, elems, InfiniteIntegerLiteral(0)))
 
       case BagAdd(b, e) =>
         val bag = rec(b)
@@ -496,12 +496,12 @@ trait AbstractZ3Solver extends Z3Solver {
         rec(BagDifference(b1, BagDifference(b1, b2)))
 
       case BagDifference(b1, b2) =>
-        val abs = z3.getFuncDecl(OpAbs, typeToSort(IntegerType))
+        val abs = z3.getAbsFuncDecl()
         val plus = z3.getFuncDecl(OpAdd, typeToSort(IntegerType), typeToSort(IntegerType))
         val minus = z3.getFuncDecl(OpSub, typeToSort(IntegerType), typeToSort(IntegerType))
         val div = z3.getFuncDecl(OpDiv, typeToSort(IntegerType), typeToSort(IntegerType))
 
-        val all2 = z3.mkArrayConst(typeToSort(IntegerType), z3.mkInt(2))
+        val all2 = z3.mkConstArray(typeToSort(IntegerType), z3.mkInt(2, typeToSort(IntegerType)))
         val withNeg = z3.mkArrayMap(minus, rec(b1), rec(b2))
         z3.mkArrayMap(div, z3.mkArrayMap(plus, withNeg, z3.mkArrayMap(abs, withNeg)), all2)
 
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 04f0e34aa46c012425622a2b5fce9f8054d04405..b2059214b9d7fa666cae8028ea821d45e62d5f26 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -133,8 +133,8 @@ class FairZ3Solver(val sctx: SolverContext, val program: Program)
 
     def extractNot(l: Z3AST): Option[Z3AST] = z3.getASTKind(l) match {
       case Z3AppAST(decl, args) => z3.getDeclKind(decl) match {
-        case Z3DeclKind.OpNot => Some(args.head)
-        case Z3DeclKind.OpUninterpreted => None
+        case OpNot => Some(args.head)
+        case _ => None
       }
       case ast => None
     }
diff --git a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
index c367f8f3c4156375c2e03eb18359e8d2eec87d2f..454cc37dc2de78e38b038f835a2ec38f24c8d539 100644
--- a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
@@ -10,6 +10,5 @@ import unrolling._
 import theories._
 
 class Z3UnrollingSolver(context: SolverContext, program: Program, underlying: Z3Solver)
-  extends UnrollingSolver(context, program, underlying,
-                          new StringEncoder(context.context, program)
+  extends UnrollingSolver(context, program, underlying, new StringEncoder(context.context, program))
      with Z3Solver
diff --git a/unmanaged/scalaz3-unix-64.jar b/unmanaged/scalaz3-unix-64.jar
index 722e6494ae7890a4723eb00e9ba85e07ec53b6d4..de541da39b992694a47a585c3a29d7f749a0f9e5 100644
Binary files a/unmanaged/scalaz3-unix-64.jar and b/unmanaged/scalaz3-unix-64.jar differ