diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index c655799b929..7065c0b77e3 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -3,7 +3,7 @@ name: Weekly Builds of KeY on: workflow_dispatch: schedule: - - cron: '0 5 * * 1' # every monday morning + - cron: '0 5 * * 1' # every monday morning permissions: contents: write @@ -12,7 +12,6 @@ permissions: env: JAVA_VERSION: 21 - jobs: build: runs-on: ubuntu-latest @@ -24,84 +23,51 @@ jobs: java-version: ${{ env.JAVA_VERSION }} distribution: 'temurin' cache: 'gradle' + gpg-private-key: ${{ secrets.GPG_PRIVATE_KEY }} + gpg-passphrase: ${{ secrets.GPG_PASSPHRASE }} - name: Setup Gradle uses: gradle/actions/setup-gradle@v5 - name: Build with Gradle - run: ./gradlew --parallel assemble + run: ./gradlew --parallel assemble javadoc alldoc - doc: - needs: [build] - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v6 - - name: Set up JDK ${{ env.JAVA_VERSION }} - uses: actions/setup-java@v5 + - name: Upload ShadowJar + uses: actions/upload-artifact@v7 with: - java-version: ${{ env.JAVA_VERSION }} - distribution: 'temurin' - cache: 'gradle' - - - name: Setup Gradle - uses: gradle/actions/setup-gradle@v5 - - - name: Build Documentation with Gradle - run: ./gradlew alldoc + name: shadowjars + path: "*/build/libs/*-exe.jar" + retention-days: 1 - name: Package run: tar cvf key-javadoc.tar.xz build/docs/javadoc - deploy: - needs: [build, doc] - runs-on: ubuntu-latest - steps: - name: Upload Javadoc uses: actions/upload-artifact@v7 with: name: javadoc - path: "javadoc.tar.xz" - - - name: Upload ShadowJar - uses: actions/upload-artifact@v7 - with: - name: shadowjars - path: "*/build/libs/*-exe.jar" + path: "key-javadoc.tar.xz" + retention-days: 1 - name: Delete previous nightly release continue-on-error: true env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} run: | - gh release delete nightly --yes --cleanup-tag + gh release delete KEY-2.12.4-Release-Candidate --yes --cleanup-tag - name: Create nightly release id: create_release env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - run: | - gh release create --generate-notes --title "Nightly Release" \ + run: | + gh release create --generate-notes --title "KeY 2.12.4 Pre-Release" \ --prerelease --notes-start-tag KEY-2.12.3 \ - nightly key.ui/build/libs/key-*-exe.jar - - deploy-maven: - needs: [ build, doc ] - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v6 - - name: Set up JDK ${{ env.JAVA_VERSION }} - uses: actions/setup-java@v5 - with: - java-version: ${{ env.JAVA_VERSION }} - distribution: 'temurin' - cache: 'gradle' - - - name: Setup Gradle - uses: gradle/actions/setup-gradle@v5 + KEY-2.12.4-Release-Candidate key.ui/build/libs/key-*-exe.jar key-javadoc.tar.xz + - run: export GPG_TTY=$(tty) - name: Upload to SNAPSHOT repository - run: ./gradlew publishMavenJavaPublicationToKEYLABRepository + run: ./gradlew --parallel publishMavenJavaPublicationToKEYLABRepository env: BUILD_NUMBER: "SNAPSHOT" GITLAB_DEPLOY_TOKEN: ${{ secrets.GITLAB_DEPLOY_TOKEN }} - diff --git a/LICENSE.TXT b/LICENSE.TXT index dbafedb51f2..1a701bdf921 100644 --- a/LICENSE.TXT +++ b/LICENSE.TXT @@ -3,7 +3,7 @@ Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany Universitaet Koblenz-Landau, Germany Chalmers University of Technology, Sweden - Copyright (C) 2011-2019 Karlsruhe Institute of Technology, Germany + Copyright (C) 2011-2026 Karlsruhe Institute of Technology, Germany Technical University Darmstadt, Germany Chalmers University of Technology, Sweden diff --git a/README.md b/README.md index e9d834c472a..99cb4dc561c 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ For more information, refer to * [Verification of `java.util.IdentityHashMap`](https://doi.org/10.1007/978-3-031-07727-2_4), * [Google Award for analysing a bug in `LinkedList`](https://www.key-project.org/2023/07/23/cwi-researchers-win-google-award-for-finding-a-bug-in-javas-linkedlist-using-key/) -The current version of KeY is 2.12.2, licensed under GPL v2. +The current version of KeY is 2.12.4, licensed under GPL v2. Feel free to use the project templates to get started using KeY: @@ -83,7 +83,7 @@ Assuming you are in the directory of this README file, you can create a runnable # Developing KeY -* Quality is automatically assessed using [SonarQube](https://sonarqube.org) on each pull request. +* Quality is automatically assessed on each pull request. The results of the assessments (pass/fail) can be inspected in the checks section of the PR. The rules and quality gate are maintained by Alexander Weigl @@ -113,7 +113,7 @@ This is the KeY project - Integrated Deductive Software Design Copyright (C) 2001-2011 Universität Karlsruhe, Germany Universität Koblenz-Landau, Germany and Chalmers University of Technology, Sweden -Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany +Copyright (C) 2011-2026 Karlsruhe Institute of Technology, Germany Technical University Darmstadt, Germany Chalmers University of Technology, Sweden diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java index 78106d81b4a..8d1418a2327 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodReference.java @@ -355,7 +355,8 @@ public void visit(Visitor v) { public KeYJavaType getKeYJavaType(Services services, ExecutionContext ec) { IProgramMethod meth = method(services, determineStaticPrefixType(services, ec), ec); if (meth == null) { - return ec.getTypeReference().getKeYJavaType(); + throw new IllegalStateException( + "Could not determine type for method " + name.toString()); } return meth.getReturnType(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java index 19426a84d81..4d187845b04 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java @@ -157,14 +157,38 @@ public String newName(String baseName, NamespaceSet localNamespace) { return savedName.toString(); } + final String result = freeName(baseName, localNamespace, null); + + services.getNameRecorder().addProposal(new Name(result)); + + return result; + } + + /** + * Returns the first name out of {@code baseName, baseName_0, baseName_1, ...} that is neither + * present in {@code localNamespace} nor contained in {@code taken}. + *

