diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
index 90cc0822..ba3e6949 100644
--- a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
+++ b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
@@ -2547,7 +2547,7 @@ object RewritingSystem {
               addContract(label, cas.requires, cas.ensures)
             }
         }
-      } else {
+      } else if (minfo.ast.isStrictPure) {
         r = r :+ methodPatternOf(th, cache, minfo)
       }
       return r