Made Tipeable.

sireum · Sep 14, 2023 · 1db9387 · 1db9387
1 parent ea008cb
commit 1db9387
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala
@@ -293,9 +293,10 @@ import InceptionPlugin._
         reporter.error(step.claim.posOpt, Logika.kind, st"Could not derive the stated claim from $id's $conc${if (ensures.size > 1) "s" else ""}".render)
         return emptyResult
       }
-      val (status, nextFresh, claims, claim) = if (logika.config.mode == Config.VerificationMode.SymExe)
-        logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
-      else logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+      val (status, nextFresh, claims, claim): (B, Z, ISZ[State.Claim], State.Claim) =
+        if (logika.config.mode == Config.VerificationMode.SymExe)
+          logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
+        else logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
       if (status && logika.config.detailedInfo) {
         val (ePos, ensure, tensure) = ePosExpTExpOpt.get
         evidence = evidence :+