+ * This is the side-effect-free core of the "find a fresh name" loop: it neither touches the + * name recorder nor advances any counter, + * so the result depends only on the supplied namespaces and the {@code taken} set. That makes + * it safe to call from contexts that run during (speculative) taclet matching, where a + * mutable side effect would render the result non-deterministic across proof reloads (see + * {@link de.uka.ilkd.key.rule.conditions.NewLocalVarsCondition} / issue #3834). + * + * @param baseName the base name (prefix) + * @param localNamespace the namespaces to check for collisions + * @param taken additional names to avoid (may be {@code null}); useful when several fresh + * names are generated before any of them is registered in the namespaces + * @return a name not occurring in {@code localNamespace} or {@code taken} + */ + public static String freeName(String baseName, NamespaceSet localNamespace, + java.util.Set taken) { int i = 0; String result = baseName; - while (localNamespace.lookup(new Name(result)) != null) { + while (localNamespace.lookup(new Name(result)) != null + || (taken != null && taken.contains(result))) { result = baseName + "_" + i++; } - - services.getNameRecorder().addProposal(new Name(result)); - return result; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java index f1c099e78e9..96a1364a2f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java @@ -380,7 +380,14 @@ protected ProgramElementName getNameProposalForSchemaVariable(String basename, collision = false; for (String previousProposal : previousProposals) { if (previousProposal.equals(result.toString())) { - result = createName(basename, ++cnt, null); + cnt += 1; + result = createName(basename, cnt, null); + + while (services.getNamespaces().lookupLogicSymbol(result) != null) { + cnt += 1; + result = createName(basename, cnt, null); + } + collision = true; break; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java index a87c562263d..4f77b699a9a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/VariableNameProposer.java @@ -138,7 +138,7 @@ private String getNameProposalForSkolemTermVariable(String name, Services servic name = basename + cnt; l_name = new Name(name); cnt++; - } while (nss.lookup(l_name) != null && !previousProposals.contains(name)); + } while (nss.lookup(l_name) != null || previousProposals.contains(name)); return name; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/UrlRuleSource.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/UrlRuleSource.java index f921f77d6e3..5144c389717 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/UrlRuleSource.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/UrlRuleSource.java @@ -61,11 +61,11 @@ public Path file() { try { return Paths.get(uri); } catch (FileSystemNotFoundException e) { - URI rootFs = URI.create(StringUtil.takeUntil(uri.toString(), "\\!")); - String internal = StringUtil.takeAfter(uri.toString(), "\\!"); - try (FileSystem zipfs = FileSystems.newFileSystem(rootFs, new HashMap<>())) { - return zipfs.getPath(internal); - } + URI rootFs = URI.create(StringUtil.takeUntil(uri.toString(), "!")); + String internal = StringUtil.takeAfter(uri.toString(), "!"); + // keep the file system open. + FileSystem zipfs = FileSystems.newFileSystem(rootFs, new HashMap<>()); + return zipfs.getPath(internal); } } catch (URISyntaxException | IOException e) { throw new RuntimeException(e); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java index 1f1203c3e5e..ed5b676f78e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java @@ -4,7 +4,9 @@ package de.uka.ilkd.key.rule.conditions; import java.util.ArrayList; +import java.util.HashSet; import java.util.List; +import java.util.Set; import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.Services; @@ -16,6 +18,8 @@ import de.uka.ilkd.key.java.declaration.VariableSpecification; import de.uka.ilkd.key.java.reference.TypeRef; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.ProgramElementName; +import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.util.MiscTools; @@ -85,9 +89,18 @@ public MatchResultInfo check(SchemaVariable var, SyntaxElement instCandidate, ImmutableList updatesBefore = ImmutableSLList.nil(); ImmutableList updatesFrame = ImmutableSLList.nil(); var tb = services.getTermBuilder(); + // Names of "before" variables generated within this single application; needed because + // the new variables are not yet registered in the namespaces while we build them. + final Set reserved = new HashSet<>(); for (var v : vars) { - final var newName = - services.getVariableNamer().getTemporaryNameProposal(v.name() + "_before"); + // Deterministically derive a unique name from the current proof state instead of + // using getVariableNamer().getTemporaryNameProposal(), which appends a '#'-index + // taken from a proof-global counter. That counter is advanced as a side effect of + // (speculative) taclet matching, so the number of increments differs between a + // freshly created proof and a reloaded/pruned-and-reapplied one. The resulting name + // mismatch (e.g. k_before#0 vs. k_before#1) breaks the slicing mechanism, which + // relies on formula equivalence across reloads. See issue #3834. + final var newName = uniqueBeforeName(v.name() + "_before", services, reserved); KeYJavaType type = v.getKeYJavaType(); var locVar = new LocationVariable(newName, type); var spec = new VariableSpecification(locVar); @@ -109,6 +122,28 @@ public MatchResultInfo check(SchemaVariable var, SyntaxElement instCandidate, .add(updateFrameSV, tb.parallel(updatesFrame), services)); } + /** + * Produces a fresh {@link ProgramElementName} for a "before" variable that is deterministic + * w.r.t. the current proof state. The name is unique with respect to all current namespaces of + * {@code services} as well as the names already handed out within the current rule application + * ({@code reserved}). Unlike + * {@link de.uka.ilkd.key.logic.VariableNamer#getTemporaryNameProposal(String)}, this does not + * depend on a mutable proof-global counter, so it stays stable across proof reloads and + * prune/reapply cycles (issue #3834). + * + * @param basename the desired base name, e.g. {@code "k_before"} + * @param services the services whose namespaces are consulted for collisions + * @param reserved names already used within the current application; the chosen name is added + * @return a fresh, collision-free name + */ + private static ProgramElementName uniqueBeforeName(String basename, Services services, + Set reserved) { + final String candidate = + TermBuilder.freeName(basename, services.getNamespaces(), reserved); + reserved.add(candidate); + return new ProgramElementName(candidate); + } + @Override public String toString() { return "\\newLocalVars(" + varDeclsSV + ", " + updateBeforeSV + ", " + updateFrameSV + ", " diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java index 297b663ad3c..624237c6f03 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java @@ -33,7 +33,6 @@ */ public class SwitchToIf extends ProgramTransformer { - private boolean noNewBreak = true; /** * creates a switch-to-if ProgramTransformer @@ -49,6 +48,7 @@ public ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations insts) { Switch sw = (Switch) pe; + VariableNamer varNamer = services.getVariableNamer(); Label l = varNamer.getTemporaryNameProposal("_l"); @@ -62,7 +62,8 @@ public ProgramElement[] transform(ProgramElement pe, Services services, Statement s = KeYJavaASTFactory.declare(name, sw.getExpression().getKeYJavaType(services, ec)); - sw = changeBreaks(sw, newBreak); + final var changeBreakResult = changeBreaks(sw, newBreak, true); + sw = (Switch) changeBreakResult.result; Statement currentBlock = null; for (int i = sw.getBranchCount() - 1; 0 <= i; i--) { if (sw.getBranchAt(i) instanceof Default) { @@ -96,7 +97,7 @@ public ProgramElement[] transform(ProgramElement pe, Services services, // empty switch of primitive type, the expression can still have side-effects result = KeYJavaASTFactory.block(s, KeYJavaASTFactory.assign(exV, sw.getExpression())); } - if (noNewBreak) { + if (changeBreakResult.noNewBreak) { return new ProgramElement[] { result }; } else { return new ProgramElement[] { @@ -130,69 +131,103 @@ private If mkIfNullCheck(Services services, ProgramVariable var, Statement elseB /** * Replaces all breaks in sw, whose target is sw, with b */ - private Switch changeBreaks(Switch sw, Break b) { + private ChangeBreakResult changeBreaks(Switch sw, Break b, boolean noNewBreak) { int n = sw.getBranchCount(); Branch[] branches = new Branch[n]; for (int i = 0; i < n; i++) { - branches[i] = (Branch) recChangeBreaks(sw.getBranchAt(i), b); + final var branch = recChangeBreaks(sw.getBranchAt(i), b, noNewBreak); + noNewBreak = branch.noNewBreak; + branches[i] = (Branch) branch.result; } - return KeYJavaASTFactory.switchBlock(sw.getExpression(), branches); + return new ChangeBreakResult(KeYJavaASTFactory.switchBlock(sw.getExpression(), branches), + noNewBreak); } - private ProgramElement recChangeBreaks(ProgramElement p, Break b) { + private ChangeBreakResult recChangeBreaks(ProgramElement p, Break b, boolean noNewBreak) { if (p == null) { return null; } if (p instanceof Break && ((Break) p).getLabel() == null) { - noNewBreak = false; - return b; + return new ChangeBreakResult(b, false); } if (p instanceof Branch) { Statement[] s = new Statement[((Branch) p).getStatementCount()]; for (int i = 0; i < ((Branch) p).getStatementCount(); i++) { - s[i] = (Statement) recChangeBreaks(((Branch) p).getStatementAt(i), b); + final ChangeBreakResult r = + recChangeBreaks(((Branch) p).getStatementAt(i), b, noNewBreak); + noNewBreak = r.noNewBreak; + s[i] = (Statement) r.result; } if (p instanceof Case) { - return KeYJavaASTFactory.caseBlock(((Case) p).getExpression(), s); + return new ChangeBreakResult( + KeYJavaASTFactory.caseBlock(((Case) p).getExpression(), s), + noNewBreak); } if (p instanceof Default) { - return KeYJavaASTFactory.defaultBlock(s); + return new ChangeBreakResult( + KeYJavaASTFactory.defaultBlock(s), + noNewBreak); } if (p instanceof Catch) { - return KeYJavaASTFactory.catchClause(((Catch) p).getParameterDeclaration(), s); + return new ChangeBreakResult( + KeYJavaASTFactory.catchClause(((Catch) p).getParameterDeclaration(), s), + noNewBreak); } if (p instanceof Finally) { - return KeYJavaASTFactory.finallyBlock(s); + return new ChangeBreakResult(KeYJavaASTFactory.finallyBlock(s), + noNewBreak); } if (p instanceof Then) { - return KeYJavaASTFactory.thenBlock(s); + return new ChangeBreakResult( + KeYJavaASTFactory.thenBlock(s), + noNewBreak); } if (p instanceof Else) { - return KeYJavaASTFactory.elseBlock(s); + return new ChangeBreakResult( + KeYJavaASTFactory.elseBlock(s), + noNewBreak); } } if (p instanceof If) { - return KeYJavaASTFactory.ifElse(((If) p).getExpression(), - (Then) recChangeBreaks(((If) p).getThen(), b), - (Else) recChangeBreaks(((If) p).getElse(), b)); + final ChangeBreakResult then = recChangeBreaks(((If) p).getThen(), b, noNewBreak); + noNewBreak = then.noNewBreak; + final ChangeBreakResult _else = recChangeBreaks(((If) p).getElse(), b, noNewBreak); + noNewBreak = _else.noNewBreak; + return new ChangeBreakResult( + KeYJavaASTFactory.ifElse(((If) p).getExpression(), + (Then) then.result, (Else) _else.result), + noNewBreak); + } if (p instanceof StatementBlock) { Statement[] s = new Statement[((StatementBlock) p).getStatementCount()]; for (int i = 0; i < ((StatementBlock) p).getStatementCount(); i++) { - s[i] = (Statement) recChangeBreaks(((StatementBlock) p).getStatementAt(i), b); + final ChangeBreakResult blockStmnt = + recChangeBreaks(((StatementBlock) p).getStatementAt(i), b, noNewBreak); + noNewBreak = blockStmnt.noNewBreak; + s[i] = (Statement) blockStmnt.result; } - return KeYJavaASTFactory.block(s); + return new ChangeBreakResult( + KeYJavaASTFactory.block(s), + noNewBreak); } if (p instanceof Try) { int n = ((Try) p).getBranchCount(); Branch[] branches = new Branch[n]; for (int i = 0; i < n; i++) { - branches[i] = (Branch) recChangeBreaks(((Try) p).getBranchAt(i), b); + final ChangeBreakResult branch = + recChangeBreaks(((Try) p).getBranchAt(i), b, noNewBreak); + noNewBreak = branch.noNewBreak; + branches[i] = (Branch) branch.result; } - return KeYJavaASTFactory - .tryBlock((StatementBlock) recChangeBreaks(((Try) p).getBody(), b), branches); + final var block = recChangeBreaks(((Try) p).getBody(), b, noNewBreak); + noNewBreak = block.noNewBreak; + return new ChangeBreakResult( + KeYJavaASTFactory + .tryBlock((StatementBlock) block.result, branches), + noNewBreak); } - return p; + return new ChangeBreakResult(p, noNewBreak); } /** @@ -216,4 +251,7 @@ private StatementBlock collectStatements(Switch s, int count) { return KeYJavaASTFactory.block(stats); } + record ChangeBreakResult(ProgramElement result, boolean noNewBreak) { + } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java index c313592f4de..8d115bb3673 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java @@ -186,6 +186,8 @@ public Taclet generateRelationalRepresentsTaclet(Name tacletName, JTerm original tacletBuilder.setFind(findTerm); tacletBuilder.addTacletGoalTemplate(axiomTemplate); tacletBuilder.addVarsNotFreeIn(schemaAxiom.boundVars, selfSV); + tacletBuilder.setApplicationRestriction( + new ApplicationRestriction(ApplicationRestriction.SAME_UPDATE_LEVEL)); for (SchemaVariable heapSV : heapSVs) { tacletBuilder.addVarsNotFreeIn(schemaAxiom.boundVars, heapSV); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java index 832318754ec..da5c4f1c7ba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java @@ -127,22 +127,24 @@ public void writeSettings(Configuration props) { } protected PropertyEntry createDoubleProperty(String key, double defValue) { - PropertyEntry pe = - new DefaultPropertyEntry<>(key, defValue, parseDouble, (it) -> (double) it); + PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseDouble, + (it) -> ((Number) it).doubleValue()); propertyEntries.add(pe); return pe; } protected PropertyEntry createIntegerProperty(String key, int defValue) { + // A stored numeric value may deserialize as Integer or Long depending on its magnitude and + // the settings format, so accept any Number rather than assuming a particular boxed type. PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseInt, - (it) -> Math.toIntExact((Long) it)); + (it) -> Math.toIntExact(((Number) it).longValue())); propertyEntries.add(pe); return pe; } protected PropertyEntry createFloatProperty(String key, float defValue) { - PropertyEntry pe = - new DefaultPropertyEntry<>(key, defValue, parseFloat, (it) -> (float) (double) it); + PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseFloat, + (it) -> ((Number) it).floatValue()); propertyEntries.add(pe); return pe; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java index 3e59fd0e488..62704e2e31d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java @@ -1178,31 +1178,10 @@ public static Pair handleNameCla Operator newOp1; Operator newOp2; - if (partnerStateOp instanceof Function partnerFun) { - newOp1 = rename(new Name(tb.newName(partnerStateOp.name().toString(), - thisGoal.getLocalNamespaces())), (Function) mergeStateOp); - thisGoalNamespaces.functions().add((Function) newOp1); - thisGoalNamespaces.flushToParent(); - - newOp2 = rename(new Name(tb.newName(partnerStateOp.name().toString(), - thisGoal.getLocalNamespaces())), partnerFun); - thisGoalNamespaces.functions().add((Function) newOp2); - thisGoalNamespaces.flushToParent(); - } else if (partnerStateOp instanceof LocationVariable partnerLV) { - newOp1 = rename(new Name(tb.newName(partnerStateOp.name().toString(), - thisGoal.getLocalNamespaces())), (LocationVariable) mergeStateOp); - thisGoalNamespaces.programVariables().add((LocationVariable) newOp1); - thisGoalNamespaces.flushToParent(); - - newOp2 = rename(new Name(tb.newName(partnerStateOp.name().toString(), - thisGoal.getLocalNamespaces())), partnerLV); - thisGoalNamespaces.programVariables().add((LocationVariable) newOp2); - thisGoalNamespaces.flushToParent(); - } else { - throw new RuntimeException( - "MergeRule: Unexpected type of Operator involved in name clash: " - + partnerStateOp.getClass().getSimpleName()); - } + + newOp1 = renameMergeParticipantOp(partnerStateOp, mergeStateOp, thisGoal); + + newOp2 = renameMergeParticipantOp(partnerStateOp, partnerStateOp, thisGoal); mergeState = new SymbolicExecutionState( OpReplacer.replace(mergeStateOp, newOp1, mergeState.getSymbolicState(), tb.tf(), @@ -1223,6 +1202,36 @@ public static Pair handleNameCla return new Pair<>(mergeState, mergePartnerState); } + /** + * returns an operator of the same kind like mergeStateOp but with a unique name + * + * @param partnerStateOp the {@link Operator} on whose name the name is based + * @param mergeStateOp the {@link Operator} to rename + * @param thisGoal the {@link Goal} where the mergeStateOp occurs + * @return the renamed {@link Operator} + */ + private static @NonNull Operator renameMergeParticipantOp(Operator partnerStateOp, + Operator mergeStateOp, Goal thisGoal) { + final TermBuilder tb = thisGoal.getOverlayServices().getTermBuilder(); + final NamespaceSet thisGoalNamespaces = thisGoal.getLocalNamespaces(); + Operator newOp1; + if (mergeStateOp instanceof Function mergeFct) { + newOp1 = rename(new Name(tb.newName(partnerStateOp.name().toString(), + thisGoal.getLocalNamespaces())), mergeFct); + thisGoalNamespaces.functions().add((Function) newOp1); + } else if (mergeStateOp instanceof LocationVariable mergeLV) { + newOp1 = rename(new Name(tb.newName(partnerStateOp.name().toString(), + thisGoal.getLocalNamespaces())), mergeLV); + thisGoalNamespaces.programVariables().add((LocationVariable) newOp1); + } else { + throw new RuntimeException( + "MergeRule: Unexpected type of Operator involved in name clash: " + + mergeStateOp + " : " + mergeStateOp.getClass().getSimpleName()); + } + thisGoalNamespaces.flushToParent(); + return newOp1; + } + /** * Parses a declaration of the type "<SORT> <NAME>", where <SORT> must be a * sort known to the proof and <NAME> must be a fresh name. This method is used, for diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Math.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Math.java index 60b6f262fa3..10584b0885f 100755 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Math.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Math.java @@ -1,7 +1,7 @@ package java.lang; public final class Math { - + private Math() {} /*@ public normal_behavior @@ -92,4 +92,6 @@ public static float max(float a, float b) { public static double pow(double a , double b); public static double exp(double a); public static double atan(double a); + + public static double random(); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java index 9e3a2489693..7ff333e05b0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/String.java @@ -4,12 +4,6 @@ public final class String extends java.lang.Object implements java.io.Serializab { // public final static java.util.Comparator CASE_INSENSITIVE_ORDER; - /*@ normal_behavior - ensures \result == \dl_seqLen(\dl_strContent(this)); - */ - public /*@pure*/ int length(); - - /*@ public normal_behavior requires true; diff --git a/key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof b/key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof index bef3d72c971..27d1feea12b 100644 --- a/key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof +++ b/key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof @@ -385,14 +385,14 @@ instantiate hide var=iv with=(jv_1); instantiate hide var=jv with=(v_x_0); rule impLeft; tryclose branch; -tryclose branch; +// tryclose branch; // established: r4 is permutation // established: r4 fixes v_y_0 // from now on v_x_0 != v_y_0 and s_0[v_x_0]!= v_x_0 and // s_0[v_y_0]!= v_y_0 and s_0[v_x_0]!= v_y_0 and s_0[v_y_0]!=v_x_0; // this corresponds to case B4iv in the Notes // in the following r5 refers to this instantion -tryclose branch; +//tryclose branch; // established: r5 is of the correct length rule seqNPermSwapNPerm formula=(seqNPerm(s_0)); instantiate hide var=iv with=(v_x_0); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java index 6da047917e9..25c93c7a53f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java @@ -133,7 +133,10 @@ public Component getListCellRendererComponent(JList list, Object value, int i } else if (ps.getProofClosedByCache()) { label.setIcon(KEY_CACHED_CLOSED); } else { - assert ps.getProofOpen(); + if (!ps.getProofOpen()) { + LOGGER.warn("Unknown proof status " + ps + + " in ProofManagementDialog. Displaying open icon."); + } label.setIcon(KEY_OPEN); } } @@ -514,6 +517,8 @@ private void updateStartButton() { startButton.setIcon(KEY_OPEN); } else if (status.getProofClosedButLemmasLeft()) { startButton.setIcon(KEY_ALMOST_CLOSED); + } else if (status.getProofClosedByCache()) { + startButton.setIcon(KEY_CACHED_CLOSED); } else { assert status.getProofClosed(); startButton.setIcon(KEY_CLOSED); diff --git a/key.util/src/main/java/org/key_project/util/java/StringUtil.java b/key.util/src/main/java/org/key_project/util/java/StringUtil.java index 3d1f6ed4212..da7fc1b59a8 100644 --- a/key.util/src/main/java/org/key_project/util/java/StringUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/StringUtil.java @@ -504,14 +504,14 @@ public static String move(@NonNull String text, int line, int charPositionInLine /// Returns the string until the first match of the given regex. public static String takeUntil(String content, String regex) { - var array = content.split(regex, 1); + var array = content.split(regex, 2); return array[0]; } /// Returns the string after the first match of the given regex. public static String takeAfter(String content, String regex) { - var array = content.split(regex, 1); - return array[0]; + var array = content.split(regex, 2); + return array[1]; } diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/Issue3437Test.java b/keyext.slicing/src/test/java/org/key_project/slicing/Issue3437Test.java index 0c3b79031df..0ee0319a3ca 100644 --- a/keyext.slicing/src/test/java/org/key_project/slicing/Issue3437Test.java +++ b/keyext.slicing/src/test/java/org/key_project/slicing/Issue3437Test.java @@ -44,7 +44,7 @@ void loadsAndSlicesCorrectly() throws Exception { .constructSlicer(control, proof, results, env.getUi()); var newFile = replayer.slice(); var env2 = KeYEnvironment.load(newFile); - var proof2 = env.getLoadedProof(); + var proof2 = env2.getLoadedProof(); assertTrue(proof2.closed()); env.dispose(); diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/Issue3834Test.java b/keyext.slicing/src/test/java/org/key_project/slicing/Issue3834Test.java new file mode 100644 index 00000000000..e1e01e27d54 --- /dev/null +++ b/keyext.slicing/src/test/java/org/key_project/slicing/Issue3834Test.java @@ -0,0 +1,66 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.slicing; + +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.io.ProblemLoaderControl; +import de.uka.ilkd.key.settings.GeneralSettings; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertTrue; + +/** + * Regression test for issue #3834. The loop scope rule introduces "before" variables (e.g. + * {@code k_before}) via {@code NewLocalVarsCondition}. These names used to carry a {@code #}-index + * taken from a proof-global counter that is advanced as a side effect of (speculative) taclet + * matching. The number of increments differs between a freshly created proof and one that has been + * pruned and re-run, so the variable name changed (e.g. {@code k_before#0} vs. {@code k_before#1}), + * which broke slicing (it relies on formula equivalence across reloads). + *

+ * The scenario mirrors {@link Issue3437Test}: load the proof, prune it and re-run automode so that + * the (previously volatile) counters would differ, then slice the proof and reload the slice. + */ +public class Issue3834Test { + public static final Path testCaseDirectory = FindResources.getTestCasesDirectory(); + + @Test + void loadsAndSlicesCorrectly() throws Exception { + GeneralSettings.noPruningClosed = false; + + var file = testCaseDirectory.resolve( + "issues/3834/SumAndMax(SumAndMax__sumAndMax((I)).JML normal_behavior operation contract.0.proof"); + var env = KeYEnvironment.load(file); + var proof = env.getLoadedProof(); + var tracker = new DependencyTracker(proof); + env.getProofControl().startAutoMode(proof, proof.openEnabledGoals()); + env.getProofControl().waitWhileAutoMode(); + assertTrue(proof.closed()); + // prune and re-run automode so the loop scope rule is reapplied; previously this changed + // the counter on the temporary "before" variables and thereby their names + proof.pruneProof(proof.findAny(x -> x.serialNr() == 13)); + env.getProofControl().startAutoMode(proof, proof.openEnabledGoals()); + env.getProofControl().waitWhileAutoMode(); + assertTrue(proof.closed()); + + var results = tracker.analyze(true, false); + + ProblemLoaderControl control = new DefaultUserInterfaceControl(); + SlicingProofReplayer replayer = SlicingProofReplayer + .constructSlicer(control, proof, results, env.getUi()); + var newFile = replayer.slice(); + var env2 = KeYEnvironment.load(newFile); + var proof2 = env2.getLoadedProof(); + assertTrue(proof2.closed()); + + env.dispose(); + env2.dispose(); + GeneralSettings.noPruningClosed = true; + } +} diff --git a/keyext.slicing/src/test/resources/testcase/issues/3834/SumAndMax(SumAndMax__sumAndMax((I)).JML normal_behavior operation contract.0.proof b/keyext.slicing/src/test/resources/testcase/issues/3834/SumAndMax(SumAndMax__sumAndMax((I)).JML normal_behavior operation contract.0.proof new file mode 100644 index 00000000000..fda22d0095d --- /dev/null +++ b/keyext.slicing/src/test/resources/testcase/issues/3834/SumAndMax(SumAndMax__sumAndMax((I)).JML normal_behavior operation contract.0.proof @@ -0,0 +1,2439 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 10000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_COMPLETION", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "."; + +\proofObligation +// +{ + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "SumAndMax[SumAndMax::sumAndMax([I)].JML normal_behavior operation contract.0", + "name" : "SumAndMax[SumAndMax::sumAndMax([I)].JML normal_behavior operation contract.0" +} + +\proof { +(keyLog "0" (keyUser "bubel" ) (keyVersion "0ded37352caf2fe8c6abf2495252f6125373ac71")) + +(autoModeTime "1929") + +(branch "dummy ID" + (builtin "One Step Simplification" (formula "1") (newnames "heapAtPre,o,f")) +(rule "impRight" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "3")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "5")) +(rule "andLeft" (formula "1")) +(rule "notLeft" (formula "7")) +(rule "andLeft" (formula "1")) +(rule "andLeft" (formula "1")) +(rule "notLeft" (formula "2")) +(rule "eqSymm" (formula "10") (term "1,0,0,1,0,1")) +(rule "eqSymm" (formula "10") (term "0,1,1,0,0,0,1")) +(rule "eqSymm" (formula "10") (term "1,0,1,0,1,0,0,0,1")) +(rule "replace_known_right" (formula "4") (term "0") (ifseqformula "9")) + (builtin "One Step Simplification" (formula "4")) +(rule "polySimp_mulComm0" (formula "10") (term "1,0,1,1,1,0,0,0,1")) +(rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,0,0,0,0,0,1")) +(rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1")) +(rule "inEqSimp_gtToGeq" (formula "10") (term "0,0,1,0,0,0,1")) +(rule "times_zero_1" (formula "10") (term "1,0,0,0,0,1,0,0,0,1")) +(rule "add_zero_right" (formula "10") (term "0,0,0,0,1,0,0,0,1")) +(rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,0,1,0,1,0,0,0,1")) +(rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,0,1,0,1,0,0,0,1")) +(rule "inEqSimp_ltToLeq" (formula "6") (term "1,0,0")) +(rule "polySimp_mulComm0" (formula "6") (term "1,0,0,1,0,0")) +(rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,1,0,1,0,0,0,1")) +(rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,0,0,0,0,1")) +(rule "inEqSimp_commuteLeq" (formula "6") (term "0,0,0")) +(rule "inEqSimp_commuteLeq" (formula "6") (term "1,0")) +(rule "inEqSimp_commuteLeq" (formula "10") (term "0,1,1,1,0,0,0,1")) +(rule "assignment" (formula "10") (term "1")) + (builtin "One Step Simplification" (formula "10")) +(rule "inEqSimp_sepPosMonomial0" (formula "6") (term "1,0,0")) +(rule "polySimp_mulComm0" (formula "6") (term "1,1,0,0")) +(rule "polySimp_rightDist" (formula "6") (term "1,1,0,0")) +(rule "polySimp_mulLiterals" (formula "6") (term "1,1,1,0,0")) +(rule "mul_literals" (formula "6") (term "0,1,1,0,0")) +(rule "polySimp_elimOne" (formula "6") (term "1,1,1,0,0")) +(rule "inEqSimp_sepPosMonomial0" (formula "10") (term "1,0,0,0,0,0,0,1")) +(rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,0,0,0,0,1")) +(rule "polySimp_rightDist" (formula "10") (term "1,1,0,0,0,0,0,0,1")) +(rule "polySimp_mulLiterals" (formula "10") (term "1,1,1,0,0,0,0,0,0,1")) +(rule "mul_literals" (formula "10") (term "0,1,1,0,0,0,0,0,0,1")) +(rule "polySimp_elimOne" (formula "10") (term "1,1,1,0,0,0,0,0,0,1")) +(rule "inEqSimp_sepPosMonomial0" (formula "10") (term "1,0,0,1,0,1,0,0,0,1")) +(rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,1,0,1,0,0,0,1")) +(rule "polySimp_rightDist" (formula "10") (term "1,1,0,0,1,0,1,0,0,0,1")) +(rule "polySimp_mulLiterals" (formula "10") (term "1,1,1,0,0,1,0,1,0,0,0,1")) +(rule "mul_literals" (formula "10") (term "0,1,1,0,0,1,0,1,0,0,0,1")) +(rule "polySimp_elimOne" (formula "10") (term "1,1,1,0,0,1,0,1,0,0,0,1")) +(rule "inEqSimp_sepPosMonomial1" (formula "10") (term "0,0,1,0,0,0,1")) +(rule "mul_literals" (formula "10") (term "1,0,0,1,0,0,0,1")) +(rule "elementOfUnion" (formula "10") (term "0,0,0,0,1,0,1")) +(rule "elementOfSingleton" (formula "10") (term "0,0,0,0,0,1,0,1")) +(rule "elementOfSingleton" (formula "10") (term "1,0,0,0,0,1,0,1")) +(rule "nnf_imp2or" (formula "6") (term "0")) +(rule "nnf_notAnd" (formula "6") (term "0,0")) +(rule "inEqSimp_notLeq" (formula "6") (term "1,0,0")) +(rule "polySimp_rightDist" (formula "6") (term "1,0,0,1,0,0")) +(rule "mul_literals" (formula "6") (term "0,1,0,0,1,0,0")) +(rule "polySimp_addAssoc" (formula "6") (term "0,0,1,0,0")) +(rule "add_literals" (formula "6") (term "0,0,0,1,0,0")) +(rule "add_zero_left" (formula "6") (term "0,0,1,0,0")) +(rule "inEqSimp_sepPosMonomial1" (formula "6") (term "1,0,0")) +(rule "polySimp_mulLiterals" (formula "6") (term "1,1,0,0")) +(rule "polySimp_elimOne" (formula "6") (term "1,1,0,0")) +(rule "inEqSimp_notGeq" (formula "6") (term "0,0,0")) +(rule "times_zero_1" (formula "6") (term "1,0,0,0,0,0")) +(rule "add_zero_right" (formula "6") (term "0,0,0,0,0")) +(rule "inEqSimp_sepPosMonomial0" (formula "6") (term "0,0,0")) +(rule "mul_literals" (formula "6") (term "1,0,0,0")) +(rule "nnf_imp2or" (formula "10") (term "0,0,0,0,0,1")) +(rule "nnf_notAnd" (formula "10") (term "0,0,0,0,0,0,1")) +(rule "inEqSimp_notGeq" (formula "10") (term "0,0,0,0,0,0,0,1")) +(rule "times_zero_1" (formula "10") (term "1,0,0,0,0,0,0,0,0,0,1")) +(rule "add_zero_right" (formula "10") (term "0,0,0,0,0,0,0,0,0,1")) +(rule "inEqSimp_sepPosMonomial0" (formula "10") (term "0,0,0,0,0,0,0,1")) +(rule "mul_literals" (formula "10") (term "1,0,0,0,0,0,0,0,1")) +(rule "inEqSimp_notLeq" (formula "10") (term "1,0,0,0,0,0,0,1")) +(rule "polySimp_rightDist" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1")) +(rule "mul_literals" (formula "10") (term "0,1,0,0,1,0,0,0,0,0,0,1")) +(rule "polySimp_addAssoc" (formula "10") (term "0,0,1,0,0,0,0,0,0,1")) +(rule "add_literals" (formula "10") (term "0,0,0,1,0,0,0,0,0,0,1")) +(rule "add_zero_left" (formula "10") (term "0,0,1,0,0,0,0,0,0,1")) +(rule "inEqSimp_sepPosMonomial1" (formula "10") (term "1,0,0,0,0,0,0,1")) +(rule "polySimp_mulLiterals" (formula "10") (term "1,1,0,0,0,0,0,0,1")) +(rule "polySimp_elimOne" (formula "10") (term "1,1,0,0,0,0,0,0,1")) +(rule "Class_invariant_axiom_for_SumAndMax" (formula "7") (ifseqformula "3")) +(rule "true_left" (formula "7")) +(rule "methodBodyExpand" (formula "9") (term "1") (newnames "heapBefore_sumAndMax,savedHeapBefore_sumAndMax,_aBefore_sumAndMax")) + (builtin "One Step Simplification" (formula "9")) +(rule "assignment_write_attribute_this" (formula "9")) + (builtin "One Step Simplification" (formula "9")) +(rule "assignment_write_attribute_this" (formula "9")) + (builtin "One Step Simplification" (formula "9")) +(rule "variableDeclarationAssign" (formula "9") (term "1")) +(rule "variableDeclaration" (formula "9") (term "1") (newnames "k")) +(rule "assignment" (formula "9") (term "1")) + (builtin "One Step Simplification" (formula "9")) +(rule "loopScopeInvDia" (formula "9") (term "1") (newnames "k_0,o,f") (inst "#heapBefore_LOOP=h") (inst "#permissionsBefore_LOOP=h_2") (inst "#savedHeapBefore_LOOP=h_1") (inst "#variant=a_1") (inst "#x=b") (inst "anon_heap_LOOP=anon_heap_LOOP_0") (inst "anon_permissions_LOOP=anon_permissions_LOOP_0") (inst "anon_savedHeap_LOOP=anon_savedHeap_LOOP_0")) +(branch "Invariant Initially Valid" + (builtin "One Step Simplification" (formula "9")) + (rule "bsum_lower_equals_upper" (formula "9") (term "1,1,0")) + (rule "greater_literals" (formula "9") (term "0,1,0,0")) + (builtin "One Step Simplification" (formula "9")) + (rule "leq_literals" (formula "9") (term "0,0,0,0,0")) + (builtin "One Step Simplification" (formula "9")) + (rule "times_zero_2" (formula "9") (term "1,1")) + (rule "dismissNonSelectedField" (formula "9") (term "0,1,0,1,0,0,0")) + (rule "dismissNonSelectedField" (formula "9") (term "0,1,0")) + (rule "dismissNonSelectedField" (formula "9") (term "0,1")) + (rule "dismissNonSelectedField" (formula "9") (term "0,1,0,1,0,0,0")) + (rule "inEqSimp_ltToLeq" (formula "9") (term "1,0,0,1,0,0,0")) + (rule "times_zero_1" (formula "9") (term "1,0,0,1,0,0,1,0,0,0")) + (rule "add_zero_right" (formula "9") (term "0,0,1,0,0,1,0,0,0")) + (rule "inEqSimp_commuteLeq" (formula "9") (term "0,0,0,0")) + (rule "inEqSimp_commuteLeq" (formula "9") (term "0,0,0,1,0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "9") (term "1,0,0,1,0,0,0")) + (rule "mul_literals" (formula "9") (term "1,1,0,0,1,0,0,0")) + (rule "pullOutSelect" (formula "9") (term "0,1,0,0") (inst "selectSK=SumAndMax_max_0:int")) + (rule "applyEq" (formula "10") (term "1,1,0,1,0,0,0") (ifseqformula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "0")) + (rule "applyEqReverse" (formula "10") (term "0,1,0,0") (ifseqformula "1")) + (builtin "One Step Simplification" (formula "10")) + (rule "applyEqReverse" (formula "10") (term "1,1,0,1,0,0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "pullOutSelect" (formula "9") (term "0,1,0") (inst "selectSK=SumAndMax_sum_0:int")) + (rule "applyEq" (formula "10") (term "0,1") (ifseqformula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "0")) + (rule "applyEqReverse" (formula "10") (term "0,1,0") (ifseqformula "1")) + (builtin "One Step Simplification" (formula "10")) + (rule "applyEqReverse" (formula "10") (term "0,1") (ifseqformula "1")) + (rule "leq_literals" (formula "10") (term "1")) + (builtin "One Step Simplification" (formula "10")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "nnf_imp2or" (formula "9") (term "0,1")) + (rule "nnf_notAnd" (formula "9") (term "0,0,1")) + (rule "inEqSimp_notLeq" (formula "9") (term "1,0,0,1")) + (rule "mul_literals" (formula "9") (term "1,0,0,1,0,0,1")) + (rule "add_literals" (formula "9") (term "0,0,1,0,0,1")) + (rule "add_zero_left" (formula "9") (term "0,1,0,0,1")) + (builtin "One Step Simplification" (formula "9")) + (rule "inEqSimp_geqRight" (formula "9")) + (rule "times_zero_1" (formula "1") (term "1,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1")) + (rule "mul_literals" (formula "1") (term "1")) + (rule "arrayLengthNotNegative" (formula "7") (term "1,1,0,0")) + (rule "inEqSimp_contradInEq0" (formula "7") (ifseqformula "1")) + (rule "qeq_literals" (formula "7") (term "0")) + (builtin "One Step Simplification" (formula "7")) + (rule "closeFalse" (formula "7")) +) +(branch "Invariant Preserved and Used" + (builtin "One Step Simplification" (formula "10")) + (rule "eqSymm" (formula "10") (term "1,0,0,1,0,1,1,0,1,1,0,1")) + (rule "eqSymm" (formula "10") (term "1,0,0,0,1,1,0,1,1,0,1")) + (rule "eqSymm" (formula "10") (term "1,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "eqSymm" (formula "10") (term "1,0,0,0,1")) + (rule "eqSymm" (formula "10") (term "1,0,1,1,0,0,0,0,1")) + (rule "polySimp_elimSub" (formula "10") (term "0,1,0,1,0,1")) + (rule "polySimp_elimSub" (formula "10") (term "0,1,1,1,0,1,1,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,1")) + (rule "polySimp_addComm0" (formula "10") (term "0,1,0,1,0,1")) + (rule "polySimp_addComm0" (formula "10") (term "0,1,1,1,0,1,1,0,1")) + (rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,0,1,1,0,0,0,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,0,1,1,0,0,0,0,1")) + (rule "inEqSimp_gtToGeq" (formula "10") (term "0,1,0,0,0,0,1")) + (rule "times_zero_1" (formula "10") (term "1,0,0,0,1,0,0,0,0,1")) + (rule "add_zero_right" (formula "10") (term "0,0,0,1,0,0,0,0,1")) + (rule "inEqSimp_gtToGeq" (formula "10") (term "0,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "times_zero_1" (formula "10") (term "1,0,0,0,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "add_zero_right" (formula "10") (term "0,0,0,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,0,1,0,0,0,0,0,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,1,1,0,0,0,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "1,0,0,0,0,0,0,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,0,0,0,0,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "1,0,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,1,0,0,0,0,0,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "1,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_commuteLeq" (formula "10") (term "1,0,0,1")) + (rule "variableDeclaration" (formula "10") (term "1") (newnames "h")) + (rule "variableDeclaration" (formula "10") (term "1") (newnames "h_1")) + (rule "variableDeclaration" (formula "10") (term "1") (newnames "h_2")) + (rule "variableDeclaration" (formula "10") (term "1") (newnames "a_1")) + (rule "variableDeclaration" (formula "10") (term "1") (newnames "k_before")) + (rule "variableDeclaration" (formula "10") (term "1,1,0,1") (newnames "b")) + (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_rightDist" (formula "10") (term "1,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_mulLiterals" (formula "10") (term "1,1,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "mul_literals" (formula "10") (term "0,1,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_elimOne" (formula "10") (term "1,1,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "1,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_rightDist" (formula "10") (term "1,1,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_mulLiterals" (formula "10") (term "1,1,1,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "mul_literals" (formula "10") (term "0,1,1,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_elimOne" (formula "10") (term "1,1,1,0,0,1,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "1,0,0,1,1,0,0,0,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,1,1,0,0,0,0,1")) + (rule "polySimp_rightDist" (formula "10") (term "1,1,0,0,1,1,0,0,0,0,1")) + (rule "polySimp_mulLiterals" (formula "10") (term "1,1,1,0,0,1,1,0,0,0,0,1")) + (rule "mul_literals" (formula "10") (term "0,1,1,0,0,1,1,0,0,0,0,1")) + (rule "polySimp_elimOne" (formula "10") (term "1,1,1,0,0,1,1,0,0,0,0,1")) + (rule "inEqSimp_sepPosMonomial1" (formula "10") (term "0,1,0,0,0,0,1")) + (rule "mul_literals" (formula "10") (term "1,0,1,0,0,0,0,1")) + (rule "inEqSimp_sepPosMonomial1" (formula "10") (term "0,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "mul_literals" (formula "10") (term "1,0,1,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_rightDist" (formula "10") (term "1,1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_mulLiterals" (formula "10") (term "1,1,1,0,0,1,0,0,0,0,0,0,1")) + (rule "mul_literals" (formula "10") (term "0,1,1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_elimOne" (formula "10") (term "1,1,1,0,0,1,0,0,0,0,0,0,1")) + (rule "elementOfUnion" (formula "10") (term "0,0,0,0,1,0,1,1,0,1,1,0,1")) + (rule "elementOfSingleton" (formula "10") (term "1,0,0,0,0,1,0,1,1,0,1,1,0,1")) + (rule "elementOfSingleton" (formula "10") (term "0,0,0,0,0,1,0,1,1,0,1,1,0,1")) + (rule "nnf_imp2or" (formula "10") (term "0,1,0,0,0,0,0,0,1")) + (rule "nnf_notAnd" (formula "10") (term "0,0,1,0,0,0,0,0,0,1")) + (rule "inEqSimp_notGeq" (formula "10") (term "0,0,0,1,0,0,0,0,0,0,1")) + (rule "times_zero_1" (formula "10") (term "1,0,0,0,0,0,1,0,0,0,0,0,0,1")) + (rule "add_zero_right" (formula "10") (term "0,0,0,0,0,1,0,0,0,0,0,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "0,0,0,1,0,0,0,0,0,0,1")) + (rule "mul_literals" (formula "10") (term "1,0,0,0,1,0,0,0,0,0,0,1")) + (rule "inEqSimp_notLeq" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_rightDist" (formula "10") (term "1,0,0,1,0,0,1,0,0,0,0,0,0,1")) + (rule "mul_literals" (formula "10") (term "0,1,0,0,1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_addAssoc" (formula "10") (term "0,0,1,0,0,1,0,0,0,0,0,0,1")) + (rule "add_literals" (formula "10") (term "0,0,0,1,0,0,1,0,0,0,0,0,0,1")) + (rule "add_zero_left" (formula "10") (term "0,0,1,0,0,1,0,0,0,0,0,0,1")) + (rule "inEqSimp_sepPosMonomial1" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_mulLiterals" (formula "10") (term "1,1,0,0,1,0,0,0,0,0,0,1")) + (rule "polySimp_elimOne" (formula "10") (term "1,1,0,0,1,0,0,0,0,0,0,1")) + (rule "nnf_imp2or" (formula "10") (term "0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "nnf_notAnd" (formula "10") (term "0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_notLeq" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_rightDist" (formula "10") (term "1,0,0,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "mul_literals" (formula "10") (term "0,1,0,0,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_addAssoc" (formula "10") (term "0,0,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "add_literals" (formula "10") (term "0,0,0,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "add_zero_left" (formula "10") (term "0,0,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_sepPosMonomial1" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_mulLiterals" (formula "10") (term "1,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "polySimp_elimOne" (formula "10") (term "1,1,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_notGeq" (formula "10") (term "0,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "times_zero_1" (formula "10") (term "1,0,0,0,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "add_zero_right" (formula "10") (term "0,0,0,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "0,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "mul_literals" (formula "10") (term "1,0,0,0,1,0,0,0,0,0,0,1,1,0,1,1,0,1")) + (rule "emptyModality" (formula "10") (term "1")) + (builtin "One Step Simplification" (formula "10")) + (rule "impRight" (formula "10")) + (rule "andLeft" (formula "1")) + (rule "andLeft" (formula "1")) + (rule "andLeft" (formula "1")) + (rule "andLeft" (formula "1")) + (rule "andLeft" (formula "1")) + (rule "andLeft" (formula "1")) + (rule "pullOutSelect" (formula "7") (term "1") (inst "selectSK=SumAndMax_sum_0:int")) + (rule "applyEq" (formula "6") (term "1") (ifseqformula "7")) + (rule "simplifySelectOfAnon" (formula "7")) + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "16"))) + (rule "dismissNonSelectedField" (formula "7") (term "2,0")) + (rule "dismissNonSelectedField" (formula "7") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "7") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "7") (term "0,1,0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "7")) + (rule "elementOfUnion" (formula "7") (term "0,0")) + (rule "elementOfSingleton" (formula "7") (term "0,0,0")) + (builtin "One Step Simplification" (formula "7")) + (rule "applyEqReverse" (formula "8") (term "1") (ifseqformula "7")) + (rule "applyEqReverse" (formula "6") (term "1") (ifseqformula "7")) + (rule "hideAuxiliaryEq" (formula "7")) + (rule "pullOutSelect" (formula "7") (term "0,0") (inst "selectSK=SumAndMax_max_0:int")) + (rule "applyEq" (formula "3") (term "1,1,0") (ifseqformula "7")) + (rule "applyEq" (formula "4") (term "0,1") (ifseqformula "7")) + (rule "applyEq" (formula "5") (term "1,1,0,1") (ifseqformula "7")) + (rule "simplifySelectOfAnon" (formula "7")) + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "16"))) + (rule "polySimp_mulComm0" (formula "8") (term "0")) + (rule "dismissNonSelectedField" (formula "7") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "7") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "7") (term "0,1,0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "7")) + (rule "elementOfUnion" (formula "7") (term "0,0")) + (rule "elementOfSingleton" (formula "7") (term "1,0,0")) + (builtin "One Step Simplification" (formula "7")) + (rule "applyEqReverse" (formula "8") (term "1,0") (ifseqformula "7")) + (rule "applyEqReverse" (formula "5") (term "1,1,0,1") (ifseqformula "7")) + (rule "applyEqReverse" (formula "4") (term "0,1") (ifseqformula "7")) + (rule "applyEqReverse" (formula "3") (term "1,1,0") (ifseqformula "7")) + (rule "hideAuxiliaryEq" (formula "7")) + (rule "polySimp_mulComm0" (formula "7") (term "0")) + (rule "commuteUnion" (formula "17") (term "1,0,1,0,1,0")) + (rule "commuteUnion" (formula "6") (term "1,0,2,0")) + (rule "commuteUnion" (formula "5") (term "1,0,0,1,0,1")) + (rule "commuteUnion" (formula "3") (term "1,0,0,1,0")) + (rule "arrayLengthNotNegative" (formula "14") (term "1,1,0,0")) + (rule "arrayLengthIsAnInt" (formula "15") (term "1,1,0,0")) + (builtin "One Step Simplification" (formula "15")) + (rule "true_left" (formula "15")) + (rule "ifElseUnfold" (formula "18") (term "1") (inst "#boolv=b_1")) + (rule "variableDeclaration" (formula "18") (term "1") (newnames "b_1")) + (rule "compound_less_than_comparison_2" (formula "18") (term "1") (inst "#v0=i") (inst "#v1=i_1")) + (rule "variableDeclarationAssign" (formula "18") (term "1")) + (rule "variableDeclaration" (formula "18") (term "1") (newnames "i")) + (rule "assignment" (formula "18") (term "1")) + (builtin "One Step Simplification" (formula "18")) + (rule "variableDeclarationAssign" (formula "18") (term "1")) + (rule "variableDeclaration" (formula "18") (term "1") (newnames "i_1")) + (rule "assignment_read_length" (formula "18")) + (branch "Normal Execution (k < _a.length != null)" + (builtin "One Step Simplification" (formula "18")) + (rule "less_than_comparison_simple" (formula "18") (term "1")) + (builtin "One Step Simplification" (formula "18")) + (rule "inEqSimp_ltToLeq" (formula "18") (term "0,0,1,0")) + (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,0,0,1,0")) + (rule "polySimp_addComm1" (formula "18") (term "0,0,0,1,0")) + (rule "inEqSimp_sepNegMonomial0" (formula "18") (term "0,0,1,0")) + (rule "polySimp_mulLiterals" (formula "18") (term "0,0,0,1,0")) + (rule "polySimp_elimOne" (formula "18") (term "0,0,0,1,0")) + (rule "ifElseSplit" (formula "18")) + (branch "if k < _a.length true" + (builtin "One Step Simplification" (formula "19")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_subsumption1" (formula "3") (ifseqformula "1")) + (rule "inEqSimp_homoInEq0" (formula "3") (term "0")) + (rule "polySimp_pullOutFactor1b" (formula "3") (term "0,0")) + (rule "add_literals" (formula "3") (term "1,1,0,0")) + (rule "times_zero_1" (formula "3") (term "1,0,0")) + (rule "add_zero_right" (formula "3") (term "0,0")) + (rule "qeq_literals" (formula "3") (term "0")) + (builtin "One Step Simplification" (formula "3")) + (rule "true_left" (formula "3")) + (rule "ifUnfold" (formula "18") (term "1") (inst "#boolv=b_2")) + (rule "variableDeclaration" (formula "18") (term "1") (newnames "b_2")) + (rule "compound_less_than_comparison_2" (formula "18") (term "1") (inst "#v0=i_2") (inst "#v1=i_3")) + (rule "variableDeclarationAssign" (formula "18") (term "1")) + (rule "variableDeclaration" (formula "18") (term "1") (newnames "i_2")) + (rule "assignment_read_attribute_this" (formula "18")) + (builtin "One Step Simplification" (formula "18")) + (rule "pullOutSelect" (formula "18") (term "0,1,0") (inst "selectSK=SumAndMax_max_1:int")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "1")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_3")) + (rule "assignment_array2" (formula "19")) + (branch "Normal Execution (k < _a.length != null)" + (builtin "One Step Simplification" (formula "19")) + (rule "pullOutSelect" (formula "19") (term "0,1,0") (inst "selectSK=arr_0:int")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "19"))) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "14")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "2") (term "0,0")) + (rule "elementOfSingleton" (formula "2") (term "0,0,0")) + (builtin "One Step Simplification" (formula "2")) + (rule "applyEqReverse" (formula "20") (term "0,1,0,0") (ifseqformula "2")) + (rule "hideAuxiliaryEq" (formula "2")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "19") (term "0,1,0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "less_than_comparison_simple" (formula "18") (term "1")) + (builtin "One Step Simplification" (formula "18")) + (rule "inEqSimp_ltToLeq" (formula "18") (term "0,0,1,0")) + (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,0,0,1,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "18") (term "0,0,1,0")) + (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,1,0")) + (rule "polySimp_rightDist" (formula "18") (term "1,0,0,1,0")) + (rule "polySimp_mulLiterals" (formula "18") (term "1,1,0,0,1,0")) + (rule "mul_literals" (formula "18") (term "0,1,0,0,1,0")) + (rule "polySimp_elimOne" (formula "18") (term "1,1,0,0,1,0")) + (rule "ifSplit" (formula "18")) + (branch "if this.max < _a[k] true" + (builtin "One Step Simplification" (formula "19")) + (builtin "One Step Simplification" (formula "1")) + (rule "eval_order_access4_this" (formula "19") (term "1") (inst "#v1=i_4")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_4")) + (rule "assignment_array2" (formula "19")) + (branch "Normal Execution (k < _a.length != null)" + (builtin "One Step Simplification" (formula "19")) + (rule "replaceKnownSelect_taclet0001_5" (formula "19") (term "0,1,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_7" (formula "19") (term "0,1,0")) + (rule "assignment_write_attribute_this" (formula "19")) + (builtin "One Step Simplification" (formula "19")) + (rule "blockEmpty" (formula "19") (term "1")) + (rule "compound_assignment_op_plus_attr" (formula "19") (term "1") (inst "#v=s")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "s")) + (rule "assignment" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "eval_order_access4" (formula "19") (term "1") (inst "#v0=s_1") (inst "#v1=i_5")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "s_1")) + (rule "assignment" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_5")) + (rule "compound_int_cast_expression" (formula "19") (term "1") (inst "#v=i_6")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_6")) + (rule "remove_parentheses_right" (formula "19") (term "1")) + (rule "compound_addition_2" (formula "19") (term "1") (inst "#v0=i_7") (inst "#v1=i_8")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_7")) + (rule "assignment_read_attribute" (formula "19")) + (branch "Normal Execution (s != null)" + (builtin "One Step Simplification" (formula "19")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0")) + (rule "pullOutSelect" (formula "19") (term "0,1,0") (inst "selectSK=SumAndMax_sum_1:int")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "18"))) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "1")) + (rule "variableDeclarationAssign" (formula "20") (term "1")) + (rule "variableDeclaration" (formula "20") (term "1") (newnames "i_8")) + (rule "assignment_array2" (formula "20")) + (branch "Normal Execution (k < _a.length != null)" + (builtin "One Step Simplification" (formula "20")) + (rule "dismissNonSelectedField" (formula "20") (term "0,1,0")) + (rule "replaceKnownSelect_taclet0001_5" (formula "20") (term "0,1,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_7" (formula "20") (term "0,1,0")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "20") (term "0,1,0,0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "assignmentAdditionInt" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "translateJavaAddInt" (formula "19") (term "0,1,0")) + (rule "polySimp_addComm0" (formula "19") (term "0,1,0")) + (rule "widening_identity_cast_5" (formula "19") (term "1")) + (rule "assignment" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "assignment_write_attribute" (formula "19")) + (branch "Normal Execution (s_1 != null)" + (builtin "One Step Simplification" (formula "19")) + (rule "postincrement" (formula "19") (term "1")) + (rule "compound_int_cast_expression" (formula "19") (term "1") (inst "#v=i_9")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_9")) + (rule "remove_parentheses_right" (formula "19") (term "1")) + (rule "assignmentAdditionInt" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "translateJavaAddInt" (formula "19") (term "0,1,0")) + (rule "polySimp_addComm0" (formula "19") (term "0,1,0")) + (rule "widening_identity_cast_5" (formula "19") (term "1")) + (rule "assignment" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "blockEmpty" (formula "19") (term "1")) + (rule "lsContinue" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19") (ifInst "" (formula "2"))) + (rule "eqSymm" (formula "19") (term "1,0,0,1,0")) + (rule "polySimp_mulComm0" (formula "19") (term "0,0,1")) + (rule "polySimp_rightDist" (formula "19") (term "0,1,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "0,0,1,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,1,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "0,0,1")) + (rule "mul_literals" (formula "19") (term "0,0,0,1")) + (rule "polySimp_addAssoc" (formula "19") (term "1,1,0,0,1,1,0,0,0,0")) + (rule "add_literals" (formula "19") (term "0,1,1,0,0,1,1,0,0,0,0")) + (rule "add_zero_left" (formula "19") (term "1,1,0,0,1,1,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0,1,1,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "1,1,0,1,0,0,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,1,0,0,0,0,0")) + (rule "bsum_induction_upper_concrete" (formula "19") (term "0,1,0,0,0")) + (rule "polySimp_homoEq" (formula "19") (term "1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_addComm0" (formula "19") (term "1,1,0,1,0,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "0,1,0,1,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "1,1,0,1,1,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0,1,0,0,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,0,1,1,0,0,0,1,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0,1,0,0")) + (rule "precOfInt" (formula "19") (term "1")) + (rule "polySimp_addAssoc" (formula "19") (term "0,1,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0,1,1,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0,1,0,0,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,0,1,1,0,0,0,1,0")) + (rule "dismissNonSelectedField" (formula "19") (term "1,0,1,0,0,1,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "2,0,1,0,1,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "1,0,1,0,0,1,0,0,0")) + (rule "replaceKnownSelect_taclet0001_5" (formula "19") (term "1,0,1,0,0,1,0,0,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_7" (formula "19") (term "1,0,1,0,0,1,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "2,0,1,0,1,0,0,0")) + (rule "inEqSimp_ltToLeq" (formula "19") (term "1,1")) + (rule "polySimp_rightDist" (formula "19") (term "1,0,0,1,1")) + (rule "polySimp_mulAssoc" (formula "19") (term "0,1,0,0,1,1")) + (rule "polySimp_mulComm0" (formula "19") (term "0,0,1,0,0,1,1")) + (rule "polySimp_mulLiterals" (formula "19") (term "0,1,0,0,1,1")) + (rule "polySimp_elimOne" (formula "19") (term "0,1,0,0,1,1")) + (rule "polySimp_addAssoc" (formula "19") (term "0,0,1,1")) + (rule "polySimp_addAssoc" (formula "19") (term "0,1,1")) + (rule "polySimp_addComm1" (formula "19") (term "0,0,1,1")) + (rule "polySimp_pullOutFactor2b" (formula "19") (term "0,1,1")) + (rule "add_literals" (formula "19") (term "1,1,0,1,1")) + (rule "times_zero_1" (formula "19") (term "1,0,1,1")) + (rule "add_zero_right" (formula "19") (term "0,1,1")) + (rule "polySimp_addAssoc" (formula "19") (term "0,1,1")) + (rule "polySimp_addComm1" (formula "19") (term "0,0,1,1")) + (rule "add_literals" (formula "19") (term "0,0,0,1,1")) + (rule "add_zero_left" (formula "19") (term "0,0,1,1")) + (rule "polySimp_pullOutFactor1" (formula "19") (term "0,1,1")) + (rule "add_literals" (formula "19") (term "1,0,1,1")) + (rule "times_zero_1" (formula "19") (term "0,1,1")) + (rule "leq_literals" (formula "19") (term "1,1")) + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_commuteLeq" (formula "19") (term "0,0,1,0,0,1,0,0,0")) + (rule "replace_known_left" (formula "19") (term "0,0,1,0,0,1,0,0,0") (ifseqformula "3")) + (builtin "One Step Simplification" (formula "19")) + (rule "polySimp_addComm0" (formula "19") (term "0,0,1,0,0,0")) + (rule "inEqSimp_homoInEq1" (formula "19") (term "1,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,1,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "1,0,1,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "0,1,0,1,0,0")) + (rule "polySimp_addAssoc" (formula "19") (term "0,1,0,0")) + (rule "polySimp_addComm0" (formula "19") (term "0,0,1,0,0")) + (rule "inEqSimp_homoInEq1" (formula "19") (term "0,1,0,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,0,1,0,0,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "1,0,0,1,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "0,1,0,0,1,0,0,0,0")) + (rule "polySimp_addAssoc" (formula "19") (term "0,0,1,0,0,0,0")) + (rule "add_literals" (formula "19") (term "0,0,0,1,0,0,0,0")) + (rule "add_zero_left" (formula "19") (term "0,0,1,0,0,0,0")) + (rule "inEqSimp_homoInEq0" (formula "19") (term "1")) + (rule "mul_literals" (formula "19") (term "1,0,1")) + (rule "add_zero_right" (formula "19") (term "0,1")) + (rule "apply_eq_monomials" (formula "19") (term "1,0,1,0,0,0") (ifseqformula "7")) + (rule "polySimp_rightDist" (formula "19") (term "0,1,0,1,0,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "1,0,1,0,1,0,0,0")) + (rule "polySimp_pullOutFactor0b" (formula "19") (term "1,0,1,0,0,0")) + (rule "add_literals" (formula "19") (term "1,1,1,0,1,0,0,0")) + (rule "times_zero_1" (formula "19") (term "1,1,0,1,0,0,0")) + (rule "add_zero_right" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_addComm1" (formula "19") (term "0,1,0,0,0")) + (rule "polySimp_sepPosMonomial" (formula "19") (term "0,1,0,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "1,0,1,0,0,0,0,0")) + (rule "polySimp_sepPosMonomial" (formula "19") (term "1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,1,0,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "1,1,0,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "1,1,1,0,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "1,1,1,0,0,0")) + (rule "polySimp_mulAssoc" (formula "19") (term "0,1,1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "0,0,1,1,0,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "0,1,1,0,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "0,1,1,0,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "19") (term "0,0,0,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "1,0,0,0,0,0,0,0")) + (rule "inEqSimp_sepNegMonomial0" (formula "19") (term "1,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "0,1,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "0,1,0,0")) + (rule "inEqSimp_invertInEq0" (formula "19") (term "0,1,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "1,0,1,0,0,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "0,0,1,0,0,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "0,0,1,0,0,0,0")) + (rule "replace_known_left" (formula "19") (term "0,1,0,0,0,0") (ifseqformula "3")) + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_sepPosMonomial1" (formula "19") (term "1")) + (rule "polySimp_mulComm0" (formula "19") (term "1,1")) + (rule "polySimp_rightDist" (formula "19") (term "1,1")) + (rule "polySimp_mulLiterals" (formula "19") (term "1,1,1")) + (rule "mul_literals" (formula "19") (term "0,1,1")) + (rule "polySimp_elimOne" (formula "19") (term "1,1,1")) + (rule "replace_known_left" (formula "19") (term "1") (ifseqformula "2")) + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_contradEq7" (formula "19") (term "0,1,0,0,0,0") (ifseqformula "3")) + (rule "add_zero_left" (formula "19") (term "0,0,0,1,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "0,0,0,1,0,0,0,0")) + (rule "leq_literals" (formula "19") (term "0,0,1,0,0,0,0")) + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_subsumption1" (formula "19") (term "0,0,0,0,0") (ifseqformula "3")) + (rule "leq_literals" (formula "19") (term "0,0,0,0,0,0")) + (builtin "One Step Simplification" (formula "19")) + (rule "pullOutSelect" (formula "19") (term "1,1,1,0") (inst "selectSK=SumAndMax_sum_2:int")) + (rule "applyEq" (formula "20") (term "0,1,0,0") (ifseqformula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "0")) + (rule "applyEqReverse" (formula "20") (term "1,1,1,0") (ifseqformula "1")) + (rule "applyEqReverse" (formula "20") (term "0,1,0,0") (ifseqformula "1")) + (builtin "One Step Simplification" (formula "20")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "polySimp_addComm0" (formula "19") (term "1,1,0")) + (rule "pullOutSelect" (formula "19") (term "0,0,1,0") (inst "selectSK=SumAndMax_max_2:int")) + (rule "applyEq" (formula "20") (term "1,1,0,0,0,0") (ifseqformula "1")) + (rule "applyEq" (formula "20") (term "0,1,1,1,0") (ifseqformula "1")) + (rule "applyEq" (formula "20") (term "1,1,0,1,0,0") (ifseqformula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "0")) + (rule "applyEqReverse" (formula "20") (term "0,0,1,0") (ifseqformula "1")) + (rule "applyEqReverse" (formula "20") (term "1,1,0,0,0,0") (ifseqformula "1")) + (rule "applyEqReverse" (formula "20") (term "0,1,1,1,0") (ifseqformula "1")) + (rule "applyEqReverse" (formula "20") (term "1,1,0,1,0,0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "polySimp_addComm1" (formula "19") (term "1,1,0")) + (rule "polySimp_pullOutFactor1" (formula "19") (term "0,1,1,0")) + (rule "add_literals" (formula "19") (term "1,0,1,1,0")) + (rule "times_zero_1" (formula "19") (term "0,1,1,0")) + (rule "add_zero_left" (formula "19") (term "1,1,0")) + (rule "cut_direct" (formula "6") (term "0")) + (branch "CUT: k_0 >= 1 TRUE" + (builtin "One Step Simplification" (formula "7")) + (rule "exLeft" (formula "7") (inst "sk=i_0:int")) + (rule "andLeft" (formula "7")) + (rule "andLeft" (formula "7")) + (rule "inEqSimp_homoInEq0" (formula "8")) + (rule "polySimp_addComm1" (formula "8") (term "0")) + (rule "inEqSimp_sepPosMonomial1" (formula "8")) + (rule "polySimp_mulComm0" (formula "8") (term "1")) + (rule "polySimp_rightDist" (formula "8") (term "1")) + (rule "polySimp_mulLiterals" (formula "8") (term "1,1")) + (rule "mul_literals" (formula "8") (term "0,1")) + (rule "polySimp_elimOne" (formula "8") (term "1,1")) + (rule "inEqSimp_contradEq7" (formula "5") (term "0") (ifseqformula "6")) + (rule "mul_literals" (formula "5") (term "1,0,0,0")) + (rule "add_zero_right" (formula "5") (term "0,0,0")) + (rule "leq_literals" (formula "5") (term "0,0")) + (builtin "One Step Simplification" (formula "5")) + (rule "true_left" (formula "5")) + (rule "inEqSimp_subsumption1" (formula "3") (ifseqformula "5")) + (rule "leq_literals" (formula "3") (term "0")) + (builtin "One Step Simplification" (formula "3")) + (rule "true_left" (formula "3")) + (rule "pullOutSelect" (formula "7") (term "0") (inst "selectSK=arr_1:int")) + (rule "simplifySelectOfAnon" (formula "7")) + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "20"))) + (rule "eqSymm" (formula "8")) + (rule "applyEqReverse" (formula "7") (term "1") (ifseqformula "8")) + (rule "hideAuxiliaryEq" (formula "8")) + (rule "dismissNonSelectedField" (formula "7") (term "2,0")) + (rule "dismissNonSelectedField" (formula "7") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "7") (term "2,0")) + (rule "dismissNonSelectedField" (formula "7") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "7") (term "0,1,0,0") (ifseqformula "14")) + (builtin "One Step Simplification" (formula "7")) + (rule "elementOfUnion" (formula "7") (term "0,0")) + (rule "elementOfSingleton" (formula "7") (term "0,0,0")) + (builtin "One Step Simplification" (formula "7")) + (rule "elementOfSingleton" (formula "7") (term "0,0")) + (builtin "One Step Simplification" (formula "7")) + (rule "eqSymm" (formula "7")) + (rule "applyEq" (formula "3") (term "1,1,0") (ifseqformula "7")) + (rule "applyEq" (formula "1") (term "0") (ifseqformula "7")) + (rule "inEqSimp_homoInEq0" (formula "1")) + (rule "polySimp_addComm1" (formula "1") (term "0")) + (rule "applyEq" (formula "9") (term "0,0") (ifseqformula "7")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "polySimp_mulComm0" (formula "1") (term "1")) + (rule "polySimp_rightDist" (formula "1") (term "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) + (rule "mul_literals" (formula "1") (term "0,1")) + (rule "polySimp_elimOne" (formula "1") (term "1,1")) + (rule "allLeft" (formula "17") (inst "t=k_0:int")) + (rule "inEqSimp_commuteGeq" (formula "17") (term "1,0")) + (rule "inEqSimp_contradInEq1" (formula "17") (term "1,0") (ifseqformula "2")) + (rule "inEqSimp_homoInEq1" (formula "17") (term "0,1,0")) + (rule "polySimp_pullOutFactor1b" (formula "17") (term "0,0,1,0")) + (rule "add_literals" (formula "17") (term "1,1,0,0,1,0")) + (rule "times_zero_1" (formula "17") (term "1,0,0,1,0")) + (rule "add_literals" (formula "17") (term "0,0,1,0")) + (rule "leq_literals" (formula "17") (term "0,1,0")) + (builtin "One Step Simplification" (formula "17")) + (rule "inEqSimp_contradInEq1" (formula "17") (term "0") (ifseqformula "4")) + (rule "qeq_literals" (formula "17") (term "0,0")) + (builtin "One Step Simplification" (formula "17")) + (rule "andRight" (formula "21")) + (branch + (rule "allLeft" (formula "3") (inst "t=i_0:int")) + (rule "replaceKnownSelect_taclet0000000001_14" (formula "3") (term "0,1")) + (rule "replaceKnownAuxiliaryConstant_taclet0000000001_15" (formula "3") (term "0,1")) + (rule "inEqSimp_commuteGeq" (formula "3") (term "1,0")) + (rule "applyEq" (formula "3") (term "0,1") (ifseqformula "8")) + (rule "inEqSimp_homoInEq0" (formula "3") (term "1")) + (rule "polySimp_pullOutFactor1" (formula "3") (term "0,1")) + (rule "add_literals" (formula "3") (term "1,0,1")) + (rule "times_zero_1" (formula "3") (term "0,1")) + (rule "qeq_literals" (formula "3") (term "1")) + (builtin "One Step Simplification" (formula "3")) + (rule "true_left" (formula "3")) + (rule "andRight" (formula "21")) + (branch + (rule "andRight" (formula "21")) + (branch + (rule "allRight" (formula "21") (inst "sk=i_10:int")) + (rule "orRight" (formula "21")) + (rule "orRight" (formula "21")) + (rule "inEqSimp_leqRight" (formula "23")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) + (rule "inEqSimp_leqRight" (formula "22")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_geqRight" (formula "23")) + (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) + (rule "mul_literals" (formula "1") (term "0,1,0,0")) + (rule "polySimp_addAssoc" (formula "1") (term "0,0")) + (rule "add_literals" (formula "1") (term "0,0,0")) + (rule "add_zero_left" (formula "1") (term "0,0")) + (rule "polySimp_addComm0" (formula "1") (term "0")) + (rule "inEqSimp_sepPosMonomial1" (formula "3")) + (rule "polySimp_mulComm0" (formula "3") (term "1")) + (rule "polySimp_rightDist" (formula "3") (term "1")) + (rule "mul_literals" (formula "3") (term "0,1")) + (rule "polySimp_mulLiterals" (formula "3") (term "1,1")) + (rule "polySimp_elimOne" (formula "3") (term "1,1")) + (rule "inEqSimp_sepNegMonomial0" (formula "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "0")) + (rule "polySimp_elimOne" (formula "1") (term "0")) + (rule "pullOutSelect" (formula "3") (term "0") (inst "selectSK=arr_2:int")) + (rule "simplifySelectOfAnon" (formula "3")) + (builtin "One Step Simplification" (formula "3") (ifInst "" (formula "24"))) + (rule "dismissNonSelectedField" (formula "3") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "3") (term "2,0")) + (rule "dismissNonSelectedField" (formula "3") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "3") (term "0,1,0,0") (ifseqformula "18")) + (builtin "One Step Simplification" (formula "3")) + (rule "dismissNonSelectedField" (formula "3") (term "2,0")) + (rule "inEqSimp_homoInEq1" (formula "4")) + (rule "polySimp_addComm1" (formula "4") (term "0")) + (rule "inEqSimp_sepPosMonomial0" (formula "4")) + (rule "polySimp_mulComm0" (formula "4") (term "1")) + (rule "polySimp_rightDist" (formula "4") (term "1")) + (rule "polySimp_mulLiterals" (formula "4") (term "1,1")) + (rule "mul_literals" (formula "4") (term "0,1")) + (rule "polySimp_elimOne" (formula "4") (term "1,1")) + (rule "elementOfUnion" (formula "3") (term "0,0")) + (rule "elementOfSingleton" (formula "3") (term "0,0,0")) + (builtin "One Step Simplification" (formula "3")) + (rule "elementOfSingleton" (formula "3") (term "0,0")) + (builtin "One Step Simplification" (formula "3")) + (rule "applyEqReverse" (formula "4") (term "1,1") (ifseqformula "3")) + (rule "hideAuxiliaryEq" (formula "3")) + (rule "inEqSimp_exactShadow3" (formula "4") (ifseqformula "3")) + (rule "polySimp_rightDist" (formula "4") (term "0,0")) + (rule "mul_literals" (formula "4") (term "0,0,0")) + (rule "polySimp_addAssoc" (formula "4") (term "0")) + (rule "polySimp_addComm1" (formula "4") (term "0,0")) + (rule "add_literals" (formula "4") (term "0,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "4")) + (rule "polySimp_mulComm0" (formula "4") (term "1")) + (rule "polySimp_rightDist" (formula "4") (term "1")) + (rule "polySimp_mulLiterals" (formula "4") (term "1,1")) + (rule "mul_literals" (formula "4") (term "0,1")) + (rule "polySimp_elimOne" (formula "4") (term "1,1")) + (rule "inEqSimp_exactShadow3" (formula "21") (ifseqformula "3")) + (rule "mul_literals" (formula "21") (term "0,0")) + (rule "add_zero_left" (formula "21") (term "0")) + (rule "inEqSimp_sepPosMonomial1" (formula "21")) + (rule "mul_literals" (formula "21") (term "1")) + (rule "allLeft" (formula "23") (inst "t=i_0:int")) + (rule "inEqSimp_commuteGeq" (formula "23") (term "1,0")) + (rule "inEqSimp_contradInEq1" (formula "23") (term "0,0") (ifseqformula "9")) + (rule "qeq_literals" (formula "23") (term "0,0,0")) + (builtin "One Step Simplification" (formula "23")) + (rule "cut_direct" (formula "23") (term "0")) + (branch "CUT: a.length <= i_0 TRUE" + (builtin "One Step Simplification" (formula "24")) + (rule "true_left" (formula "24")) + (rule "inEqSimp_exactShadow3" (formula "20") (ifseqformula "23")) + (rule "mul_literals" (formula "20") (term "0,0")) + (rule "add_zero_left" (formula "20") (term "0")) + (rule "inEqSimp_exactShadow3" (formula "6") (ifseqformula "23")) + (rule "polySimp_rightDist" (formula "6") (term "0,0")) + (rule "mul_literals" (formula "6") (term "0,0,0")) + (rule "polySimp_addComm1" (formula "6") (term "0")) + (rule "inEqSimp_sepNegMonomial1" (formula "6")) + (rule "polySimp_mulLiterals" (formula "6") (term "0")) + (rule "polySimp_elimOne" (formula "6") (term "0")) + (rule "inEqSimp_contradInEq1" (formula "6") (ifseqformula "11")) + (rule "andLeft" (formula "6")) + (rule "inEqSimp_homoInEq1" (formula "6")) + (rule "polySimp_mulComm0" (formula "6") (term "1,0")) + (rule "polySimp_rightDist" (formula "6") (term "1,0")) + (rule "mul_literals" (formula "6") (term "0,1,0")) + (rule "polySimp_addAssoc" (formula "6") (term "0")) + (rule "polySimp_addComm1" (formula "6") (term "0,0")) + (rule "add_literals" (formula "6") (term "0,0,0")) + (rule "polySimp_pullOutFactor1b" (formula "6") (term "0")) + (rule "add_literals" (formula "6") (term "1,1,0")) + (rule "times_zero_1" (formula "6") (term "1,0")) + (rule "add_literals" (formula "6") (term "0")) + (rule "leq_literals" (formula "6")) + (rule "closeFalse" (formula "6")) + ) + (branch "CUT: a.length <= i_0 FALSE" + (builtin "One Step Simplification" (formula "23")) + (rule "inEqSimp_leqRight" (formula "25")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "polySimp_mulComm0" (formula "1") (term "1")) + (rule "polySimp_rightDist" (formula "1") (term "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) + (rule "mul_literals" (formula "1") (term "0,1")) + (rule "polySimp_elimOne" (formula "1") (term "1,1")) + (rule "allLeft" (formula "8") (inst "t=i_10:int")) + (rule "replaceKnownSelect_taclet0000000000001_16" (formula "8") (term "0,1")) + (rule "replaceKnownAuxiliaryConstant_taclet0000000000001_17" (formula "8") (term "0,1")) + (rule "inEqSimp_commuteGeq" (formula "8") (term "1,0")) + (rule "inEqSimp_contradInEq1" (formula "8") (term "0,0") (ifseqformula "3")) + (rule "qeq_literals" (formula "8") (term "0,0,0")) + (builtin "One Step Simplification" (formula "8")) + (rule "inEqSimp_contradInEq1" (formula "8") (term "1") (ifseqformula "5")) + (rule "inEqSimp_homoInEq1" (formula "8") (term "0,1")) + (rule "polySimp_pullOutFactor1b" (formula "8") (term "0,0,1")) + (rule "add_literals" (formula "8") (term "1,1,0,0,1")) + (rule "times_zero_1" (formula "8") (term "1,0,0,1")) + (rule "add_literals" (formula "8") (term "0,0,1")) + (rule "leq_literals" (formula "8") (term "0,1")) + (builtin "One Step Simplification" (formula "8")) + (rule "inEqSimp_antiSymm" (formula "2") (ifseqformula "8")) + (rule "applyEqRigid" (formula "9") (term "0") (ifseqformula "2")) + (rule "inEqSimp_homoInEq0" (formula "9")) + (rule "polySimp_pullOutFactor1" (formula "9") (term "0")) + (rule "add_literals" (formula "9") (term "1,0")) + (rule "times_zero_1" (formula "9") (term "0")) + (rule "qeq_literals" (formula "9")) + (rule "true_left" (formula "9")) + (rule "applyEq" (formula "10") (term "0") (ifseqformula "2")) + (rule "applyEq" (formula "5") (term "0,2,0") (ifseqformula "2")) + (rule "inEqSimp_homoInEq0" (formula "5")) + (rule "polySimp_pullOutFactor1b" (formula "5") (term "0")) + (rule "add_literals" (formula "5") (term "1,1,0")) + (rule "times_zero_1" (formula "5") (term "1,0")) + (rule "add_literals" (formula "5") (term "0")) + (rule "qeq_literals" (formula "5")) + (rule "closeFalse" (formula "5")) + ) + ) + (branch + (rule "nnf_ex2all" (formula "21")) + (rule "nnf_notAnd" (formula "1") (term "0")) + (rule "nnf_notAnd" (formula "1") (term "0,0")) + (rule "inEqSimp_notLeq" (formula "1") (term "1,0,0")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0,1,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1") (term "1,0,0")) + (rule "polySimp_mulComm0" (formula "1") (term "1,1,0,0")) + (rule "polySimp_rightDist" (formula "1") (term "1,1,0,0")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1,1,0,0")) + (rule "mul_literals" (formula "1") (term "0,1,1,0,0")) + (rule "polySimp_elimOne" (formula "1") (term "1,1,1,0,0")) + (rule "inEqSimp_notGeq" (formula "1") (term "0,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,0,0,0")) + (rule "add_literals" (formula "1") (term "0,0,0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "0,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,0")) + (rule "allLeft" (formula "1") (inst "t=k_0:int")) + (rule "replaceKnownSelect_taclet0001_5" (formula "1") (term "0,0,1")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_7" (formula "1") (term "0,0,1")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_homoInEq1" (formula "1") (term "1")) + (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,1")) + (rule "add_literals" (formula "1") (term "1,1,0,1")) + (rule "times_zero_1" (formula "1") (term "1,0,1")) + (rule "add_literals" (formula "1") (term "0,1")) + (rule "leq_literals" (formula "1") (term "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "6")) + (rule "qeq_literals" (formula "1") (term "0")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) + (branch + (rule "inEqSimp_geqRight" (formula "21")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1")) + (rule "polySimp_mulComm0" (formula "1") (term "1")) + (rule "polySimp_rightDist" (formula "1") (term "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) + (rule "mul_literals" (formula "1") (term "0,1")) + (rule "polySimp_elimOne" (formula "1") (term "1,1")) + (rule "allLeft" (formula "19") (inst "t=i_0:int")) + (rule "inEqSimp_commuteGeq" (formula "19") (term "1,0")) + (rule "inEqSimp_contradInEq1" (formula "19") (term "0,0") (ifseqformula "6")) + (rule "qeq_literals" (formula "19") (term "0,0,0")) + (builtin "One Step Simplification" (formula "19")) + (rule "cut_direct" (formula "19") (term "0")) + (branch "CUT: a.length <= i_0 TRUE" + (builtin "One Step Simplification" (formula "20")) + (rule "true_left" (formula "20")) + (rule "inEqSimp_exactShadow3" (formula "3") (ifseqformula "19")) + (rule "polySimp_rightDist" (formula "3") (term "0,0")) + (rule "mul_literals" (formula "3") (term "0,0,0")) + (rule "polySimp_addComm1" (formula "3") (term "0")) + (rule "inEqSimp_sepNegMonomial1" (formula "3")) + (rule "polySimp_mulLiterals" (formula "3") (term "0")) + (rule "polySimp_elimOne" (formula "3") (term "0")) + (rule "inEqSimp_contradInEq0" (formula "8") (ifseqformula "3")) + (rule "andLeft" (formula "8")) + (rule "inEqSimp_homoInEq1" (formula "8")) + (rule "polySimp_mulComm0" (formula "8") (term "1,0")) + (rule "polySimp_rightDist" (formula "8") (term "1,0")) + (rule "mul_literals" (formula "8") (term "0,1,0")) + (rule "polySimp_addAssoc" (formula "8") (term "0")) + (rule "polySimp_addComm1" (formula "8") (term "0,0")) + (rule "add_literals" (formula "8") (term "0,0,0")) + (rule "polySimp_pullOutFactor1b" (formula "8") (term "0")) + (rule "add_literals" (formula "8") (term "1,1,0")) + (rule "times_zero_1" (formula "8") (term "1,0")) + (rule "add_literals" (formula "8") (term "0")) + (rule "leq_literals" (formula "8")) + (rule "closeFalse" (formula "8")) + ) + (branch "CUT: a.length <= i_0 FALSE" + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_leqRight" (formula "21")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "polySimp_mulComm0" (formula "1") (term "1")) + (rule "polySimp_rightDist" (formula "1") (term "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) + (rule "mul_literals" (formula "1") (term "0,1")) + (rule "polySimp_elimOne" (formula "1") (term "1,1")) + (rule "sign_case_distinction" (inst "signCasesLeft=length(a)")) + (branch "a.length is negative" + (rule "inEqSimp_contradInEq0" (formula "19") (ifseqformula "1")) + (rule "qeq_literals" (formula "19") (term "0")) + (builtin "One Step Simplification" (formula "19")) + (rule "closeFalse" (formula "19")) + ) + (branch "a.length is zero" + (rule "applyEq" (formula "19") (term "0") (ifseqformula "1")) + (rule "qeq_literals" (formula "19")) + (rule "true_left" (formula "19")) + (rule "applyEq" (formula "21") (term "1,1,0,0") (ifseqformula "1")) + (rule "applyEq" (formula "2") (term "0") (ifseqformula "1")) + (rule "inEqSimp_homoInEq1" (formula "2")) + (rule "mul_literals" (formula "2") (term "1,0")) + (rule "add_zero_right" (formula "2") (term "0")) + (rule "applyEq" (formula "5") (term "0") (ifseqformula "1")) + (rule "inEqSimp_homoInEq1" (formula "5")) + (rule "mul_literals" (formula "5") (term "1,0")) + (rule "add_zero_right" (formula "5") (term "0")) + (rule "inEqSimp_sepPosMonomial0" (formula "2")) + (rule "mul_literals" (formula "2") (term "1")) + (rule "inEqSimp_sepPosMonomial0" (formula "5")) + (rule "mul_literals" (formula "5") (term "1")) + (rule "inEqSimp_contradInEq0" (formula "7") (ifseqformula "5")) + (rule "qeq_literals" (formula "7") (term "0")) + (builtin "One Step Simplification" (formula "7")) + (rule "closeFalse" (formula "7")) + ) + (branch "a.length is positive" + (rule "inEqSimp_subsumption1" (formula "19") (ifseqformula "1")) + (rule "leq_literals" (formula "19") (term "0")) + (builtin "One Step Simplification" (formula "19")) + (rule "true_left" (formula "19")) + (rule "multiply_2_inEq3" (formula "4") (ifseqformula "7")) + (rule "polySimp_elimOne" (formula "4") (term "0,0,1")) + (rule "polySimp_elimOne" (formula "4") (term "1,1")) + (rule "polySimp_elimNeg" (formula "4") (term "0,0,1")) + (rule "polySimp_mulComm0" (formula "4") (term "1,0,1")) + (rule "polySimp_mulComm0" (formula "4") (term "0,0,1")) + (rule "polySimp_rightDist" (formula "4") (term "1,0,1")) + (rule "polySimp_elimOne" (formula "4") (term "0,1,0,1")) + (rule "polySimp_rightDist" (formula "4") (term "0,0,1")) + (rule "mul_literals" (formula "4") (term "0,0,0,1")) + (rule "polySimp_addAssoc" (formula "4") (term "0,1")) + (rule "polySimp_addComm1" (formula "4") (term "1")) + (rule "polySimp_addComm1" (formula "4") (term "0,0,1")) + (rule "inEqSimp_exactShadow3" (formula "4") (ifseqformula "3")) + (rule "polySimp_rightDist" (formula "4") (term "0,0")) + (rule "polySimp_addComm1" (formula "4") (term "0")) + (rule "polySimp_rightDist" (formula "4") (term "0,0,0")) + (rule "polySimp_rightDist" (formula "4") (term "0,0,0,0")) + (rule "polySimp_mulLiterals" (formula "4") (term "1,0,0,0,0")) + (rule "polySimp_elimOne" (formula "4") (term "1,0,0,0,0")) + (rule "polySimp_rightDist" (formula "4") (term "0,0,0,0,0")) + (rule "mul_literals" (formula "4") (term "0,0,0,0,0,0")) + (rule "polySimp_addAssoc" (formula "4") (term "0,0")) + (rule "polySimp_addComm1" (formula "4") (term "0,0,0")) + (rule "polySimp_addComm1" (formula "4") (term "0,0,0,0")) + (rule "polySimp_addComm1" (formula "4") (term "0,0,0,0,0")) + (rule "add_literals" (formula "4") (term "0,0,0,0,0,0")) + (rule "add_zero_left" (formula "4") (term "0,0,0,0,0")) + (rule "inEqSimp_sepNegMonomial1" (formula "4")) + (rule "polySimp_mulLiterals" (formula "4") (term "0")) + (rule "polySimp_elimOne" (formula "4") (term "0")) + (rule "inEqSimp_exactShadow3" (formula "14") (ifseqformula "4")) + (rule "polySimp_mulComm0" (formula "14") (term "0,0")) + (rule "polySimp_addAssoc" (formula "14") (term "0")) + (rule "polySimp_addComm0" (formula "14") (term "0,0")) + (rule "polySimp_pullOutFactor2b" (formula "14") (term "0")) + (rule "add_literals" (formula "14") (term "1,1,0")) + (rule "times_zero_1" (formula "14") (term "1,0")) + (rule "add_zero_right" (formula "14") (term "0")) + (rule "inEqSimp_sepNegMonomial1" (formula "14")) + (rule "polySimp_mulLiterals" (formula "14") (term "0")) + (rule "polySimp_elimOne" (formula "14") (term "0")) + (rule "inEqSimp_exactShadow3" (formula "6") (ifseqformula "14")) + (rule "polySimp_rightDist" (formula "6") (term "0,0")) + (rule "mul_literals" (formula "6") (term "0,0,0")) + (rule "polySimp_addAssoc" (formula "6") (term "0")) + (rule "polySimp_addComm1" (formula "6") (term "0,0")) + (rule "polySimp_pullOutFactor2b" (formula "6") (term "0")) + (rule "add_literals" (formula "6") (term "1,1,0")) + (rule "times_zero_1" (formula "6") (term "1,0")) + (rule "add_zero_right" (formula "6") (term "0")) + (rule "inEqSimp_sepNegMonomial1" (formula "6")) + (rule "polySimp_mulLiterals" (formula "6") (term "0")) + (rule "polySimp_elimOne" (formula "6") (term "0")) + (rule "inEqSimp_contradInEq1" (formula "6") (ifseqformula "10")) + (rule "qeq_literals" (formula "6") (term "0")) + (builtin "One Step Simplification" (formula "6")) + (rule "closeFalse" (formula "6")) + ) + ) + ) + ) + (branch + (rule "allRight" (formula "21") (inst "sk=f_0:Field")) + (rule "allRight" (formula "21") (inst "sk=o_0:java.lang.Object")) + (rule "orRight" (formula "21")) + (rule "orRight" (formula "21")) + (rule "orRight" (formula "21")) + (rule "pullOutSelect" (formula "24") (term "0") (inst "selectSK=f_0_0:any")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "25")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "22")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "23")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "replace_known_right" (formula "1") (term "1,0,0") (ifseqformula "24")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0,0")) + (rule "elementOfSingleton" (formula "1") (term "1,0,0,0")) + (rule "replace_known_right" (formula "1") (term "1,0,0,0") (ifseqformula "22")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0,0") (ifseqformula "23")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "25"))) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "CUT: k_0 >= 1 FALSE" + (builtin "One Step Simplification" (formula "6")) + (rule "true_left" (formula "6")) + (rule "inEqSimp_geqRight" (formula "16")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_antiSymm" (formula "4") (ifseqformula "1")) + (rule "replace_known_left" (formula "7") (term "0") (ifseqformula "4")) + (builtin "One Step Simplification" (formula "7")) + (rule "applyEqRigid" (formula "6") (term "1,1,0,0") (ifseqformula "4")) + (rule "applyEqRigid" (formula "8") (term "1,0") (ifseqformula "4")) + (rule "bsum_lower_equals_upper" (formula "8") (term "0")) + (rule "eqSymm" (formula "8")) + (rule "applyEqRigid" (formula "20") (term "0,2,3,0,0,0,1,0,0,1") (ifseqformula "4")) + (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "4")) + (rule "leq_literals" (formula "1")) + (rule "true_left" (formula "1")) + (rule "applyEqRigid" (formula "1") (term "0,2,1,1") (ifseqformula "3")) + (rule "applyEqRigid" (formula "4") (term "0") (ifseqformula "3")) + (rule "qeq_literals" (formula "4")) + (rule "true_left" (formula "4")) + (rule "applyEq" (formula "7") (term "0,0") (ifseqformula "5")) + (rule "times_zero_2" (formula "7") (term "0")) + (rule "inEqSimp_commuteGeq" (formula "7")) + (rule "applyEq" (formula "2") (term "1,1") (ifseqformula "3")) + (rule "add_zero_right" (formula "2") (term "1")) + (rule "applyEq" (formula "1") (term "0") (ifseqformula "5")) + (rule "inEqSimp_homoInEq0" (formula "1")) + (rule "mul_literals" (formula "1") (term "1,0")) + (rule "add_zero_right" (formula "1") (term "0")) + (rule "applyEq" (formula "18") (term "0,2,1,1,0,0,0,0") (ifseqformula "3")) + (rule "applyEq" (formula "18") (term "1,0,1,0") (ifseqformula "3")) + (rule "times_zero_1" (formula "18") (term "0,1,0")) + (rule "inEqSimp_commuteGeq" (formula "18") (term "1,0")) + (rule "replace_known_left" (formula "18") (term "1,0") (ifseqformula "7")) + (builtin "One Step Simplification" (formula "18")) + (rule "applyEq" (formula "4") (term "1,1,0") (ifseqformula "5")) + (rule "applyEq" (formula "18") (term "1,1,1,0,0,0,0") (ifseqformula "3")) + (rule "add_zero_right" (formula "18") (term "1,1,0,0,0,0")) + (rule "applyEq" (formula "18") (term "1,3,0,0,1,0,0,1") (ifseqformula "6")) + (rule "add_zero_right" (formula "18") (term "3,0,0,1,0,0,1")) + (rule "applyEq" (formula "18") (term "1,1,0,0,1,0") (ifseqformula "3")) + (rule "applyEq" (formula "7") (term "0") (ifseqformula "6")) + (rule "leq_literals" (formula "7")) + (rule "true_left" (formula "7")) + (rule "applyEq" (formula "17") (term "0,2,3,0,0,1,0,0,1") (ifseqformula "3")) + (rule "applyEq" (formula "17") (term "0,2,1,1,0,1,0") (ifseqformula "3")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "mul_literals" (formula "1") (term "1")) + (rule "inEqSimp_subsumption1" (formula "13") (ifseqformula "2")) + (rule "leq_literals" (formula "13") (term "0")) + (builtin "One Step Simplification" (formula "13")) + (rule "true_left" (formula "13")) + (rule "inEqSimp_or_tautInEq0" (formula "4") (term "0,0")) + (rule "add_zero_right" (formula "4") (term "1,1,0,0")) + (rule "qeq_literals" (formula "4") (term "1,0,0")) + (builtin "One Step Simplification" (formula "4")) + (rule "true_left" (formula "4")) + (rule "inEqSimp_or_antiSymm0" (formula "15") (term "0,0,0,0")) + (rule "add_literals" (formula "15") (term "1,0,1,0,0,0,0")) + (rule "add_literals" (formula "15") (term "0,0,0,0,0,0")) + (builtin "One Step Simplification" (formula "15")) + (rule "andRight" (formula "15")) + (branch + (rule "andRight" (formula "15")) + (branch + (rule "allRight" (formula "15") (inst "sk=i_0:int")) + (rule "orRight" (formula "15")) + (rule "notRight" (formula "15")) + (rule "inEqSimp_leqRight" (formula "16")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) + (rule "applyEq" (formula "1") (term "0,2,1,0") (ifseqformula "2")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "polySimp_mulComm0" (formula "1") (term "1")) + (rule "polySimp_rightDist" (formula "1") (term "1")) + (rule "mul_literals" (formula "1") (term "0,1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) + (rule "polySimp_elimOne" (formula "1") (term "1,1")) + (rule "pullOutSelect" (formula "1") (term "0") (inst "selectSK=arr_1:int")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "13")) + (builtin "One Step Simplification" (formula "1")) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "inEqSimp_homoInEq1" (formula "2")) + (rule "polySimp_addComm1" (formula "2") (term "0")) + (rule "inEqSimp_sepPosMonomial0" (formula "2")) + (rule "polySimp_mulComm0" (formula "2") (term "1")) + (rule "polySimp_rightDist" (formula "2") (term "1")) + (rule "polySimp_mulLiterals" (formula "2") (term "1,1")) + (rule "mul_literals" (formula "2") (term "0,1")) + (rule "polySimp_elimOne" (formula "2") (term "1,1")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "1,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "2") (term "1,1") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "inEqSimp_homoInEq0" (formula "1")) + (rule "polySimp_pullOutFactor1b" (formula "1") (term "0")) + (rule "add_literals" (formula "1") (term "1,1,0")) + (rule "times_zero_1" (formula "1") (term "1,0")) + (rule "add_literals" (formula "1") (term "0")) + (rule "qeq_literals" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + (branch + (rule "nnf_ex2all" (formula "15")) + (rule "nnf_notAnd" (formula "1") (term "0")) + (rule "nnf_notAnd" (formula "1") (term "0,0")) + (rule "inEqSimp_notGeq" (formula "1") (term "0,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,0,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0,0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "0,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,0")) + (rule "inEqSimp_notLeq" (formula "1") (term "1,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,1,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0,1,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1") (term "1,0,0")) + (rule "mul_literals" (formula "1") (term "1,1,0,0")) + (rule "inEqSimp_or_antiSymm0" (formula "1") (term "0,0")) + (rule "add_literals" (formula "1") (term "0,0,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "add_literals" (formula "1") (term "1,0,0,0")) + (rule "commute_or" (formula "1") (term "0")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "pullOutSelect" (formula "13") (term "0") (inst "selectSK=arr_1:int")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "16"))) + (rule "eqSymm" (formula "14")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "1")) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "14"))) + (rule "closeFalse" (formula "1")) + ) + ) + (branch + (rule "allRight" (formula "15") (inst "sk=f_0:Field")) + (rule "allRight" (formula "15") (inst "sk=o_0:java.lang.Object")) + (rule "orRight" (formula "15")) + (rule "orRight" (formula "15")) + (rule "orRight" (formula "15")) + (rule "pullOutSelect" (formula "18") (term "1") (inst "selectSK=f_0_0:any")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "17")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "16")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "19") (term "1") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "pullOutSelect" (formula "18") (term "0") (inst "selectSK=f_0_1:any")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "19")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "16")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "17")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "replaceKnownSelect_taclet11000000001_14" (formula "1") (term "2,0")) + (rule "replaceKnownAuxiliaryConstant_taclet11000000001_16" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "replace_known_right" (formula "1") (term "1,0,0") (ifseqformula "18")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0,0")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0,0,0") (ifseqformula "17")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0,0") (ifseqformula "16")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "19"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Null Reference (s_1 = null)" + (builtin "One Step Simplification" (formula "20")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "18"))) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "Null Reference (k < _a.length = null)" + (rule "false_right" (formula "21")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "20"))) + (rule "closeFalse" (formula "1")) + ) + (branch "Index Out of Bounds (k < _a.length != null, but k < _a.length Out of Bounds!)" + (rule "false_right" (formula "21")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "20"))) + (rule "inEqSimp_ltToLeq" (formula "1") (term "1")) + (rule "mul_literals" (formula "1") (term "1,0,0,1")) + (rule "add_literals" (formula "1") (term "0,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "1")) + (rule "mul_literals" (formula "1") (term "1,1")) + (rule "inEqSimp_contradInEq1" (formula "1") (term "1") (ifseqformula "5")) + (rule "qeq_literals" (formula "1") (term "0,1")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "4")) + (rule "andLeft" (formula "1")) + (rule "inEqSimp_homoInEq1" (formula "1")) + (rule "polySimp_pullOutFactor1b" (formula "1") (term "0")) + (rule "add_literals" (formula "1") (term "1,1,0")) + (rule "times_zero_1" (formula "1") (term "1,0")) + (rule "add_literals" (formula "1") (term "0")) + (rule "leq_literals" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "Null Reference (s = null)" + (builtin "One Step Simplification" (formula "20")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "18"))) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "Null Reference (k < _a.length = null)" + (rule "false_right" (formula "20")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "19"))) + (rule "closeFalse" (formula "1")) + ) + (branch "Index Out of Bounds (k < _a.length != null, but k < _a.length Out of Bounds!)" + (rule "false_right" (formula "20")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "19"))) + (rule "inEqSimp_ltToLeq" (formula "1") (term "1")) + (rule "mul_literals" (formula "1") (term "1,0,0,1")) + (rule "add_zero_right" (formula "1") (term "0,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "1")) + (rule "mul_literals" (formula "1") (term "1,1")) + (rule "inEqSimp_contradInEq1" (formula "1") (term "1") (ifseqformula "4")) + (rule "qeq_literals" (formula "1") (term "0,1")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "3")) + (rule "andLeft" (formula "1")) + (rule "inEqSimp_homoInEq1" (formula "1")) + (rule "polySimp_pullOutFactor1b" (formula "1") (term "0")) + (rule "add_literals" (formula "1") (term "1,1,0")) + (rule "times_zero_1" (formula "1") (term "1,0")) + (rule "add_zero_right" (formula "1") (term "0")) + (rule "leq_literals" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "if this.max < _a[k] false" + (builtin "One Step Simplification" (formula "19")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "inEqSimp_leqRight" (formula "16")) + (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) + (rule "mul_literals" (formula "1") (term "0,1,0,0")) + (rule "polySimp_addAssoc" (formula "1") (term "0,0")) + (rule "add_literals" (formula "1") (term "0,0,0")) + (rule "add_zero_left" (formula "1") (term "0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1")) + (rule "polySimp_elimOne" (formula "1") (term "1")) + (rule "compound_assignment_op_plus_attr" (formula "19") (term "1") (inst "#v=s")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "s")) + (rule "assignment" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "eval_order_access4" (formula "19") (term "1") (inst "#v0=s_1") (inst "#v1=i_4")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "s_1")) + (rule "assignment" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_4")) + (rule "compound_int_cast_expression" (formula "19") (term "1") (inst "#v=i_5")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_5")) + (rule "remove_parentheses_right" (formula "19") (term "1")) + (rule "compound_addition_2" (formula "19") (term "1") (inst "#v0=i_6") (inst "#v1=i_7")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_6")) + (rule "assignment_read_attribute" (formula "19")) + (branch "Normal Execution (s != null)" + (builtin "One Step Simplification" (formula "19")) + (rule "pullOutSelect" (formula "19") (term "0,1,0") (inst "selectSK=SumAndMax_sum_1:int")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "18"))) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "12")) + (builtin "One Step Simplification" (formula "1")) + (rule "variableDeclarationAssign" (formula "20") (term "1")) + (rule "variableDeclaration" (formula "20") (term "1") (newnames "i_7")) + (rule "assignment_array2" (formula "20")) + (branch "Normal Execution (k < _a.length != null)" + (builtin "One Step Simplification" (formula "20")) + (rule "replaceKnownSelect_taclet0001_5" (formula "20") (term "0,1,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_7" (formula "20") (term "0,1,0")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "1,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "20") (term "0,1,0,0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "assignmentAdditionInt" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "translateJavaAddInt" (formula "19") (term "0,1,0")) + (rule "polySimp_addComm0" (formula "19") (term "0,1,0")) + (rule "widening_identity_cast_5" (formula "19") (term "1")) + (rule "assignment" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "assignment_write_attribute" (formula "19")) + (branch "Normal Execution (s_1 != null)" + (builtin "One Step Simplification" (formula "19")) + (rule "postincrement" (formula "19") (term "1")) + (rule "compound_int_cast_expression" (formula "19") (term "1") (inst "#v=i_8")) + (rule "variableDeclarationAssign" (formula "19") (term "1")) + (rule "variableDeclaration" (formula "19") (term "1") (newnames "i_8")) + (rule "remove_parentheses_right" (formula "19") (term "1")) + (rule "assignmentAdditionInt" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "translateJavaAddInt" (formula "19") (term "0,1,0")) + (rule "polySimp_addComm0" (formula "19") (term "0,1,0")) + (rule "widening_identity_cast_5" (formula "19") (term "1")) + (rule "assignment" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19")) + (rule "blockEmpty" (formula "19") (term "1")) + (rule "lsContinue" (formula "19") (term "1")) + (builtin "One Step Simplification" (formula "19") (ifInst "" (formula "2"))) + (rule "eqSymm" (formula "19") (term "1,0,0,1,0")) + (rule "polySimp_mulComm0" (formula "19") (term "0,0,1")) + (rule "polySimp_rightDist" (formula "19") (term "0,1,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "0,0,1,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,1,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "0,0,1")) + (rule "mul_literals" (formula "19") (term "0,0,0,1")) + (rule "polySimp_addAssoc" (formula "19") (term "1,1,0,0,1,1,0,0,0,0")) + (rule "add_literals" (formula "19") (term "0,1,1,0,0,1,1,0,0,0,0")) + (rule "add_zero_left" (formula "19") (term "1,1,0,0,1,1,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "2,0,1,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "1,1,0,1,0,0,0,0,0,0")) + (rule "replaceKnownSelect_taclet001_4" (formula "19") (term "1,1,0,1,0,0,0,0,0,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_6" (formula "19") (term "1,1,0,1,0,0,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0,1,1,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,1,0,0,0,0,0")) + (rule "replaceKnownSelect_taclet001_4" (formula "19") (term "0,1,1,0,0,0,0,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_6" (formula "19") (term "0,1,1,0,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,0,1,1,0,0,0,1,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0,1,0,0,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "1,1,0,1,1,0,0,0,0")) + (rule "replaceKnownSelect_taclet001_4" (formula "19") (term "1,1,0,1,1,0,0,0,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_6" (formula "19") (term "1,1,0,1,1,0,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,0,1,0,0")) + (rule "replaceKnownSelect_taclet001_4" (formula "19") (term "0,0,1,0,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_6" (formula "19") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,1,0,1,0,0")) + (rule "replaceKnownSelect_taclet001_4" (formula "19") (term "0,1,0,1,0,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_6" (formula "19") (term "0,1,0,1,0,0")) + (rule "precOfInt" (formula "19") (term "1")) + (rule "bsum_induction_upper_concrete" (formula "19") (term "0,1,0,0,0")) + (rule "replaceKnownSelect_taclet0001_5" (formula "19") (term "1,1,0,1,0,0,0")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_7" (formula "19") (term "1,1,0,1,0,0,0")) + (rule "polySimp_homoEq" (formula "19") (term "1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_addComm0" (formula "19") (term "1,1,0,1,0,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "0,1,0,1,0,0,0")) + (rule "dismissNonSelectedField" (formula "19") (term "0,0,1,1,0,0,0,1,0")) + (rule "polySimp_addAssoc" (formula "19") (term "0,1,0,0,0")) + (rule "inEqSimp_ltToLeq" (formula "19") (term "1,1")) + (rule "polySimp_rightDist" (formula "19") (term "1,0,0,1,1")) + (rule "polySimp_mulAssoc" (formula "19") (term "0,1,0,0,1,1")) + (rule "polySimp_mulComm0" (formula "19") (term "0,0,1,0,0,1,1")) + (rule "polySimp_mulLiterals" (formula "19") (term "0,1,0,0,1,1")) + (rule "polySimp_elimOne" (formula "19") (term "0,1,0,0,1,1")) + (rule "polySimp_addAssoc" (formula "19") (term "0,0,1,1")) + (rule "polySimp_addAssoc" (formula "19") (term "0,1,1")) + (rule "polySimp_addComm1" (formula "19") (term "0,0,1,1")) + (rule "polySimp_pullOutFactor2b" (formula "19") (term "0,1,1")) + (rule "add_literals" (formula "19") (term "1,1,0,1,1")) + (rule "times_zero_1" (formula "19") (term "1,0,1,1")) + (rule "add_zero_right" (formula "19") (term "0,1,1")) + (rule "polySimp_addAssoc" (formula "19") (term "0,1,1")) + (rule "polySimp_addComm1" (formula "19") (term "0,0,1,1")) + (rule "add_literals" (formula "19") (term "0,0,0,1,1")) + (rule "add_zero_left" (formula "19") (term "0,0,1,1")) + (rule "polySimp_pullOutFactor1" (formula "19") (term "0,1,1")) + (rule "add_literals" (formula "19") (term "1,0,1,1")) + (rule "times_zero_1" (formula "19") (term "0,1,1")) + (rule "leq_literals" (formula "19") (term "1,1")) + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_commuteLeq" (formula "19") (term "0,0,1,0,0,1,0,0,0")) + (rule "replace_known_left" (formula "19") (term "0,0,1,0,0,1,0,0,0") (ifseqformula "3")) + (builtin "One Step Simplification" (formula "19")) + (rule "polySimp_addComm0" (formula "19") (term "0,0,1,0,0,0")) + (rule "inEqSimp_homoInEq0" (formula "19") (term "1")) + (rule "mul_literals" (formula "19") (term "1,0,1")) + (rule "add_zero_right" (formula "19") (term "0,1")) + (rule "inEqSimp_homoInEq1" (formula "19") (term "1,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,1,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "1,0,1,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "0,1,0,1,0,0")) + (rule "polySimp_addAssoc" (formula "19") (term "0,1,0,0")) + (rule "polySimp_addComm0" (formula "19") (term "0,0,1,0,0")) + (rule "inEqSimp_homoInEq1" (formula "19") (term "0,1,0,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,0,1,0,0,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "1,0,0,1,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "0,1,0,0,1,0,0,0,0")) + (rule "polySimp_addAssoc" (formula "19") (term "0,0,1,0,0,0,0")) + (rule "add_literals" (formula "19") (term "0,0,0,1,0,0,0,0")) + (rule "add_zero_left" (formula "19") (term "0,0,1,0,0,0,0")) + (rule "apply_eq_monomials" (formula "19") (term "1,0,1,0,0,0") (ifseqformula "7")) + (rule "polySimp_rightDist" (formula "19") (term "0,1,0,1,0,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "1,0,1,0,1,0,0,0")) + (rule "polySimp_pullOutFactor0b" (formula "19") (term "1,0,1,0,0,0")) + (rule "add_literals" (formula "19") (term "1,1,1,0,1,0,0,0")) + (rule "times_zero_1" (formula "19") (term "1,1,0,1,0,0,0")) + (rule "add_zero_right" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_addComm1" (formula "19") (term "0,1,0,0,0")) + (rule "polySimp_sepPosMonomial" (formula "19") (term "0,1,0,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "1,0,1,0,0,0,0,0")) + (rule "polySimp_sepPosMonomial" (formula "19") (term "1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "1,1,0,0,0")) + (rule "polySimp_rightDist" (formula "19") (term "1,1,0,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "1,1,1,0,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "1,1,1,0,0,0")) + (rule "polySimp_mulAssoc" (formula "19") (term "0,1,1,0,0,0")) + (rule "polySimp_mulComm0" (formula "19") (term "0,0,1,1,0,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "0,1,1,0,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "0,1,1,0,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "19") (term "0,0,0,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "1,0,0,0,0,0,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "19") (term "1")) + (rule "polySimp_mulComm0" (formula "19") (term "1,1")) + (rule "polySimp_rightDist" (formula "19") (term "1,1")) + (rule "polySimp_mulLiterals" (formula "19") (term "1,1,1")) + (rule "mul_literals" (formula "19") (term "0,1,1")) + (rule "polySimp_elimOne" (formula "19") (term "1,1,1")) + (rule "replace_known_left" (formula "19") (term "1") (ifseqformula "2")) + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_sepNegMonomial0" (formula "19") (term "1,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "0,1,0")) + (rule "polySimp_elimOne" (formula "19") (term "0,1,0")) + (rule "inEqSimp_invertInEq0" (formula "19") (term "0,1,0,0,0")) + (rule "mul_literals" (formula "19") (term "1,0,1,0,0,0")) + (rule "polySimp_mulLiterals" (formula "19") (term "0,0,1,0,0,0")) + (rule "polySimp_elimOne" (formula "19") (term "0,0,1,0,0,0")) + (rule "replace_known_left" (formula "19") (term "0,1,0,0,0") (ifseqformula "3")) + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_contradEq7" (formula "19") (term "0,1,0,0,0,0") (ifseqformula "3")) + (rule "add_zero_left" (formula "19") (term "0,0,0,1,0,0,0,0")) + (rule "mul_literals" (formula "19") (term "0,0,0,1,0,0,0,0")) + (rule "leq_literals" (formula "19") (term "0,0,1,0,0,0,0")) + (builtin "One Step Simplification" (formula "19")) + (rule "inEqSimp_subsumption1" (formula "19") (term "0,0,0,0,0") (ifseqformula "3")) + (rule "leq_literals" (formula "19") (term "0,0,0,0,0,0")) + (builtin "One Step Simplification" (formula "19")) + (rule "pullOutSelect" (formula "19") (term "1,1,1,0") (inst "selectSK=SumAndMax_sum_2:int")) + (rule "applyEq" (formula "20") (term "0,1,0,0") (ifseqformula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "0")) + (rule "applyEqReverse" (formula "20") (term "1,1,1,0") (ifseqformula "1")) + (rule "applyEqReverse" (formula "20") (term "0,1,0,0") (ifseqformula "1")) + (builtin "One Step Simplification" (formula "20")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "polySimp_addAssoc" (formula "19") (term "1,1,0")) + (rule "polySimp_addComm0" (formula "19") (term "0,1,1,0")) + (rule "cut_direct" (formula "6") (term "0")) + (branch "CUT: k_0 >= 1 TRUE" + (builtin "One Step Simplification" (formula "7")) + (rule "exLeft" (formula "7") (inst "sk=i_0:int")) + (rule "andLeft" (formula "7")) + (rule "andLeft" (formula "7")) + (rule "inEqSimp_homoInEq0" (formula "8")) + (rule "polySimp_addComm1" (formula "8") (term "0")) + (rule "inEqSimp_sepPosMonomial1" (formula "8")) + (rule "polySimp_mulComm0" (formula "8") (term "1")) + (rule "polySimp_rightDist" (formula "8") (term "1")) + (rule "polySimp_mulLiterals" (formula "8") (term "1,1")) + (rule "mul_literals" (formula "8") (term "0,1")) + (rule "polySimp_elimOne" (formula "8") (term "1,1")) + (rule "inEqSimp_contradEq7" (formula "5") (term "0") (ifseqformula "6")) + (rule "mul_literals" (formula "5") (term "1,0,0,0")) + (rule "add_zero_right" (formula "5") (term "0,0,0")) + (rule "leq_literals" (formula "5") (term "0,0")) + (builtin "One Step Simplification" (formula "5")) + (rule "true_left" (formula "5")) + (rule "inEqSimp_subsumption1" (formula "3") (ifseqformula "5")) + (rule "leq_literals" (formula "3") (term "0")) + (builtin "One Step Simplification" (formula "3")) + (rule "true_left" (formula "3")) + (rule "pullOutSelect" (formula "7") (term "0") (inst "selectSK=arr_1:int")) + (rule "simplifySelectOfAnon" (formula "7")) + (builtin "One Step Simplification" (formula "7") (ifInst "" (formula "20"))) + (rule "eqSymm" (formula "8")) + (rule "applyEqReverse" (formula "7") (term "1") (ifseqformula "8")) + (rule "hideAuxiliaryEq" (formula "8")) + (rule "dismissNonSelectedField" (formula "7") (term "2,0")) + (rule "dismissNonSelectedField" (formula "7") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "7") (term "2,0")) + (rule "dismissNonSelectedField" (formula "7") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "7") (term "0,1,0,0") (ifseqformula "14")) + (builtin "One Step Simplification" (formula "7")) + (rule "elementOfUnion" (formula "7") (term "0,0")) + (rule "elementOfSingleton" (formula "7") (term "0,0,0")) + (builtin "One Step Simplification" (formula "7")) + (rule "elementOfSingleton" (formula "7") (term "0,0")) + (builtin "One Step Simplification" (formula "7")) + (rule "eqSymm" (formula "7")) + (rule "applyEq" (formula "20") (term "1,1,0,0,0,0") (ifseqformula "7")) + (rule "applyEq" (formula "1") (term "0") (ifseqformula "7")) + (rule "inEqSimp_commuteGeq" (formula "1")) + (rule "applyEq" (formula "3") (term "1,1,0") (ifseqformula "7")) + (rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "7")) + (rule "applyEq" (formula "9") (term "0,0") (ifseqformula "7")) + (rule "applyEq" (formula "20") (term "0,1,0,1,1,0") (ifseqformula "7")) + (rule "polySimp_addComm0" (formula "20") (term "0,1,1,0")) + (rule "applyEq" (formula "20") (term "1,1,0,1,0,0") (ifseqformula "7")) + (rule "allLeft" (formula "17") (inst "t=k_0:int")) + (rule "inEqSimp_commuteGeq" (formula "17") (term "1,0")) + (rule "inEqSimp_contradInEq1" (formula "17") (term "0,0") (ifseqformula "4")) + (rule "qeq_literals" (formula "17") (term "0,0,0")) + (builtin "One Step Simplification" (formula "17")) + (rule "inEqSimp_contradInEq1" (formula "17") (term "0") (ifseqformula "2")) + (rule "inEqSimp_homoInEq1" (formula "17") (term "0,0")) + (rule "polySimp_pullOutFactor1b" (formula "17") (term "0,0,0")) + (rule "add_literals" (formula "17") (term "1,1,0,0,0")) + (rule "times_zero_1" (formula "17") (term "1,0,0,0")) + (rule "add_zero_right" (formula "17") (term "0,0,0")) + (rule "leq_literals" (formula "17") (term "0,0")) + (builtin "One Step Simplification" (formula "17")) + (rule "inEqSimp_exactShadow3" (formula "17") (ifseqformula "1")) + (rule "mul_literals" (formula "17") (term "0,0")) + (rule "add_zero_left" (formula "17") (term "0")) + (rule "allLeft" (formula "3") (inst "t=i_0:int")) + (rule "replaceKnownSelect_taclet000010001_12" (formula "3") (term "0,1")) + (rule "replaceKnownAuxiliaryConstant_taclet000010001_13" (formula "3") (term "0,1")) + (rule "inEqSimp_commuteGeq" (formula "3") (term "1,0")) + (rule "applyEq" (formula "3") (term "0,1") (ifseqformula "8")) + (rule "inEqSimp_homoInEq0" (formula "3") (term "1")) + (rule "polySimp_pullOutFactor1" (formula "3") (term "0,1")) + (rule "add_literals" (formula "3") (term "1,0,1")) + (rule "times_zero_1" (formula "3") (term "0,1")) + (rule "qeq_literals" (formula "3") (term "1")) + (builtin "One Step Simplification" (formula "3")) + (rule "true_left" (formula "3")) + (rule "andRight" (formula "22")) + (branch + (rule "andRight" (formula "22")) + (branch + (rule "andRight" (formula "22")) + (branch + (rule "allRight" (formula "22") (inst "sk=i_9:int")) + (rule "orRight" (formula "22")) + (rule "orRight" (formula "22")) + (rule "inEqSimp_leqRight" (formula "24")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) + (rule "inEqSimp_leqRight" (formula "23")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_geqRight" (formula "24")) + (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) + (rule "mul_literals" (formula "1") (term "0,1,0,0")) + (rule "polySimp_addAssoc" (formula "1") (term "0,0")) + (rule "add_literals" (formula "1") (term "0,0,0")) + (rule "add_zero_left" (formula "1") (term "0,0")) + (rule "polySimp_addComm0" (formula "1") (term "0")) + (rule "inEqSimp_sepPosMonomial1" (formula "3")) + (rule "polySimp_mulComm0" (formula "3") (term "1")) + (rule "polySimp_rightDist" (formula "3") (term "1")) + (rule "mul_literals" (formula "3") (term "0,1")) + (rule "polySimp_mulLiterals" (formula "3") (term "1,1")) + (rule "polySimp_elimOne" (formula "3") (term "1,1")) + (rule "inEqSimp_sepNegMonomial0" (formula "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "0")) + (rule "polySimp_elimOne" (formula "1") (term "0")) + (rule "pullOutSelect" (formula "3") (term "0") (inst "selectSK=arr_2:int")) + (rule "simplifySelectOfAnon" (formula "3")) + (builtin "One Step Simplification" (formula "3") (ifInst "" (formula "25"))) + (rule "dismissNonSelectedField" (formula "3") (term "2,0")) + (rule "dismissNonSelectedField" (formula "3") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "3") (term "2,0")) + (rule "dismissNonSelectedField" (formula "3") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "3") (term "0,1,0,0") (ifseqformula "18")) + (builtin "One Step Simplification" (formula "3")) + (rule "inEqSimp_homoInEq1" (formula "4")) + (rule "polySimp_addComm1" (formula "4") (term "0")) + (rule "inEqSimp_sepPosMonomial0" (formula "4")) + (rule "polySimp_mulComm0" (formula "4") (term "1")) + (rule "polySimp_rightDist" (formula "4") (term "1")) + (rule "mul_literals" (formula "4") (term "0,1")) + (rule "polySimp_mulLiterals" (formula "4") (term "1,1")) + (rule "polySimp_elimOne" (formula "4") (term "1,1")) + (rule "elementOfUnion" (formula "3") (term "0,0")) + (rule "elementOfSingleton" (formula "3") (term "1,0,0")) + (builtin "One Step Simplification" (formula "3")) + (rule "elementOfSingleton" (formula "3") (term "0,0")) + (builtin "One Step Simplification" (formula "3")) + (rule "applyEqReverse" (formula "4") (term "1,1") (ifseqformula "3")) + (rule "hideAuxiliaryEq" (formula "3")) + (rule "inEqSimp_homoInEq0" (formula "3")) + (rule "polySimp_addComm1" (formula "3") (term "0")) + (rule "inEqSimp_sepPosMonomial1" (formula "3")) + (rule "polySimp_mulComm0" (formula "3") (term "1")) + (rule "polySimp_rightDist" (formula "3") (term "1")) + (rule "polySimp_mulLiterals" (formula "3") (term "1,1")) + (rule "mul_literals" (formula "3") (term "0,1")) + (rule "polySimp_elimOne" (formula "3") (term "1,1")) + (rule "allLeft" (formula "6") (inst "t=i_9:int")) + (rule "replaceKnownSelect_taclet000000010001_14" (formula "6") (term "0,1")) + (rule "replaceKnownAuxiliaryConstant_taclet000000010001_15" (formula "6") (term "0,1")) + (rule "inEqSimp_commuteGeq" (formula "6") (term "1,0")) + (rule "inEqSimp_contradInEq1" (formula "6") (term "1") (ifseqformula "3")) + (rule "inEqSimp_homoInEq1" (formula "6") (term "0,1")) + (rule "polySimp_pullOutFactor1b" (formula "6") (term "0,0,1")) + (rule "add_literals" (formula "6") (term "1,1,0,0,1")) + (rule "times_zero_1" (formula "6") (term "1,0,0,1")) + (rule "add_literals" (formula "6") (term "0,0,1")) + (rule "leq_literals" (formula "6") (term "0,1")) + (builtin "One Step Simplification" (formula "6")) + (rule "inEqSimp_contradInEq1" (formula "6") (term "0") (ifseqformula "2")) + (rule "qeq_literals" (formula "6") (term "0,0")) + (builtin "One Step Simplification" (formula "6")) + (rule "inEqSimp_antiSymm" (formula "1") (ifseqformula "6")) + (rule "applyEqRigid" (formula "8") (term "1,1,0,0") (ifseqformula "1")) + (rule "applyEqRigid" (formula "14") (term "1,0") (ifseqformula "1")) + (rule "applyEq" (formula "2") (term "0") (ifseqformula "1")) + (rule "inEqSimp_homoInEq1" (formula "2")) + (rule "polySimp_pullOutFactor1" (formula "2") (term "0")) + (rule "add_literals" (formula "2") (term "1,0")) + (rule "times_zero_1" (formula "2") (term "0")) + (rule "leq_literals" (formula "2")) + (rule "true_left" (formula "2")) + (rule "applyEq" (formula "22") (term "0,2,0") (ifseqformula "1")) + (rule "applyEq" (formula "4") (term "0,2,0") (ifseqformula "1")) + (rule "applyEqRigid" (formula "5") (term "1,1") (ifseqformula "1")) + (rule "applyEq" (formula "12") (term "1,0") (ifseqformula "1")) + (rule "applyEq" (formula "6") (term "0") (ifseqformula "1")) + (rule "inEqSimp_homoInEq0" (formula "6")) + (rule "polySimp_pullOutFactor1" (formula "6") (term "0")) + (rule "add_literals" (formula "6") (term "1,0")) + (rule "times_zero_1" (formula "6") (term "0")) + (rule "qeq_literals" (formula "6")) + (rule "true_left" (formula "6")) + (rule "applyEqRigid" (formula "9") (term "0") (ifseqformula "1")) + (rule "applyEq" (formula "7") (term "0") (ifseqformula "1")) + (rule "inEqSimp_contradInEq1" (formula "4") (ifseqformula "3")) + (rule "andLeft" (formula "4")) + (rule "inEqSimp_homoInEq1" (formula "4")) + (rule "polySimp_pullOutFactor1b" (formula "4") (term "0")) + (rule "add_literals" (formula "4") (term "1,1,0")) + (rule "times_zero_1" (formula "4") (term "1,0")) + (rule "add_literals" (formula "4") (term "0")) + (rule "leq_literals" (formula "4")) + (rule "closeFalse" (formula "4")) + ) + (branch + (rule "nnf_ex2all" (formula "22")) + (rule "nnf_notAnd" (formula "1") (term "0")) + (rule "nnf_notAnd" (formula "1") (term "0,0")) + (rule "inEqSimp_notGeq" (formula "1") (term "0,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,0,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0,0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "0,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,0")) + (rule "inEqSimp_notLeq" (formula "1") (term "1,0,0")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0,1,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1") (term "1,0,0")) + (rule "polySimp_mulComm0" (formula "1") (term "1,1,0,0")) + (rule "polySimp_rightDist" (formula "1") (term "1,1,0,0")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1,1,0,0")) + (rule "mul_literals" (formula "1") (term "0,1,1,0,0")) + (rule "polySimp_elimOne" (formula "1") (term "1,1,1,0,0")) + (rule "allLeft" (formula "1") (inst "t=k_0:int")) + (rule "replaceKnownSelect_taclet0001_5" (formula "1") (term "0,0,1")) + (rule "replaceKnownAuxiliaryConstant_taclet0001_7" (formula "1") (term "0,0,1")) + (rule "inEqSimp_homoInEq1" (formula "1") (term "1,0")) + (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,1,0")) + (rule "add_literals" (formula "1") (term "1,1,0,1,0")) + (rule "times_zero_1" (formula "1") (term "1,0,1,0")) + (rule "add_zero_right" (formula "1") (term "0,1,0")) + (rule "leq_literals" (formula "1") (term "1,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_contradInEq1" (formula "1") (term "0") (ifseqformula "6")) + (rule "qeq_literals" (formula "1") (term "0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "inEqSimp_strengthen0" (formula "2") (ifseqformula "21")) + (rule "inEqSimp_contradEq3" (formula "21") (ifseqformula "2")) + (rule "polySimp_mulComm0" (formula "21") (term "1,0,0")) + (rule "polySimp_pullOutFactor1b" (formula "21") (term "0,0")) + (rule "add_literals" (formula "21") (term "1,1,0,0")) + (rule "times_zero_1" (formula "21") (term "1,0,0")) + (rule "add_zero_right" (formula "21") (term "0,0")) + (rule "qeq_literals" (formula "21") (term "0")) + (builtin "One Step Simplification" (formula "21")) + (rule "false_right" (formula "21")) + (rule "inEqSimp_exactShadow3" (formula "19") (ifseqformula "2")) + (rule "mul_literals" (formula "19") (term "0,0")) + (rule "add_zero_left" (formula "19") (term "0")) + (rule "inEqSimp_sepPosMonomial1" (formula "19")) + (rule "mul_literals" (formula "19") (term "1")) + (rule "inEqSimp_subsumption1" (formula "18") (ifseqformula "19")) + (rule "leq_literals" (formula "18") (term "0")) + (builtin "One Step Simplification" (formula "18")) + (rule "true_left" (formula "18")) + (rule "allLeft" (formula "1") (inst "t=i_0:int")) + (rule "replaceKnownSelect_taclet000010001_12" (formula "1") (term "0,0,1")) + (rule "replaceKnownAuxiliaryConstant_taclet000010001_13" (formula "1") (term "0,0,1")) + (rule "replace_known_left" (formula "1") (term "0,1") (ifseqformula "9")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_homoInEq1" (formula "1") (term "1")) + (rule "polySimp_addComm1" (formula "1") (term "0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "1")) + (rule "polySimp_mulComm0" (formula "1") (term "1,1")) + (rule "polySimp_rightDist" (formula "1") (term "1,1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1,1")) + (rule "mul_literals" (formula "1") (term "0,1,1")) + (rule "polySimp_elimOne" (formula "1") (term "1,1,1")) + (rule "inEqSimp_contradInEq1" (formula "1") (term "1") (ifseqformula "8")) + (rule "inEqSimp_homoInEq1" (formula "1") (term "0,1")) + (rule "polySimp_mulComm0" (formula "1") (term "1,0,0,1")) + (rule "polySimp_rightDist" (formula "1") (term "1,0,0,1")) + (rule "mul_literals" (formula "1") (term "0,1,0,0,1")) + (rule "polySimp_addAssoc" (formula "1") (term "0,0,1")) + (rule "polySimp_addComm1" (formula "1") (term "0,0,0,1")) + (rule "add_literals" (formula "1") (term "0,0,0,0,1")) + (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,0,1")) + (rule "add_literals" (formula "1") (term "1,1,0,0,1")) + (rule "times_zero_1" (formula "1") (term "1,0,0,1")) + (rule "add_zero_right" (formula "1") (term "0,0,1")) + (rule "leq_literals" (formula "1") (term "0,1")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_contradInEq0" (formula "7") (ifseqformula "1")) + (rule "qeq_literals" (formula "7") (term "0")) + (builtin "One Step Simplification" (formula "7")) + (rule "closeFalse" (formula "7")) + ) + ) + (branch + (rule "inEqSimp_geqRight" (formula "22")) + (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) + (rule "polySimp_rightDist" (formula "1") (term "0,1,0,0")) + (rule "polySimp_mulAssoc" (formula "1") (term "0,0,1,0,0")) + (rule "polySimp_mulComm0" (formula "1") (term "0,0,0,1,0,0")) + (rule "polySimp_mulLiterals" (formula "1") (term "0,0,1,0,0")) + (rule "polySimp_elimOne" (formula "1") (term "0,0,1,0,0")) + (rule "polySimp_addAssoc" (formula "1") (term "0,0")) + (rule "polySimp_addAssoc" (formula "1") (term "0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1")) + (rule "polySimp_mulComm0" (formula "1") (term "1")) + (rule "polySimp_rightDist" (formula "1") (term "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) + (rule "polySimp_elimOne" (formula "1") (term "1,1")) + (rule "polySimp_rightDist" (formula "1") (term "0,1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1,0,1")) + (rule "polySimp_elimOne" (formula "1") (term "1,0,1")) + (rule "polySimp_rightDist" (formula "1") (term "0,0,1")) + (rule "mul_literals" (formula "1") (term "0,0,0,1")) + (rule "inEqSimp_exactShadow3" (formula "10") (ifseqformula "1")) + (rule "polySimp_mulComm0" (formula "10") (term "0,0")) + (rule "polySimp_addAssoc" (formula "10") (term "0")) + (rule "polySimp_addComm0" (formula "10") (term "0,0")) + (rule "polySimp_pullOutFactor2b" (formula "10") (term "0")) + (rule "add_literals" (formula "10") (term "1,1,0")) + (rule "times_zero_1" (formula "10") (term "1,0")) + (rule "add_zero_right" (formula "10") (term "0")) + (rule "inEqSimp_sepPosMonomial1" (formula "10")) + (rule "polySimp_mulComm0" (formula "10") (term "1")) + (rule "polySimp_rightDist" (formula "10") (term "1")) + (rule "polySimp_mulLiterals" (formula "10") (term "1,1")) + (rule "mul_literals" (formula "10") (term "0,1")) + (rule "polySimp_elimOne" (formula "10") (term "1,1")) + (rule "inEqSimp_contradInEq0" (formula "10") (ifseqformula "2")) + (rule "andLeft" (formula "10")) + (rule "inEqSimp_homoInEq1" (formula "10")) + (rule "polySimp_pullOutFactor1b" (formula "10") (term "0")) + (rule "add_literals" (formula "10") (term "1,1,0")) + (rule "times_zero_1" (formula "10") (term "1,0")) + (rule "add_zero_right" (formula "10") (term "0")) + (rule "leq_literals" (formula "10")) + (rule "closeFalse" (formula "10")) + ) + ) + (branch + (rule "allRight" (formula "22") (inst "sk=f_0:Field")) + (rule "allRight" (formula "22") (inst "sk=o_0:java.lang.Object")) + (rule "orRight" (formula "22")) + (rule "orRight" (formula "22")) + (rule "orRight" (formula "22")) + (rule "pullOutSelect" (formula "25") (term "1") (inst "selectSK=f_0_0:any")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "24")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "23")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "26") (term "1") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "pullOutSelect" (formula "25") (term "0") (inst "selectSK=f_0_1:any")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "26")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "23")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "replaceKnownSelect_taclet1000010001_14" (formula "1") (term "2,0")) + (rule "replaceKnownAuxiliaryConstant_taclet1000010001_16" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "replace_known_right" (formula "1") (term "1,0,0") (ifseqformula "25")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0,0")) + (rule "elementOfSingleton" (formula "1") (term "1,0,0,0")) + (rule "replace_known_right" (formula "1") (term "1,0,0,0") (ifseqformula "23")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0,0") (ifseqformula "24")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "26"))) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "CUT: k_0 >= 1 FALSE" + (builtin "One Step Simplification" (formula "6")) + (rule "true_left" (formula "6")) + (rule "inEqSimp_geqRight" (formula "16")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_literals" (formula "1") (term "0,0")) + (rule "add_zero_left" (formula "1") (term "0")) + (rule "inEqSimp_antiSymm" (formula "4") (ifseqformula "1")) + (rule "replace_known_left" (formula "7") (term "0") (ifseqformula "4")) + (builtin "One Step Simplification" (formula "7")) + (rule "applyEq" (formula "9") (term "1,0") (ifseqformula "4")) + (rule "times_zero_1" (formula "9") (term "0")) + (rule "inEqSimp_commuteGeq" (formula "9")) + (rule "applyEq" (formula "6") (term "1,1,0,0") (ifseqformula "4")) + (rule "applyEqRigid" (formula "20") (term "1,0,1,0") (ifseqformula "4")) + (rule "times_zero_1" (formula "20") (term "0,1,0")) + (rule "inEqSimp_homoInEq1" (formula "20") (term "1,0")) + (rule "mul_literals" (formula "20") (term "1,0,1,0")) + (rule "add_zero_right" (formula "20") (term "0,1,0")) + (rule "applyEqRigid" (formula "8") (term "1,0") (ifseqformula "4")) + (rule "bsum_lower_equals_upper" (formula "8") (term "0")) + (rule "eqSymm" (formula "8")) + (rule "applyEq" (formula "20") (term "1,1,0,0,0,0") (ifseqformula "7")) + (rule "applyEq" (formula "5") (term "0") (ifseqformula "4")) + (rule "qeq_literals" (formula "5")) + (rule "true_left" (formula "5")) + (rule "applyEqRigid" (formula "19") (term "1,1,0,0,1,0,0") (ifseqformula "4")) + (rule "applyEq" (formula "1") (term "0") (ifseqformula "4")) + (rule "leq_literals" (formula "1")) + (rule "true_left" (formula "1")) + (rule "applyEq" (formula "1") (term "0") (ifseqformula "5")) + (rule "inEqSimp_commuteGeq" (formula "1")) + (rule "applyEqRigid" (formula "2") (term "1,1") (ifseqformula "3")) + (rule "add_zero_right" (formula "2") (term "1")) + (rule "applyEq" (formula "4") (term "1,1,0") (ifseqformula "5")) + (rule "applyEqRigid" (formula "18") (term "1,1,1,0,0,0,0,0") (ifseqformula "3")) + (rule "add_zero_right" (formula "18") (term "1,1,0,0,0,0,0")) + (rule "applyEqRigid" (formula "1") (term "0,2,0") (ifseqformula "3")) + (rule "applyEq" (formula "18") (term "1,0,1,0") (ifseqformula "6")) + (rule "add_zero_right" (formula "18") (term "0,1,0")) + (rule "applyEq" (formula "18") (term "1,3,0,0,1,0,0,1") (ifseqformula "6")) + (rule "add_zero_right" (formula "18") (term "3,0,0,1,0,0,1")) + (rule "applyEq" (formula "7") (term "0") (ifseqformula "6")) + (rule "leq_literals" (formula "7")) + (rule "true_left" (formula "7")) + (rule "applyEq" (formula "17") (term "1,1,0,1,0,0") (ifseqformula "5")) + (rule "applyEq" (formula "17") (term "0,2,3,0,0,1,0,0,1") (ifseqformula "3")) + (rule "applyEq" (formula "17") (term "0,1,0,1,0") (ifseqformula "5")) + (rule "mul_literals" (formula "17") (term "1,0,1,0")) + (rule "add_zero_right" (formula "17") (term "0,1,0")) + (rule "applyEqRigid" (formula "17") (term "0,2,0,1,0") (ifseqformula "3")) + (rule "replace_known_left" (formula "17") (term "1,0") (ifseqformula "1")) + (builtin "One Step Simplification" (formula "17")) + (rule "inEqSimp_subsumption1" (formula "13") (ifseqformula "2")) + (rule "leq_literals" (formula "13") (term "0")) + (builtin "One Step Simplification" (formula "13")) + (rule "true_left" (formula "13")) + (rule "inEqSimp_or_tautInEq0" (formula "4") (term "0,0")) + (rule "add_zero_right" (formula "4") (term "1,1,0,0")) + (rule "qeq_literals" (formula "4") (term "1,0,0")) + (builtin "One Step Simplification" (formula "4")) + (rule "true_left" (formula "4")) + (rule "inEqSimp_or_antiSymm0" (formula "15") (term "0,0,0,0")) + (rule "add_literals" (formula "15") (term "1,0,1,0,0,0,0")) + (rule "add_literals" (formula "15") (term "0,0,0,0,0,0")) + (builtin "One Step Simplification" (formula "15")) + (rule "andRight" (formula "15")) + (branch + (rule "andRight" (formula "15")) + (branch + (rule "allRight" (formula "15") (inst "sk=i_0:int")) + (rule "orRight" (formula "15")) + (rule "notRight" (formula "15")) + (rule "inEqSimp_leqRight" (formula "16")) + (rule "mul_literals" (formula "1") (term "1,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0")) + (rule "applyEq" (formula "1") (term "0,2,1,0") (ifseqformula "2")) + (rule "inEqSimp_sepPosMonomial1" (formula "1")) + (rule "mul_literals" (formula "1") (term "1")) + (rule "pullOutSelect" (formula "1") (term "0") (inst "selectSK=arr_1:int")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "13")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "1,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "2") (term "0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "inEqSimp_contradInEq1" (formula "3") (ifseqformula "1")) + (rule "qeq_literals" (formula "3") (term "0")) + (builtin "One Step Simplification" (formula "3")) + (rule "closeFalse" (formula "3")) + ) + (branch + (rule "nnf_ex2all" (formula "15")) + (rule "nnf_notAnd" (formula "1") (term "0")) + (rule "nnf_notAnd" (formula "1") (term "0,0")) + (rule "inEqSimp_notGeq" (formula "1") (term "0,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,0,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0,0,0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "0,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,0")) + (rule "inEqSimp_notLeq" (formula "1") (term "1,0,0")) + (rule "mul_literals" (formula "1") (term "1,0,0,1,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0,1,0,0")) + (rule "inEqSimp_sepPosMonomial1" (formula "1") (term "1,0,0")) + (rule "mul_literals" (formula "1") (term "1,1,0,0")) + (rule "inEqSimp_or_antiSymm0" (formula "1") (term "0,0")) + (rule "add_literals" (formula "1") (term "1,0,1,0,0")) + (rule "add_literals" (formula "1") (term "0,0,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "commute_or" (formula "1") (term "0")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "pullOutSelect" (formula "13") (term "0") (inst "selectSK=arr_1:int")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "16"))) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "14") (term "0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "inEqSimp_strengthen0" (formula "1") (ifseqformula "13")) + (rule "add_zero_right" (formula "1") (term "1")) + (rule "inEqSimp_contradEq3" (formula "13") (ifseqformula "1")) + (rule "mul_literals" (formula "13") (term "1,0,0")) + (rule "add_zero_right" (formula "13") (term "0,0")) + (rule "qeq_literals" (formula "13") (term "0")) + (builtin "One Step Simplification" (formula "13")) + (rule "false_right" (formula "13")) + (rule "allLeft" (formula "12") (inst "t=Z(0(#)):int")) + (rule "leq_literals" (formula "12") (term "0,0")) + (builtin "One Step Simplification" (formula "12")) + (rule "inEqSimp_commuteGeq" (formula "12") (term "0")) + (rule "inEqSimp_contradInEq1" (formula "12") (term "0") (ifseqformula "2")) + (rule "qeq_literals" (formula "12") (term "0,0")) + (builtin "One Step Simplification" (formula "12")) + (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "12")) + (rule "qeq_literals" (formula "1") (term "0")) + (builtin "One Step Simplification" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) + (branch + (rule "allRight" (formula "15") (inst "sk=f_0:Field")) + (rule "allRight" (formula "15") (inst "sk=o_0:java.lang.Object")) + (rule "orRight" (formula "15")) + (rule "orRight" (formula "15")) + (rule "orRight" (formula "15")) + (rule "pullOutSelect" (formula "18") (term "0") (inst "selectSK=f_0_0:any")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "19")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "16")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "replace_known_right" (formula "1") (term "1,0,0") (ifseqformula "18")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0,0")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0,0,0") (ifseqformula "17")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0,0") (ifseqformula "16")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "19"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Null Reference (s_1 = null)" + (builtin "One Step Simplification" (formula "20")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "18"))) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "Null Reference (k < _a.length = null)" + (builtin "One Step Simplification" (formula "21")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "20"))) + (rule "closeFalse" (formula "1")) + ) + (branch "Index Out of Bounds (k < _a.length != null, but k < _a.length Out of Bounds!)" + (rule "false_right" (formula "21")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "20"))) + (rule "inEqSimp_ltToLeq" (formula "1") (term "1")) + (rule "mul_literals" (formula "1") (term "1,0,0,1")) + (rule "add_literals" (formula "1") (term "0,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "1")) + (rule "mul_literals" (formula "1") (term "1,1")) + (rule "inEqSimp_contradInEq1" (formula "1") (term "0") (ifseqformula "4")) + (rule "inEqSimp_homoInEq1" (formula "1") (term "0,0")) + (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,0,0")) + (rule "add_literals" (formula "1") (term "1,1,0,0,0")) + (rule "times_zero_1" (formula "1") (term "1,0,0,0")) + (rule "add_zero_right" (formula "1") (term "0,0,0")) + (rule "leq_literals" (formula "1") (term "0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_contradEq3" (formula "7") (term "0") (ifseqformula "1")) + (rule "mul_literals" (formula "7") (term "1,0,0,0")) + (rule "add_zero_right" (formula "7") (term "0,0,0")) + (rule "qeq_literals" (formula "7") (term "0,0")) + (builtin "One Step Simplification" (formula "7")) + (rule "true_left" (formula "7")) + (rule "inEqSimp_contradInEq0" (formula "7") (term "0") (ifseqformula "1")) + (rule "qeq_literals" (formula "7") (term "0,0")) + (builtin "One Step Simplification" (formula "7")) + (rule "true_left" (formula "7")) + (rule "inEqSimp_contradInEq0" (formula "5") (ifseqformula "1")) + (rule "qeq_literals" (formula "5") (term "0")) + (builtin "One Step Simplification" (formula "5")) + (rule "closeFalse" (formula "5")) + ) + ) + (branch "Null Reference (s = null)" + (rule "false_right" (formula "20")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "18"))) + (rule "closeFalse" (formula "1")) + ) + ) + ) + (branch "Null Reference (k < _a.length = null)" + (builtin "One Step Simplification" (formula "20")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "19"))) + (rule "closeFalse" (formula "1")) + ) + (branch "Index Out of Bounds (k < _a.length != null, but k < _a.length Out of Bounds!)" + (rule "false_right" (formula "20")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "19"))) + (rule "inEqSimp_ltToLeq" (formula "1") (term "1")) + (rule "times_zero_1" (formula "1") (term "1,0,0,1")) + (rule "add_literals" (formula "1") (term "0,0,1")) + (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "1")) + (rule "mul_literals" (formula "1") (term "1,1")) + (rule "inEqSimp_contradInEq1" (formula "1") (term "1") (ifseqformula "4")) + (rule "qeq_literals" (formula "1") (term "0,1")) + (builtin "One Step Simplification" (formula "1")) + (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "3")) + (rule "andLeft" (formula "1")) + (rule "inEqSimp_homoInEq1" (formula "1")) + (rule "polySimp_pullOutFactor1b" (formula "1") (term "0")) + (rule "add_literals" (formula "1") (term "1,1,0")) + (rule "times_zero_1" (formula "1") (term "1,0")) + (rule "add_literals" (formula "1") (term "0")) + (rule "leq_literals" (formula "1")) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "if k < _a.length false" + (builtin "One Step Simplification" (formula "19")) + (builtin "One Step Simplification" (formula "1")) + (rule "notLeft" (formula "1")) + (rule "inEqSimp_geqRight" (formula "16")) + (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) + (rule "mul_literals" (formula "1") (term "0,1,0,0")) + (rule "polySimp_addAssoc" (formula "1") (term "0,0")) + (rule "add_literals" (formula "1") (term "0,0,0")) + (rule "add_zero_left" (formula "1") (term "0,0")) + (rule "inEqSimp_sepPosMonomial0" (formula "1")) + (rule "polySimp_mulLiterals" (formula "1") (term "1")) + (rule "polySimp_elimOne" (formula "1") (term "1")) + (rule "inEqSimp_antiSymm" (formula "3") (ifseqformula "1")) + (rule "applyEq" (formula "20") (term "1,0,1,1,0") (ifseqformula "3")) + (rule "polySimp_pullOutFactor2" (formula "20") (term "0,1,1,0")) + (rule "add_literals" (formula "20") (term "1,0,1,1,0")) + (rule "times_zero_1" (formula "20") (term "0,1,1,0")) + (rule "applyEq" (formula "4") (term "0") (ifseqformula "3")) + (rule "inEqSimp_homoInEq1" (formula "4")) + (rule "polySimp_pullOutFactor1" (formula "4") (term "0")) + (rule "add_literals" (formula "4") (term "1,0")) + (rule "times_zero_1" (formula "4") (term "0")) + (rule "leq_literals" (formula "4")) + (rule "true_left" (formula "4")) + (rule "applyEq" (formula "1") (term "0") (ifseqformula "3")) + (rule "inEqSimp_homoInEq0" (formula "1")) + (rule "polySimp_pullOutFactor1" (formula "1") (term "0")) + (rule "add_literals" (formula "1") (term "1,0")) + (rule "times_zero_1" (formula "1") (term "0")) + (rule "qeq_literals" (formula "1")) + (rule "true_left" (formula "1")) + (rule "applyEq" (formula "14") (term "0") (ifseqformula "2")) + (rule "applyEq" (formula "14") (term "1,1,0,0") (ifseqformula "2")) + (rule "blockBreak" (formula "17") (term "1")) + (rule "lsBreak" (formula "17") (term "1")) + (rule "assignment" (formula "17") (term "1")) + (builtin "One Step Simplification" (formula "17")) + (rule "methodCallEmpty" (formula "17") (term "1")) + (rule "tryEmpty" (formula "17") (term "1")) + (rule "emptyModality" (formula "17") (term "1")) + (builtin "One Step Simplification" (formula "17")) + (rule "eqSymm" (formula "17") (term "1,0,0,1")) + (rule "applyEq" (formula "17") (term "1,0,0,1,1,0") (ifseqformula "2")) + (rule "applyEq" (formula "17") (term "1,1,1,0,0,1,0,1,0") (ifseqformula "2")) + (rule "applyEq" (formula "17") (term "1,0,0,1,1,1,0") (ifseqformula "2")) + (rule "applyEq" (formula "17") (term "1,1,0,0,0,0") (ifseqformula "2")) + (rule "applyEq" (formula "17") (term "0,0,0,1,0") (ifseqformula "2")) + (rule "pullOutSelect" (formula "17") (term "1,0,1,1,0") (inst "selectSK=SumAndMax_sum_1:int")) + (rule "applyEq" (formula "18") (term "1,0,1,1,1,0") (ifseqformula "1")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "16"))) + (rule "dismissNonSelectedField" (formula "1") (term "2,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "1,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "18") (term "1,0,1,1,1,0") (ifseqformula "1")) + (rule "applyEqReverse" (formula "18") (term "1,0,1,1,0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "replace_known_left" (formula "17") (term "0,1,1,0") (ifseqformula "6")) + (builtin "One Step Simplification" (formula "17")) + (rule "pullOutSelect" (formula "17") (term "0,0,0,1,1,0") (inst "selectSK=SumAndMax_max_1:int")) + (rule "applyEq" (formula "18") (term "1,1,0,0,0") (ifseqformula "1")) + (rule "applyEq" (formula "18") (term "1,1,0,1,0,1,0") (ifseqformula "1")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "16"))) + (rule "polySimp_mulComm0" (formula "18") (term "0,0,1,1,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,0,0")) + (rule "replace_known_left" (formula "1") (term "0,1,0,0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (builtin "One Step Simplification" (formula "1")) + (rule "applyEqReverse" (formula "18") (term "1,1,0,1,0,1,0") (ifseqformula "1")) + (rule "applyEqReverse" (formula "18") (term "1,1,0,0,0") (ifseqformula "1")) + (rule "applyEqReverse" (formula "18") (term "1,0,0,1,1,0") (ifseqformula "1")) + (rule "hideAuxiliaryEq" (formula "1")) + (rule "replace_known_left" (formula "17") (term "0,1,0") (ifseqformula "5")) + (builtin "One Step Simplification" (formula "17") (ifInst "" (formula "3"))) + (rule "polySimp_mulComm0" (formula "17") (term "0,0,0")) + (rule "replace_known_left" (formula "17") (term "0,0") (ifseqformula "7")) + (builtin "One Step Simplification" (formula "17")) + (rule "Class_invariant_axiom_for_SumAndMax" (formula "17") (term "0") (ifseqformula "11")) + (builtin "One Step Simplification" (formula "17")) + (rule "allRight" (formula "17") (inst "sk=f_0:Field")) + (rule "allRight" (formula "17") (inst "sk=o_0:java.lang.Object")) + (rule "orRight" (formula "17")) + (rule "orRight" (formula "17")) + (rule "orRight" (formula "17")) + (rule "pullOutSelect" (formula "20") (term "0") (inst "selectSK=f_0_0:any")) + (rule "simplifySelectOfAnon" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "eqSymm" (formula "21")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "dismissNonSelectedField" (formula "1") (term "0,0,1,1,0,0")) + (rule "replace_known_right" (formula "1") (term "1,0,0") (ifseqformula "20")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfUnion" (formula "1") (term "0,0,0")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0,0,0") (ifseqformula "19")) + (builtin "One Step Simplification" (formula "1")) + (rule "elementOfSingleton" (formula "1") (term "0,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0,0") (ifseqformula "18")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "19")) + (builtin "One Step Simplification" (formula "1")) + (rule "simplifySelectOfStore" (formula "1")) + (builtin "One Step Simplification" (formula "1")) + (rule "castDel" (formula "1") (term "1,0")) + (rule "eqSymm" (formula "1") (term "0,0,0")) + (rule "eqSymm" (formula "1") (term "1,0,0")) + (rule "replace_known_right" (formula "1") (term "0,0") (ifseqformula "18")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "21"))) + (rule "closeFalse" (formula "1")) + ) + ) + (branch "Null Reference (k < _a.length = null)" + (rule "false_right" (formula "19")) + (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "18"))) + (rule "closeFalse" (formula "1")) + ) +) +) +} diff --git a/keyext.slicing/src/test/resources/testcase/issues/3834/SumAndMax.java b/keyext.slicing/src/test/resources/testcase/issues/3834/SumAndMax.java new file mode 100644 index 00000000000..f0b8302b959 --- /dev/null +++ b/keyext.slicing/src/test/resources/testcase/issues/3834/SumAndMax.java @@ -0,0 +1,39 @@ +class SumAndMax { + + int sum; + int max; + + /*@ normal_behaviour + @ requires (\forall int i; 0 <= i && i < a.length; 0 <= a[i]); + @ assignable sum, max; + @ ensures (\forall int i; 0 <= i && i < a.length; a[i] <= max); + @ ensures (a.length > 0 + @ ==> (\exists int i; 0 <= i && i < a.length; max == a[i])); + @ ensures sum == (\sum int i; 0 <= i && i < a.length; a[i]); + @ ensures sum <= a.length * max; + @*/ + void sumAndMax(int[] a) { + sum = 0; + max = 0; + int k = 0; + + /*@ loop_invariant + @ 0 <= k && k <= a.length + @ && (\forall int i; 0 <= i && i < k; a[i] <= max) + @ && (k == 0 ==> max == 0) + @ && (k > 0 ==> (\exists int i; 0 <= i && i < k; max == a[i])) + @ && sum == (\sum int i; 0 <= i && i < k; a[i]) + @ && sum <= k * max; + @ + @ assignable sum, max; + @ decreases a.length - k; + @*/ + while(k < a.length) { + if(max < a[k]) { + max = a[k]; + } + sum += a[k]; + k++; + } + } +}