Enforce single-commit PR

Workflow runs for Enforce single-commit PR

• Enforce single-commit PR

  completed successfully:
  Enforce single-commit PR#986:Merge group checks requested
  Oct 30, 20268s
  More actions for workflow run 986

• Enforce single-commit PR

  completed successfully:
  Enforce single-commit PR#985:Merge group checks requested
  Oct 30, 20268s
  More actions for workflow run 985

• [documentation]: document while tactic

  failed:
  Enforce single-commit PR#984:Pull request#880synchronizebyfdupress
  doc-while-tactic

  Oct 30, 20266s
  More actions for workflow run 984

• [documentation]: document seq tactic

  completed successfully:
  Enforce single-commit PR#983:Pull request#879synchronizebyfdupress
  doc-seq-tactic

  Oct 30, 20267s
  More actions for workflow run 983

• [documentation]: document seq tactic

  failed:
  Enforce single-commit PR#982:Pull request#879synchronizebyfdupress
  doc-seq-tactic

  Oct 30, 20267s
  More actions for workflow run 982

• [docker] bump z3 5.3.2 to 5.3.3

  completed successfully:
  Enforce single-commit PR#981:Pull request#1225openedbyfdupress
  docker-z3-5.3.3

  Oct 30, 20263m 16s
  More actions for workflow run 981

• feat(theories): make FinType.card abstract, specified by card_spec

  requires action with the application:
  Enforce single-commit PR#980:Pull request#1224openedbymattc-try
  mattc-try:feat/fintype-abstract-card

  Oct 30, 2026Action required
  More actions for workflow run 980

• fix(phl): require the invariant on loop entry in the while variant rule

  completed successfully:
  Enforce single-commit PR#979:Pull request#1132synchronizebyYiping106283
  Yiping106283:fix-phoare-while-variant-entry

  Oct 30, 20267s
  More actions for workflow run 979

• fix(phl): check the bound of the upper-bound while rule on all memories

  completed successfully:
  Enforce single-commit PR#978:Pull request#1130synchronizebyYiping106283
  Yiping106283:fix-phoare-while-le-bound

  Oct 30, 20265s
  More actions for workflow run 978

• Enforce single-commit PR

  completed successfully:
  Enforce single-commit PR#977:Merge group checks requested
  Oct 29, 20266s
  More actions for workflow run 977

• fix(sim): eqobs_in must not assume an abstract call preserves glob A for distinct oracles

  completed successfully:
  Enforce single-commit PR#976:Pull request#1143synchronizebynamasikanam
  fix/eqobs-abs-oracle-glob

  Oct 29, 20268s
  More actions for workflow run 976

• Enforce single-commit PR

  completed successfully:
  Enforce single-commit PR#975:Merge group checks requested
  Oct 28, 20266s
  More actions for workflow run 975

• upgrade to why3 1.9.0

  completed successfully:
  Enforce single-commit PR#974:Pull request#1220synchronizebystrub
  why3-1.9

  Oct 28, 20266s
  More actions for workflow run 974

• upgrade to why3 1.9.0

  completed successfully:
  Enforce single-commit PR#973:Pull request#1220synchronizebystrub
  why3-1.9

  Oct 28, 20266s
  More actions for workflow run 973

• fix(fixpoint): matchfix termination check must descend into all call arguments

  completed successfully:
  Enforce single-commit PR#972:Pull request#1144synchronizebynamasikanam
  fix/matchfix-sibling-arg-termination

  Oct 28, 20267s
  More actions for workflow run 972

• perf(smt): no relevance tables when no lemma is to be selected

  completed successfully:
  Enforce single-commit PR#971:Pull request#1221synchronizebystrub
  perf/smt-given-lemmas

  Oct 28, 20268s
  More actions for workflow run 971

• perf(smt): no relevance tables when no lemma is to be selected

  completed successfully:
  Enforce single-commit PR#970:Pull request#1221synchronizebystrub
  perf/smt-given-lemmas

  Oct 28, 20262m 21s
  More actions for workflow run 970

• perf(smt): memories as abstract values, local variables as functions of them

  completed successfully:
  Enforce single-commit PR#969:Pull request#1222synchronizebystrub
  perf/smt-memory-locals

  Oct 28, 20265s
  More actions for workflow run 969

• perf(smt): memories as abstract values, local variables as functions of them

  failed:
  Enforce single-commit PR#968:Pull request#1222synchronizebystrub
  perf/smt-memory-locals

  Oct 28, 20267s
  More actions for workflow run 968

• perf(smt): memories as abstract values, local variables as functions of them

  completed successfully:
  Enforce single-commit PR#967:Pull request#1222openedbystrub
  perf/smt-memory-locals

  Oct 28, 20266s
  More actions for workflow run 967

• upgrade to why3 1.9.0

  completed successfully:
  Enforce single-commit PR#966:Pull request#1220synchronizebyfdupress
  why3-1.9

  Oct 28, 20266s
  More actions for workflow run 966

• fix(phl): check the bound of the upper-bound while rule on all memories

  failed:
  Enforce single-commit PR#965:Pull request#1130synchronizebyoskgo
  Yiping106283:fix-phoare-while-le-bound

  Oct 27, 20267s
  More actions for workflow run 965

• fix(phl): require the invariant on loop entry in the while variant rule

  failed:
  Enforce single-commit PR#964:Pull request#1132synchronizebyoskgo
  Yiping106283:fix-phoare-while-variant-entry

  Oct 27, 20267s
  More actions for workflow run 964

• perf(smt): no relevance tables when no lemma is to be selected

  completed successfully:
  Enforce single-commit PR#963:Pull request#1221synchronizebystrub
  perf/smt-given-lemmas

  Oct 27, 20267s
  More actions for workflow run 963

• perf(smt): no relevance tables when no lemma is to be selected

  completed successfully:
  Enforce single-commit PR#962:Pull request#1221openedbystrub
  perf/smt-given-lemmas

  Oct 27, 20268s
  More actions for workflow run 962