diff --git a/src/main/scala/leon/utils/IncrementalBijection.scala b/src/main/scala/leon/utils/IncrementalBijection.scala
index 1b57644b690744611335935b33a28ebdcca66d14..18f568ee2c5f3c9daea256aed8a165e4d5dbb99a 100644
--- a/src/main/scala/leon/utils/IncrementalBijection.scala
+++ b/src/main/scala/leon/utils/IncrementalBijection.scala
@@ -75,6 +75,12 @@ class IncrementalBijection[A,B] extends Bijection[A,B] with IncrementalState {
     b2aStack.pop()
   }
 
+  /** Return an IncrementalBijection in the other direction
+    *
+    * The returned bijection remains linked to the original, which
+    * means that any push/pop on any of the two bijection should be
+    * visible in both, same goes for new mappings added.
+    */
   override def swap: IncrementalBijection[B, A] = new IncrementalBijection[B, A] {
     override protected val a2b = IncrementalBijection.this.b2a
     override protected val b2a = IncrementalBijection.this.a2b
diff --git a/src/test/scala/leon/unit/utils/IncrementalBijectionSuite.scala b/src/test/scala/leon/unit/utils/IncrementalBijectionSuite.scala
index fe316af1dd12dcda2ee9f062aa8b373668a6833a..618e8094b6515df5c980531a508581923197620a 100644
--- a/src/test/scala/leon/unit/utils/IncrementalBijectionSuite.scala
+++ b/src/test/scala/leon/unit/utils/IncrementalBijectionSuite.scala
@@ -118,4 +118,178 @@ class IncrementalBijectionSuite extends FunSuite {
     assert(b.getA(33) === Some(12))
   }
 
+  test("swap simple bijection is working") {
+    val b = new IncrementalBijection[Int, Int]
+    b += (1 -> 10)
+    b += (2 -> 20)
+    val c = b.swap
+
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === Some(20))
+    assert(b.getB(10) === None)
+    assert(b.getB(20) === None)
+    assert(b.getA(10) === Some(1))
+    assert(b.getA(20) === Some(2))
+    assert(b.getA(1) === None)
+    assert(b.getA(2) === None)
+
+    assert(c.getB(1) === None)
+    assert(c.getB(2) === None)
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === Some(2))
+    assert(c.getA(10) === None)
+    assert(c.getA(20) === None)
+    assert(c.getA(1) === Some(10))
+    assert(c.getA(2) === Some(20))
+  }
+
+  test("updates to swapped bijection are visible in original") {
+    val b = new IncrementalBijection[Int, Int]
+    b += (1 -> 10)
+    val c = b.swap
+    c += (20 -> 2)
+
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === Some(20))
+    assert(b.getB(10) === None)
+    assert(b.getB(20) === None)
+    assert(b.getA(10) === Some(1))
+    assert(b.getA(20) === Some(2))
+    assert(b.getA(1) === None)
+    assert(b.getA(2) === None)
+
+    assert(c.getB(1) === None)
+    assert(c.getB(2) === None)
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === Some(2))
+    assert(c.getA(10) === None)
+    assert(c.getA(20) === None)
+    assert(c.getA(1) === Some(10))
+    assert(c.getA(2) === Some(20))
+  }
+
+  test("swap bijection then overrides some mappings") {
+    val b = new IncrementalBijection[Int, Int]
+    b += (1 -> 10)
+    b += (2 -> 20)
+    val c = b.swap
+    b += (1 -> 30)
+
+    assert(b.getB(1) === Some(30))
+    assert(b.getB(2) === Some(20))
+    assert(b.getB(10) === None)
+    assert(b.getB(20) === None)
+    assert(b.getB(30) === None)
+    assert(b.getA(10) === None)
+    assert(b.getA(20) === Some(2))
+    assert(b.getA(30) === Some(1))
+    assert(b.getA(1) === None)
+    assert(b.getA(2) === None)
+
+    assert(c.getB(1) === None)
+    assert(c.getB(2) === None)
+    assert(c.getB(10) === None)
+    assert(c.getB(20) === Some(2))
+    assert(c.getB(30) === Some(1))
+    assert(c.getA(10) === None)
+    assert(c.getA(20) === None)
+    assert(c.getA(30) === None)
+    assert(c.getA(1) === Some(30))
+    assert(c.getA(2) === Some(20))
+  }
+
+  test("Push on a swapped bijection also pushes to original") {
+    val b = new IncrementalBijection[Int, Int]
+    b += (1 -> 10)
+    val c = b.swap
+    c.push()
+    c += (20 -> 2)
+
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === Some(20))
+    assert(b.getB(10) === None)
+    assert(b.getB(20) === None)
+    assert(b.getA(10) === Some(1))
+    assert(b.getA(20) === Some(2))
+    assert(b.getA(1) === None)
+    assert(b.getA(2) === None)
+
+    assert(c.getB(1) === None)
+    assert(c.getB(2) === None)
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === Some(2))
+    assert(c.getA(10) === None)
+    assert(c.getA(20) === None)
+    assert(c.getA(1) === Some(10))
+    assert(c.getA(2) === Some(20))
+  }
+
+  test("Pop on a swapped bijection also pop to original") {
+    val b = new IncrementalBijection[Int, Int]
+    b += (1 -> 10)
+    val c = b.swap
+    c.push()
+    c += (20 -> 2)
+
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === Some(20))
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === Some(2))
+
+    c.pop()
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === None)
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === None)
+  }
+
+  test("push/pop on a swapped bijection stays consistent") {
+    val b = new IncrementalBijection[Int, Int]
+    b += (1 -> 10)
+    val c = b.swap
+    c.push()
+    c += (20 -> 2)
+
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === Some(20))
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === Some(2))
+
+    b.pop()
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === None)
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === None)
+
+    c += (30 -> 3)
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === None)
+    assert(b.getB(3) === Some(30))
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === None)
+    assert(c.getB(30) === Some(3))
+  }
+
+  test("overriding mapping in swap bijection is consistent after a pop") {
+    val b = new IncrementalBijection[Int, Int]
+    b += (1 -> 10)
+    b += (2 -> 20)
+    val c = b.swap
+    c.push()
+    c += (30 -> 1)
+
+    assert(b.getB(1) === Some(30))
+    assert(b.getB(2) === Some(20))
+    assert(c.getB(10) === None)
+    assert(c.getB(20) === Some(2))
+    assert(c.getB(30) === Some(1))
+
+    c.pop()
+    assert(b.getB(1) === Some(10))
+    assert(b.getB(2) === Some(20))
+    assert(c.getB(10) === Some(1))
+    assert(c.getB(20) === Some(2))
+    assert(c.getB(30) === None)
+  }
+
 }