InjectAssert should not insert trivial asserts

Improve equality to detect equalities between literals

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)
     }
   }
 

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))