Fixed Auto and Smt2 justifications.

Author: robby-phd

shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala

@@ -473,7 +473,7 @@ object AutoPlugin {
       if (s2.ok) {
         val s3 = checkValid(smt2, s2, State.Claim.Prop(T, conclusion))
         if (s3.ok) {
-          return logika.evalAssume(smt2, cache, T, "", state, step.claim, step.id.posOpt, reporter)._1
+          return state(claims = state.claims ++ ops.ISZOps(s3.claims).slice(s0.claims.size, s3.claims.size), nextFresh = s3.nextFresh)
         }
       }
       return err
@@ -502,7 +502,7 @@ object AutoPlugin {
       if (s6.ok) {
         val r = checkValid(psmt2, s6, State.Claim.Prop(T, conclusion))
         if (r.ok) {
-          return logika.evalAssume(smt2, cache, T, "", state, step.claim, step.id.posOpt, reporter)._1
+          return state(claims = state.claims ++ ops.ISZOps(r.claims).slice(s1.claims.size, r.claims.size), nextFresh = r.nextFresh)
         }
       }
       return err

shared/src/main/scala/org/sireum/logika/plugin/Smt2Plugin.scala

@@ -157,12 +157,12 @@ import org.sireum.logika.{Logika, Smt2, Smt2Config, Smt2Query, State, StepProofC
       if (s6.ok) {
         val s7 = checkValid(s6, conclusion)
         if (s7.ok) {
-          return logika.evalAssume(smt2, cache, T, "", state, step.claim, step.id.posOpt, reporter)._1
+          return s7(claims = state.claims ++ ops.ISZOps(s7.claims).slice(s0.claims.size, s7.claims.size), nextFresh = s7.nextFresh)
         }
       }
       return err
     } else {
-      val (suc, m) = state.unconstrainedClaims
+      val (suc, _) = state.unconstrainedClaims
       var s0 = suc
       var ok = T
       for (arg <- just.witnesses) {
@@ -184,7 +184,7 @@ import org.sireum.logika.{Logika, Smt2, Smt2Config, Smt2Query, State, StepProofC
       if (s6.ok) {
         val s7 = checkValid(s6, conclusion)
         if (s7.ok) {
-          return logika.evalAssume(smt2, cache, T, "", state, step.claim, step.id.posOpt, reporter)._1
+          return s7(claims = state.claims ++ ops.ISZOps(s7.claims).slice(s0.claims.size, s7.claims.size), nextFresh = s7.nextFresh)
         }
       }
       return err