Disabled automatic and-elimination in manual mode.

sireum · Mar 20, 2024 · 69ae3d9 · 69ae3d9
1 parent f29f25b
commit 69ae3d9
Showing 1 changed file with 10 additions and 8 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala
@@ -379,14 +379,16 @@ object AutoPlugin {
                     return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
                   case _ =>
                 }
-                for (pc <- normPathConditions.elements) {
-                  AutoPlugin.detectInPc(logika.th, claimNorm, step.claim, conjuncts(pc), pathConditions) match {
-                    case Some(acceptMsg) =>
-                      if (logika.config.detailedInfo) {
-                        reporter.inform(pos, Logika.Reporter.Info.Kind.Verified, acceptMsg.render)
-                      }
-                      return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
-                    case _ =>
+                if (logika.config.isAuto) {
+                  for (pc <- normPathConditions.elements) {
+                    AutoPlugin.detectInPc(logika.th, claimNorm, step.claim, conjuncts(pc), pathConditions) match {
+                      case Some(acceptMsg) =>
+                        if (logika.config.detailedInfo) {
+                          reporter.inform(pos, Logika.Reporter.Info.Kind.Verified, acceptMsg.render)
+                        }
+                        return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+                      case _ =>
+                    }
                   }
                 }
                 reporter.error(posOpt, Logika.kind,