Allows more strictpure forms.

sireum · Oct 7, 2024 · b29283d · b29283d
1 parent dedd712
commit b29283d
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/Util.scala b/shared/src/main/scala/org/sireum/logika/Util.scala
@@ -2937,6 +2937,8 @@ object Util {
     if (mi.ast.isStrictPure && mi.ast.bodyOpt.nonEmpty) {
       mi.ast.bodyOpt.get.stmts match {
         case ISZ(stmt: AST.Stmt.Var, _: AST.Stmt.Return) => return stmt.initOpt
+        case ISZ(stmt: AST.Stmt.Return) => return Some(AST.Stmt.Expr(stmt.expOpt.get, stmt.attr))
+        case ISZ(stmt: AST.Stmt.Expr) => return Some(stmt)
         case stmts => halt(s"Infeasible: $stmts")
       }
     } else {