Fixed Smt2 justification sub-proof handling.

sireum · Dec 4, 2024 · fafffad · fafffad
1 parent b6ebab9
commit fafffad
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/Smt2Plugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/Smt2Plugin.scala
@@ -85,7 +85,7 @@ import org.sireum.logika.{Logika, Smt2, Smt2Config, Smt2Query, State, StepProofC
             r = r + spc.stepNo ~> (T, claim)
           case spc: StepProofContext.SubProof =>
             val claims: ISZ[AST.Exp] = for (p <- computeProvenClaims(spc.spcs).entries) yield p._2._2
-            val claim = AST.Util.bigImply(F, ISZ(spc.assumption, AST.Util.bigAnd(claims, spc.stepNo.posOpt)), spc.stepNo.posOpt)
+            val claim = AST.Util.bigImply(T, ISZ(spc.assumption, AST.Util.bigAnd(claims, spc.stepNo.posOpt)), spc.stepNo.posOpt)
             r = r + spc.stepNo ~> (F, claim)
           case spc: StepProofContext.FreshSubProof =>
             val claims: ISZ[AST.Exp] = for (p <- computeProvenClaims(spc.spcs).entries) yield p._2._2
@@ -105,7 +105,7 @@ import org.sireum.logika.{Logika, Smt2, Smt2Config, Smt2Query, State, StepProofC
               params = params :+ AST.Exp.Fun.Param(Some(p.id), p.tipeOpt, p.tipeOpt.get.typedOpt)
             }
             val claim = AST.Exp.QuantType(F, AST.Exp.Fun(spc.context, params,
-              AST.Stmt.Expr(AST.Util.bigImply(F, ISZ(spc.assumption, AST.Util.bigAnd(claims, spc.stepNo.posOpt)),
+              AST.Stmt.Expr(AST.Util.bigImply(T, ISZ(spc.assumption, AST.Util.bigAnd(claims, spc.stepNo.posOpt)),
                 spc.stepNo.posOpt), tattr), tattr), AST.Attr(spc.stepNo.posOpt))
             r = r + spc.stepNo ~> (F, claim)
         }