diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala
index 6dfea1dbe2cf359b0839a65739149a57aab406e9..b71e5d81971f435af00142b1e3bbe6f82482d7f5 100644
--- a/src/main/scala/leon/purescala/DefinitionTransformer.scala
+++ b/src/main/scala/leon/purescala/DefinitionTransformer.scala
@@ -27,10 +27,8 @@ class DefinitionTransformer(
     super.transform(transformType(tpe).getOrElse(tpe))
   }
 
-
   final override def transform(id: Identifier): Identifier = transformId(id, false)
 
-
   def transformExpr(e: Expr)(implicit bindings: Map[Identifier, Identifier]): Option[Expr] = None
   final override def transform(e: Expr)(implicit bindings: Map[Identifier, Identifier]): Expr = {
     transformExpr(e) match {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 52894a29c644183f0ff77c9ea36ac530aab73ef8..eb55f9b60ea47bc89f883ce9d4c5a18d0456eaa9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -154,6 +154,9 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
       ArrayMap(plus, toSMT(b1), toSMT(b2))
 
     case BagIntersection(b1, b2) =>
+      toSMT(BagDifference(b1, BagDifference(b1, b2)))
+
+    case BagDifference(b1, b2) =>
       val abs   = SortedSymbol("abs", List(IntegerType).map(declareSort), declareSort(IntegerType))
       val plus  = SortedSymbol("+", List(IntegerType, IntegerType).map(declareSort), declareSort(IntegerType))
       val minus = SortedSymbol("-", List(IntegerType, IntegerType).map(declareSort), declareSort(IntegerType))
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 0eff41ea6b9b270bc774ec19b3f5751ec75920fd..644b91dd1a1088f725c65448a0542fa8d57639ad 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -223,6 +223,9 @@ trait AbstractZ3Solver extends Z3Solver {
     case tt @ MapType(fromType, toType) =>
       typeToSort(RawArrayType(fromType, library.optionType(toType)))
 
+    case tt @ BagType(base) =>
+      typeToSort(RawArrayType(base, IntegerType))
+
     case rat @ RawArrayType(from, to) =>
       sorts.cached(rat) {
         val fromSort = typeToSort(from)
@@ -473,6 +476,35 @@ trait AbstractZ3Solver extends Z3Solver {
       case SetDifference(s1, s2) => z3.mkSetDifference(rec(s1), rec(s2))
       case f @ FiniteSet(elems, base) => elems.foldLeft(z3.mkEmptySet(typeToSort(base)))((ast, el) => z3.mkSetAdd(ast, rec(el)))
 
+      case fb @ FiniteBag(elems, base) =>
+        typeToSort(fb.getType)
+        toSMT(RawArrayValue(base, elems, InfiniteIntegerLiteral(0)))
+
+      case BagAdd(b, e) =>
+        val bag = rec(b)
+        val elem = rec(e)
+        z3.mkStore(bag, elem, z3.mkAdd(z3.mkSelect(bag, elem), rec(InfiniteIntegerLiteral(1))))
+
+      case MultiplicityInBag(e, b) =>
+        z3.mkSelect(rec(b), rec(e))
+
+      case BagUnion(b1, b2) =>
+        val plus = z3.getFuncDecl(OpAdd, typeToSort(IntegerType), typeToSort(IntegerType))
+        z3.mkArrayMap(plus, rec(b1), rec(b2))
+
+      case BagIntersection(b1, b2) =>
+        rec(BagDifference(b1, BagDifference(b1, b2)))
+
+      case BagDifference(b1, b2) =>
+        val abs = z3.getFuncDecl(OpAbs, typeToSort(IntegerType))
+        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 withNeg = z3.mkArrayMap(minus, rec(b1), rec(b2))
+        z3.mkArrayMap(div, z3.mkArrayMap(plus, withNeg, z3.mkArrayMap(abs, withNeg)), all2)
+
       case RawArrayValue(keyTpe, elems, default) =>
         val ar = z3.mkConstArray(typeToSort(keyTpe), rec(default))
 
@@ -670,7 +702,7 @@ trait AbstractZ3Solver extends Z3Solver {
                     // We expect a RawArrayValue with keys in from and values in Option[to],
                     // with default value == None
                     if (r.default.getType != library.noneType(to)) {
-                      unsupported(r, "Solver returned a co-finite set which is not supported.")
+                      unsupported(r, "Solver returned a co-finite map which is not supported.")
                     }
                     require(r.keyTpe == from, s"Type error in solver model, expected ${from.asString}, found ${r.keyTpe.asString}")
 
@@ -682,6 +714,14 @@ trait AbstractZ3Solver extends Z3Solver {
                     FiniteMap(elems, from, to)
                 }
 
+              case BagType(base) =>
+                val r @ RawArrayValue(_, elems, default) = rec(t, RawArrayType(base, IntegerType))
+                if (default != InfiniteIntegerLiteral(0)) {
+                  unsupported(r, "Solver returned a co-finite bag which is not supported.")
+                }
+
+                FiniteBag(elems, base)
+
               case tpe @ SetType(dt) =>
                 model.getSetValue(t) match {
                   case None => unsound(t, "invalid set AST")
diff --git a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
index ce224e8dc2baaa4e7d0861f9677c663919dc5aa7..c367f8f3c4156375c2e03eb18359e8d2eec87d2f 100644
--- a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
@@ -11,6 +11,5 @@ import theories._
 
 class Z3UnrollingSolver(context: SolverContext, program: Program, underlying: Z3Solver)
   extends UnrollingSolver(context, program, underlying,
-                          new StringEncoder(context.context, program) >>
-                          new BagEncoder(context.context, program))
+                          new StringEncoder(context.context, program)
      with Z3Solver