Rewriting system.

sireum · Mar 2, 2024 · d8af16b · d8af16b
1 parent c001292
commit d8af16b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
@@ -2507,7 +2507,6 @@ object RewritingSystem {
             }
             return Some(r)
           }
-          return None()
         }
         val r = checkSubtyping()
         if (r.nonEmpty) {
@@ -2623,7 +2622,7 @@ object RewritingSystem {
             r = r :+ Rewriter.Pattern.Claim(name, F, isPermutative(c), localPatternSet, c)
           }
         }
-      case info: Info.RsVal => r = r ++ retrievePatterns(th, cache, info.ast.init, HashSet.empty)
+      case info: Info.RsVal => r = r ++ retrievePatterns(th, cache, info.ast.init, seen + name)
       case info: Info.Method =>
         if (info.ast.hasContract) {
           val context = info.name

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala
@@ -126,6 +126,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
             |
             |${(for (te <- trace) yield te.toST, "\n\n")}""")
       else None()
+
     val rwPc = Rewriter(if (logika.config.rwPar) logika.config.parCores else 1, logika.th,
       provenClaims, patterns, methodPatterns, logika.config.rwTrace, logika.config.rwEvalTrace, F, ISZ())
     val stepClaim = RewritingSystem.translateExp(logika.th, F, step.claim)
@@ -238,7 +239,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
           st"""Could not match:
               |  ${stepClaim.prettyST}
               |
-              |After ${if (isEval) "evaluating" else "rewriting"}$fromOpt to:
+              |After attempting to ${if (isEval) "evaluate" else "rewrite"}$fromOpt to:
               |  ${rwClaim.prettyST}
               |
               |$simplTraceOpt