diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index edd9e7dc87fd89f81640187204611266de513813..b37fd59a6775213ca8a0ec10f7760824010ca1e8 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -736,6 +736,13 @@ trait ASTExtractors {
       }
     }
 
+    object ExNotEquals {
+      def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
+        case Apply(Select(lhs, n), List(rhs)) if (n == nme.NE) => Some((lhs,rhs))
+        case _ => None
+      }
+    }
+
     object ExUMinus {
       def unapply(tree: Select): Option[Tree] = tree match {
         case Select(t, n) if (n == nme.UNARY_- && hasBigIntType(t)) => Some(t)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 67126c0d548f5acb16a0c14fb2bf356ca96a7a2b..86d7247ef9581c01146ee45942d66b506c33ea09 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1332,6 +1332,25 @@ trait CodeExtraction extends ASTExtractors {
         case ExBVUMinus(e)         => BVUMinus(extractTree(e))
         case ExBVNot(e)            => BVNot(extractTree(e))
 
+        case ExNotEquals(l, r) => {
+          val rl = extractTree(l)
+          val rr = extractTree(r)
+
+          (rl, rr) match {
+            case (IsTyped(_, rt), IsTyped(_, lt)) if isSubtypeOf(rt, lt) || isSubtypeOf(lt, rt) =>
+              Not(Equals(rl, rr))
+
+            case (IntLiteral(v), IsTyped(_, IntegerType)) =>
+              Not(Equals(InfiniteIntegerLiteral(v), rr))
+
+            case (IsTyped(_, IntegerType), IntLiteral(v)) =>
+              Not(Equals(rl, InfiniteIntegerLiteral(v)))
+
+            case (IsTyped(_, rt), IsTyped(_, lt)) =>
+              outOfSubsetError(tr, "Invalid comparison: (_: "+rt+") != (_: "+lt+")")
+          }
+        }
+
         case ExEquals(l, r) =>
           val rl = extractTree(l)
           val rr = extractTree(r)
@@ -1521,9 +1540,6 @@ trait CodeExtraction extends ASTExtractors {
 
               CaseClassSelector(cct, rec, fieldID)
 
-            case (a1, "!=", List(a2)) =>
-              Not(Equals(a1, a2))
-
             //BigInt methods
             case (IsTyped(a1, IntegerType), "+", List(IsTyped(a2, IntegerType))) =>
               Plus(a1, a2)
diff --git a/src/test/resources/regression/verification/purescala/error/NotEquals.scala b/src/test/resources/regression/verification/purescala/error/NotEquals.scala
new file mode 100644
index 0000000000000000000000000000000000000000..af102929ea13cf99780b463369a90cd59cbdd49c
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/error/NotEquals.scala
@@ -0,0 +1,8 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object NotEquals {
+
+  //should not pass front-end
+  def isDifferent(x: Int, s: String): Boolean = x != s
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Rational.scala b/src/test/resources/regression/verification/purescala/valid/Rational.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4979d970a53a73140733da599978f2d1184ceb1e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Rational.scala
@@ -0,0 +1,19 @@
+import leon.annotation._
+import leon.lang._
+
+object Rationals { 
+  // Represents n/d
+  case class Q(n: BigInt, d: BigInt)
+
+  def +(a: Q, b: Q) = {
+    require(isRational(a) && isRational(b))
+
+      Q(a.n*b.d + b.n*a.d, a.d*b.d)
+  } ensuring {
+    isRational(_)
+  }
+
+  //def isRational(a: Q) = a.d != 0
+  def isRational(a: Q) = a.d != 0
+
+}