diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 4b960a043d2baf82b96a05a7133bf05faf6fafe6..6a4981997d0032f16011f3ca7189d632aba331e5 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -280,7 +280,27 @@ object Constructors {
     if (a == b && isDeterministic(a)) {
       BooleanLiteral(true)
     } else  {
-      Equals(a, b)
+      (a, b) match {
+        case (a: Literal[_], b: Literal[_]) =>
+          if (a.value == b.value) {
+            BooleanLiteral(true)
+          } else {
+            BooleanLiteral(false)
+          }
+
+        case _ =>
+          Equals(a, b)
+      }
+    }
+  }
+
+  def assertion(c: Expr, err: Option[String], res: Expr) = {
+    if (c == BooleanLiteral(true)) {
+      res
+    } else if (c == BooleanLiteral(false)) {
+      Error(res.getType, err.getOrElse("Assertion failed"))
+    } else {
+      Assert(c, err, res)
     }
   }
 
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 418da12eb62e1fb1ead33bc0317da9ceb9662e28..a2ba463a6519a4c10e224c583263b805b4f660d7 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -42,34 +42,34 @@ object InjectAsserts extends SimpleLeonPhase[Program, Program] {
                      ).setPos(e))
 
         case e @ Division(_, d)  =>
-          Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+          Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
                       Some("Division by zero"),
                       e
                      ).setPos(e))
         case e @ Remainder(_, d)  =>
-          Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+          Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
                       Some("Remainder by zero"),
                       e
                      ).setPos(e))
         case e @ Modulo(_, d)  =>
-          Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
+          Some(assertion(not(equality(d, InfiniteIntegerLiteral(0))),
                       Some("Modulo by zero"),
                       e
                      ).setPos(e))
 
         case e @ BVDivision(_, d)  =>
-          Some(Assert(Not(Equals(d, IntLiteral(0))),
+          Some(assertion(not(equality(d, IntLiteral(0))),
                       Some("Division by zero"),
                       e
                      ).setPos(e))
         case e @ BVRemainder(_, d)  =>
-          Some(Assert(Not(Equals(d, IntLiteral(0))),
+          Some(assertion(not(equality(d, IntLiteral(0))),
                       Some("Remainder by zero"),
                       e
                      ).setPos(e))
 
         case e @ RealDivision(_, d)  =>
-          Some(Assert(Not(Equals(d, FractionalLiteral(0, 1))),
+          Some(assertion(not(equality(d, FractionalLiteral(0, 1))),
                       Some("Division by zero"),
                       e
                      ).setPos(e))