From 69ae3d9e2dab0186c9d2a02656cec8e075dbceae Mon Sep 17 00:00:00 2001 From: Robby Date: Wed, 20 Mar 2024 08:29:02 -0500 Subject: [PATCH] Disabled automatic and-elimination in manual mode. --- .../org/sireum/logika/plugin/AutoPlugin.scala | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 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 index a60ce14c..1108adf6 100644 --- 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,