Test better triggers for maps

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -4271,6 +4271,7 @@ object Desugar {
         } yield underlyingType(dright.typ) match {
           case _: in.SequenceT | _: in.SetT => in.Contains(dleft, dright)(src)
           case _: in.MultisetT => in.LessCmp(in.IntLit(0)(src), in.Contains(dleft, dright)(src))(src)
+          case _: in.MapT => in.Contains(dleft, dright)(src)
           case t => violation(s"expected a sequence or (multi)set type, but got $t")
         }
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -139,6 +139,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
       case PIn(left, right) => isExpr(left).out ++ isExpr(right).out ++ {
         underlyingType(exprType(right)) match {
           case t : GhostCollectionType => ghostComparableTypes.errors(exprType(left), t.elem)(expr)
+          case t : MapT => ghostComparableTypes.errors(exprType(left), t.key)(expr)
           case _ : AdtT => noMessages
           case t => error(right, s"expected a ghost collection, but got $t")
         }

src/main/scala/viper/gobra/reporting/VerifierError.scala

@@ -299,11 +299,6 @@ case class InsufficientPermissionToRangeExpressionError(info: Source.Verifier.In
   override def localMessage: String = s"Range expression should be immutable inside the loop body"
 }
 
-case class MapMakePreconditionError(info: Source.Verifier.Info) extends VerificationError {
-  override def localId: String = "make_precondition_error"
-  override def localMessage: String = s"The provided length to ${info.origin.tag.trim} might be negative"
-}
-
 case class ShiftPreconditionError(info: Source.Verifier.Info) extends VerificationError {
   override def localId: String = "shift_precondition_error"
   override def localMessage: String = s"The shift count in ${info.origin.tag.trim} might be negative"
@@ -505,6 +500,11 @@ case class SpecNotImplementedByClosure(info: Verifier.Info, closure: String, spe
   override def message: String = s"$closure might not implement $spec."
 }
 
+case class MapMakePreconditionFailed(info: Source.Verifier.Info) extends VerificationErrorReason {
+  override def id: String = "make_precondition_error"
+  override def message: String = s"The provided length to ${info.origin.tag.trim} might be negative"
+}
+
 sealed trait VerificationErrorClarification {
   def message: String
   override def toString: String = message