Do not treat inline methods or functions as ghost

frontends/benchmarks/dotty-specific/invalid/i1479.scala

@@ -0,0 +1,15 @@
+object i1479 {
+  case class MyClass(var x: BigInt, var y: BigInt, var isValid: Boolean = true) {
+    require(!isValid || x <= y)
+  }
+
+  inline def changeMyClass(m: MyClass)(inline body: => Unit): Unit =
+    m.isValid = false // Note that we may not have mc.x <= mc.y so this is invalid
+    body
+    m.isValid = true
+
+  def inc(m: MyClass): Unit =
+    changeMyClass(m):
+      m.x += 1
+      m.y += 1
+}

frontends/benchmarks/dotty-specific/valid/i1479.scala

@@ -0,0 +1,17 @@
+object i1479 {
+  case class MyClass(var x: BigInt, var y: BigInt, var isValid: Boolean = true) {
+    require(!isValid || x <= y)
+  }
+
+  inline def changeMyClass(m: MyClass)(inline body: => Unit): Unit =
+    require(m.isValid)
+    m.isValid = false
+    body
+    m.isValid = true
+
+  def inc(m: MyClass): Unit =
+    require(m.isValid)
+    changeMyClass(m):
+      m.x += 1
+      m.y += 1
+}

frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala

@@ -62,7 +62,7 @@ trait ASTExtractors {
     if (sym eq NoSymbol)
       return Seq.empty
 
-    val erased = if (sym.isEffectivelyErased) Seq(("ghost", Seq.empty[tpd.Tree])) else Seq()
+    val erased = if (sym.isEffectivelyErased && !(sym is Inline)) Seq(("ghost", Seq.empty[tpd.Tree])) else Seq()
     val selfs = sym.annotations
     val owners =
       if (ignoreOwner) List.empty[Annotation]