Added rewriting set definition and definitional/abstract strictpure m…

…ethod support.
sireum · Feb 7, 2024 · c256c29 · c256c29
1 parent 32b486d
commit c256c29
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/shared/src/main/scala/org/sireum/logika/Util.scala b/shared/src/main/scala/org/sireum/logika/Util.scala
@@ -2084,7 +2084,7 @@ object Util {
       val invs: ISZ[Info.Inv] = if (method.isHelper) ISZ[Info.Inv]() else logika.retrieveInvs(res.owner, res.isInObject)
       state = checkMethodPre(logika, smt2, cache, reporter, state, methodPosOpt, invs, requires)
       val stmts = method.bodyOpt.get.stmts
-      val (l, ss): (Logika, ISZ[State]) = if (method.purity == AST.Purity.StrictPure) {
+      val (l, ss): (Logika, ISZ[State]) = if (method.isStrictPure) {
         val stmt = stmts(0).asInstanceOf[AST.Stmt.Var]
         val spBody = stmt.initOpt.get
         val pos = spBody.asStmt.posOpt.get