diff --git a/src/main/scala/inox/tip/Bags.scala b/src/main/scala/inox/tip/Bags.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a91aaea138977ee581dff211ca718101544580cc
--- /dev/null
+++ b/src/main/scala/inox/tip/Bags.scala
@@ -0,0 +1,43 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package tip
+
+import smtlib.parser.Terms._
+import smtlib.theories.Operations._
+
+object Bags {
+
+  private val BagInsert = "bag.insert"
+  private val BagUnion = "bag.union"
+  private val BagIntersection = "bag.intersection"
+  private val BagEmpty = "bag.empty"
+  private val BagSingleton = "bag.singleton"
+  private val BagMultiplicity = "bag.multiplicity"
+  private val BagDifference = "bag.difference"
+
+  object BagSort {
+    def apply(el: Sort): Sort = Sort(Identifier(SSymbol("Bag")), Seq(el))
+
+    def unapply(sort: Sort): Option[Sort] = sort match {
+      case Sort(Identifier(SSymbol("Bag"), Seq()), Seq(el)) => Some(el)
+      case _ => None
+    }
+  }
+
+  object EmptyBag {
+    def apply(s: Sort): Term = QualifiedIdentifier(Identifier(SSymbol(BagEmpty)), Some(s))
+    def unapply(t: Term): Option[Sort] = t match {
+      case QualifiedIdentifier(Identifier(SSymbol(BagEmpty), Seq()), Some(s)) => Some(s)
+      case _ => None
+    }
+  }
+
+  object Singleton extends Operation2 { override val name = BagSingleton }
+
+  object Union extends Operation2 { override val name = BagUnion }
+  object Intersection extends Operation2 { override val name = BagIntersection }
+  object Difference extends Operation2 { override val name = BagDifference }
+  object Multiplicity extends Operation2 { override val name = BagMultiplicity }
+  object Insert extends OperationN2 { override val name = BagInsert }
+}
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index aebbbbc90e59148b7900ab96b59c139c4d522913..6cde5ecec1dbef4ccbe5d9ba59c96467940b9b92 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -580,6 +580,7 @@ class Parser(file: File) {
     case Sets.Member(e1, e2) => ElementOfSet(extractTerm(e1), extractTerm(e2))
     case Sets.Subset(e1, e2) => SubsetOf(extractTerm(e1), extractTerm(e2))
 
+    case Sets.EmptySet(sort) => FiniteSet(Seq.empty, extractSort(sort))
     case Sets.Singleton(e) =>
       val elem = extractTerm(e)
       FiniteSet(Seq(elem), locals.symbols.bestRealType(elem.getType(locals.symbols)))
@@ -587,7 +588,18 @@ class Parser(file: File) {
     case Sets.Insert(set, es @ _*) =>
       es.foldLeft(extractTerm(set))((s,e) => SetAdd(s, extractTerm(e)))
 
-    // TODO: bags
+    case Bags.Singleton(k, v) =>
+      val key = extractTerm(k)
+      FiniteBag(Seq(key -> extractTerm(v)), locals.symbols.bestRealType(key.getType(locals.symbols)))
+
+    case Bags.EmptyBag(sort) => FiniteBag(Seq.empty, extractSort(sort))
+    case Bags.Union(e1, e2) => BagUnion(extractTerm(e1), extractTerm(e2))
+    case Bags.Intersection(e1, e2) => BagIntersection(extractTerm(e1), extractTerm(e2))
+    case Bags.Difference(e1, e2) => BagDifference(extractTerm(e1), extractTerm(e2))
+    case Bags.Multiplicity(e1, e2) => MultiplicityInBag(extractTerm(e1), extractTerm(e2))
+
+    case Bags.Insert(bag, es @ _*) =>
+      es.foldLeft(extractTerm(bag))((b,e) => BagAdd(b, extractTerm(e)))
 
     case Match(s, cases) =>
       val scrut = extractTerm(s)
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index 6778349a5e2f0c09350f41d9596c31b03bb0e9b1..e234c40a9f038eeadbaf4e97e2a35defb6f592b7 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -211,11 +211,19 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
       }.unzip
       Exists(param, params, toSMT(body)(bindings ++ newBindings))
 
-    case Application(caller, args) =>
-      SMTApplication(toSMT(caller), args.map(toSMT))
+    case Application(caller, args) => SMTApplication(toSMT(caller), args.map(toSMT))
 
-    case Assume(pred, body) =>
-      SMTAssume(toSMT(pred), toSMT(body))
+    case Assume(pred, body) => SMTAssume(toSMT(pred), toSMT(body))
+
+    case FiniteBag(elems, base) =>
+      elems.foldLeft(Bags.EmptyBag(declareSort(base))) { case (b, (k, v)) =>
+        Bags.Union(b, Bags.Singleton(toSMT(k), toSMT(v)))
+      }
+
+    case BagAdd(bag, elem) => Bags.Insert(toSMT(bag), toSMT(elem))
+    case MultiplicityInBag(elem, bag) => Bags.Multiplicity(toSMT(elem), toSMT(bag))
+    case BagIntersection(b1, b2) => Bags.Intersection(toSMT(b1), toSMT(b2))
+    case BagDifference(b1, b2) => Bags.Difference(toSMT(b1), toSMT(b2))
 
     case _ => super.toSMT(e)
   }