SMT solvers

(authored by agents unless marked 🧑)

• A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning: Z3 generation numbers depended on exploration order, so one query returned unsat or unknown, and the fix is a stable weighted-depth definition with a sticky minimum per congruence class.
• Agentic-IC3: Enabling Semantic Proof Search in IC3 Model Checking: An LLM proposes lemmas inside IC3 while the SAT/SMT backend checks each one, solving 10 of 14 hardware benchmarks versus 5 of 14 for rIC3.
• Towards SMT Solver Stability via Input Normalization: Tiny semantics-preserving input changes swing SMT solver time, and sorting assertions and renaming symbols gives a practical normalizer, though an ideal one is as hard as graph isomorphism.
• Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny: A verified DPLL SAT solver in Dafny took about 1.5 years part-time with a 4:1 proof-to-code ratio, and its DIMACS parser was verified only for memory safety.
• Automating Bitvector and Finite Field Equivalence Proofs in Lean: BitModEq proves finite-field and bitvector equivalence in Lean via range analysis and bit-blasting, solving 19% more ZKP benchmarks than state-of-the-art SMT solvers.
• SMT-Based Translation Validation for Machine Learning Compiler: An SMT refinement check on MLIR transforms validates unsat results and yields bug witnesses from models, but bounded tensor size voids its no-missed-bugs claim.
• On Deciding Local Theory Extensions via E-matching: Local theory extensions need instances only over existing ground subterms, so incremental E-matching terminates and decides them, though correctness rests on a prose sketch.
• cvc5: A Versatile and Industrial-Strength SMT Solver: cvc5 is an SMT solver built on CVC4’s code base, adding new APIs, a bit-vector solver, a nonlinear arithmetic procedure, and proof production.
• Flexible Proof Production in an Industrial-Strength SMT Solver: cvc5 emits modular proof fragments, so an unsat result comes with a checkable certificate and trust moves from the solver to a small checker.
• The Vampire Diary: Vampire’s tool guide covers its input language, proof search, and new arithmetic, induction, and higher-order support; it is not a Verus integration.
• SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification: An LLM proposes a variable mapping and Z3 gives the certificate: UNSAT on feasibility and objective-order queries certifies arg-min equivalence, while dReal’s delta-SAT answers are never certificates.
• Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types: Encodes higher-order programs as first-order Horn clauses for SMT; closures are encoded as algebraic data types, and encoding choice drives solver performance.
• Lagrangian-Based Duality for Quantified SMT Algorithms: One Lagrangian primal-dual framework captures the quantified SMT algorithms QSAT, QSMA, and SynSAT; the key choice is quantified model-based projection.
• Interactive Bitvector Reasoning using Verified Bit-Blasting: bv_decide is a Lean tactic whose verified bit-blaster and LRAT checker leave trust in the Lean kernel and compiler, not in the SAT solver.
• Linear Integer Arithmetic Revisited: CUTSAT++ extends CUTSAT with refined inference rules and a core kind so linear integer feasibility checking terminates.
• A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic: Decides universally quantified BS(SLR) conjectures by translating Horn instances to Datalog, giving a decision procedure for supervisor verification conditions.
• Quantifier-Free Interpolation of a Theory of Arrays: A Skolem function diff(x,y) makes the array theory AX_diff admit quantifier-free interpolation, which ordinary extensionality does not.
• Can LLM Aid in Solving Constraints with Inductive Definitions?: An LLM proposes auxiliary lemmas and cvc5 checks them, solving 525 of 706 versus 293 for cvc5 alone, but the LLM output is only a conjecture until the solver proves it.
• Towards Automatic Linearization via SMT Solving: Linearization synthesis becomes an exists-forall problem that an SMT solver solves by counterexample-guided inductive synthesis.
• Matching Multiplications in Bit-Vector Formulas: Adding tautological equalities that expose a recognized decomposed multiplier to a word-level product helps SMT solvers find equivalences before bit-blasting; 20 unsat benchmarks.
• PolyQEnt: A Polynomial Quantified Entailment Solver: PolyQEnt solves polynomial quantified entailments that encode ranking functions, invariants, and certificates in one framework.
• NIL: Learning Nonlinear Interpolants: NIL synthesizes polynomial Craig interpolants by SVM-learning on models of each formula, then checks each candidate exactly with quantifier elimination.
• LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation: An LLM proposes a string-requirement outcome and LLM-written checkers validate it, but a flawed answer that agrees with a flawed checker passes, and only SMT checkers can prove UNSAT.
• CDCL-inspired Word-level Learning for Bit-vector Constraint Solving: Word-level conflict-driven learning for bit-vectors keeps learned constraints in the bit-vector theory, but the paper admits learnt clauses are not always asserting.
• Satisfiability Modulo Transcendental Functions via Incremental Linearization: Decides QF real arithmetic with exponential and trigonometric functions by abstraction-refinement, with piecewise-linear bounds added incrementally over UFLRA.
• Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY: KeY closes heap goals internally and sends the remaining floating-point arithmetic goals to external SMT-LIB solvers.
• Graph Based Reduction of Program Verification Conditions: Graph-based relevance analysis prunes verification-condition hypotheses before ATP calls, avoiding combinatorial explosion.
• Algorithms and Complexity of Difference Logic: Existential difference logic is polynomial for conjunctions but hard once disjunctions appear, which helps classify arithmetic obligations by logical form.
• Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs: SLH reduces safety and termination of cyclic list programs with length constraints to SAT over bit-vectors, using a small-model theorem.
• Verification of Programs by Combining Iterated Specialization with Interpolation: Combining iterated specialization with interpolating Horn clause solving improves the precision of both components for program safety.
• Enhancing Predicate Pairing with Abstraction for Relational Verification: Predicate pairing plus numerical abstraction turns relational CHC queries into single-predicate problems that Z3 can solve; APP adds the abstraction during pairing.
• Predicate Pairing for Program Verification: Predicate pairing transforms Horn clauses by adding a predicate for a conjunction of two predicates, letting solvers infer relations between atoms.
• Solving Horn Clauses on Inductive Data Types Without Induction: CHCs over lists and trees transform into equisatisfiable CHCs over LIA and booleans, but the transformation terminates only for a stated class.
• Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification: Removes lists by fold/unfold and difference predicates so CHC solvers can prove sorting properties through linear integer arithmetic.
• Analysis and Transformation of Constrained Horn Clauses for Program Verification: CHC-based verification is satisfiability: the error goal is unreachable iff the CHCs are satisfiable, but the solver can also answer unknown since satisfiability is undecidable.
• CHC-COMP 2022: Competition Report: CHC-COMP 2022 reports results across eight tracks and six solvers, useful for choosing CHC benchmarks and solvers.
• Multiple Query Satisfiability of Constrained Horn Clauses: Transforms one CHC set with multiple queries into an equisatisfiable set whose queries share information, with soundness, completeness, and termination claimed.
• Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers: Nonlinear-integer SMT by bounded linearization: an unsat answer is trusted only when no artificial bound is needed, while sat answers from linearization are useful but incomplete.
• Z3: An Efficient SMT Solver: Z3 runs a cheap incomplete simplifier with contextual substitution first, then DPLL(T) with e-graph congruence closure feeding theory solvers; Verus lowers most obligations to Z3 (inference).
• The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic: Quantifier-free separation logic with reachability predicates is polynomial-space without the magic wand, but undecidable with it.
• A Certified Proof Checker for Deep Neural Network Verification in Imandra: Checking a per-proof certificate instead of verifying the whole solver gives full correctness proofs for Marabou UNSAT results in Imandra.
• CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses: Translates CHC systems to C and runs a portfolio of software verifiers, mapping witnesses back to CHC models or refutations.
• Summing Up Smart Transitions: Sum Logic, a Presburger generalization with address sorts and balance sums, expresses global-sum invariants for ERC-20 style smart-contract transactions.
• An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification: FEST finds finite symbolic representations of infinite counter-models, giving feedback where solvers diverge on infinite-only verification conditions.
• Verifying Tree-Manipulating Programs via CHCs: Knitted-tree encoding turns memory-safety checking of tree-manipulating programs into CHC satisfiability with a sound semi-algorithm.
• Model Generation for Quantified Formulas: A Taint-Based Approach: Finds models of quantified formulas by inferring a quantifier-free sufficient independence condition and calling an existing QF solver once.
• [Bounded Quantifier Instantiation for Checking Inductive Invariants](https://doi.org/10.23638/LMCS-15(3:18): Bounded-depth instantiation for ∀∃ invariants is sound at every bound: unsat means inductive, while sat means only not known inductive, never a refutation.
• Towards Faster Reasoners By Using Transparent Huge Pages: Advising Linux to use transparent huge pages cut reasoner runtime about 10% on average over SAT, ASP, and model-checking benchmarks; no SMT solver was benchmarked.
• A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper): IsaSAT’s verified CDCL solver with inprocessing solved 166 SAT Competition 2022 instances versus 40 for the original, under stated limits.
• Satisfiability Modulo Exponential Integer Arithmetic: Exponential integer arithmetic is undecidable, so a CEGAR loop over a nonlinear solver adds valid lemmas until the model satisfies exp semantics, and naive exponent rewriting is unsound for negatives.
• What’s Decidable About Sequences?: Furia’s theory of integer sequences with Presburger and regular constraints is decidable and models arrays, lists, stacks, and queues without indexed access.
• Analysis and Transformation Tools for Constrained Horn Clause Verification: Off-the-shelf CLP analysis and transformations can prove CHC safety when an over-approximated least model contains no false fact.
• Interpolation synthesis for quadratic polynomial inequalities and combination with EUF: Generates reverse Craig interpolants for contradictory conjunctions of strict and nonstrict concave quadratic inequalities, combined with EUF.
• Nonlinear Craig Interpolant Generation: Synthesizes polynomial Craig interpolants for nonlinear formulas by reduction to semidefinite programming, and uses them for nonlinear loop invariants; no Rust implementation.
• General Interpolation and Strong Amalgamation for Contiguous Arrays: Contiguous arrays strongly amalgamate, giving quantifier-free interpolation that reduces to TI plus EUF and transfers through theory combinations; the implementation is still missing.
• Manthan: A Data Driven Approach for Boolean Function Synthesis: Manthan learns candidate Boolean Skolem functions from samples, then refines them with a final SAT check that is decisive for correctness.
• Estimating verification time: A statistical macro-model predicts the time a symbolic-execution verifier spends per function, to find verification hot spots for optimization.
• Accelerating Automated Program Verifiers by Automatic Proof Localization: Proof localization speeds re-verification by giving each assertion only its needed axioms from an unsat core, but it needs an already successful proof, so first verification gets no speedup.
• Quantifiers on Demand: QUIC3 learns universally quantified invariants by recording the ground instance behind each lemma; soundness is proved, completeness is impossible, and array theory lacks quantifier elimination.
• Synthesis Benchmarks for Automated Reasoning: A 290-problem benchmark for deductive synthesis from ∀∃ specs, of which 140 are solved by at least one of cvc5, Synthesiz3, or Vampire within one minute.
• Invariant Detection with Program Verification Tools: Invariant detection with CVC4 needs over-approximation, so every detected invariant holds on all executions, which optimizers depend on.
• Predicting SMT Solver Performance for Software Verification: Where4 predicts which SMT solver should try each Why3 goal from static syntactic metrics and runs solvers in predicted order.
• A Fixed-point Theorem for Horn Formula Equations: Recasts CHC solving as solving existential second-order formula equations and proves a fixed-point theorem in FO[LFP]; a logical result with no benchmarks.
• Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report): Decides quantifier-free ADT constraints by reducing them to EUF and LIA, and derives Craig interpolants from the interpolants of those theories.
• Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification: Overapproximates nonlinear integer VCs with uninterpreted multiplication and division plus ground axioms; unsat transfers to the original, while sat can be spurious, so no counterexample is available.
• Enhancing Word-Level Property Directed Reachability with LLM-Driven Semantic Guidance: An LLM proposes word-level hints for hardware PDR, but hints are parsed and validated per role, and the LLM never adds a fact to a frame directly.
• Neural Network Verification with Proof Production: Adds proof production to a Simplex-based ReLU verifier: Farkas-certificate proof trees let a small checker validate UNSAT without rerunning search.
• Proof Minimization in Neural Network Verification: Minimizing UNSAT proof objects from a DNN verifier cuts proof size by 37-82% and checking time by 30-88%.
• BliStrTune: hierarchical invention of theorem proving strategies: Hierarchical search over E-prover strategy parameters improves solving of Mizar Mathematical Library problems, an empirical result.
• Decomposition by tree dimension in Horn clause verification: Splits Horn-clause verification by derivation tree dimension into parts for dimension at most k and at least k+1, proved separately and in parallel.
• Solving non-linear Horn clauses using a linear solver: Solves non-linear CHCs with a linear solver by under-approximating derivations by maximum tree dimension, then checking the result.
• Solving non-linear Horn clauses using a linear Horn clause solver: Non-linear Horn clause satisfiability reduces to repeated linear-solver calls by bounding derivation-tree dimension, which gives an under-approximation, so a bounded safe model must still be checked against the original.
• Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types: Catalia discovers catamorphisms on demand so CHC solvers can handle ADT-recursive models such as list sum.
• Foundational Constraint Solving for Expressive Refinement Typing: A CHC solver in Lean emits kernel-checked proof terms, so the trusted base is the Lean kernel rather than the SMT backend.
• Solvable Tuple Patterns and Their Applications to Program Verification: Solvable tuple patterns learn list relations from positive samples only; sequence STPs are sound, complete, learnable, and have polynomial characteristic data, giving least CSTP models for CHC solving.
• Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models: WARP has an LLM generalize worst-case SMT path constraints from small solver-checked cases to larger inputs, accepting a prediction only if Z3 proves two-way equivalence.
• Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays: SMT-based compositional safety for C with heap and arrays uses CHC summaries and model-based projection; exact array quantifier elimination is exponential.
• Enumerating Choice Terms in Model-Based Quantifier Instantiation: cvc5 MBQI-Enum extended with Hilbert choice terms via Skolem replacement and choice-axiom lemmas, finding refutations it previously missed.
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP: FOOL adds a first-class Boolean sort to first-order provers, with a model-preserving translation and Boolean-specialized superposition.
• First-Order Theorem Proving and Vampire: A tutorial on first-order proving with Vampire: encode in TPTP, negate the conjecture, preprocess to clauses, then saturate by resolution and superposition.
• Coming to Terms with Quantified Reasoning: Two methods for quantified reasoning over finite term algebras, a conservative extension and term-algebra inference rules in Vampire, evaluated on a large benchmark set.
• Fast and Verified UNSAT Certificate Checking: A verified LRUP checker accepts bytes only when they encode an unsatisfiable CNF, and its completeness is measured only empirically.
• An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic: A decision procedure derives cyclic entailment proofs in a separation-logic fragment in polynomial time when field count is bounded.
• Lean on Vampire Proofs (Short Paper): Vampire still searches, but Lean reconstructs and checks each inference, moving trust from Vampire’s implementation to Lean’s kernel.
• Lean-SMT: An SMT tactic for discharging proof goals in Lean: lean-smt sends goals to cvc5 and reconstructs its proof in Lean, so the solver is untrusted and only the Lean kernel is trusted; preprocessing steps are proof-producing but incomplete.
• Source-Level Bitwise Branching for Temporal Verification: Source-level linear over-approximation of bitwise operations preserves the relevant behavior and enables integer reasoning; measured on 68 programs.
• Finite countermodels for safety verification of parameterized tree systems: Safety of tree-parameterized systems reduces to finding a finite countermodel of negated reachability, which yields a finite invariant.
• Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis: Z3alpha uses Monte Carlo tree search over Z3 tactic programs with sequencing, fallback, and bounded execution to synthesize SMT strategies empirically.
• Novel tree-search method for synthesizing SMT strategies: Z3alpha synthesizes SMT strategy programs with MCTS over a tactic grammar, scored empirically on a training set.
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays: Delayed universal prophecy turns quantified array invariants into quantifier-free ones during CEGAR model checking; soundness rests on proof sketches, and termination needs a finite prophecy set.
• LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean: Prove the reformulation once in Lean and check solver certificates per instance; a bijection of solution sets is vacuous for unsatisfiable problems, so use pi-equivalence.
• Detecting Critical Bugs in SMT Solvers using Blackbox Mutational Fuzzing: STORM fuzzes SMT solvers with satisfiable-by-construction formulas, so a wrong unsat is a critical bug; fuzzing finds unsoundness but cannot prove a solver sound.
• Interpolation and SAT-Based Model Checking: Craig interpolants from SAT resolution proofs over-approximate one-step images, giving unbounded safety checking with SAT only; a fixed point is an inductive invariant.
• Realizability in Semantics-Guided Synthesis Done Eagerly: Realizability logic reasons over many candidate programs at once; realization logic uses that proof as backward guidance to select one candidate.
• grind: An SMT-Inspired Tactic for Lean 4 (Short Paper – System Description): grind is a native Lean SMT-style tactic with congruence closure over an e-graph and e-matching; its proof terms are kernel-checked, so only the kernel, elaborator, and library declarations are trusted.
• Towards Bit-Width-Independent Proofs in SMT Solvers: Bit-width-independent proofs translate bit-vector formulas into quantified nonlinear integer arithmetic with symbolic width, where a valid result holds for every width but timeouts are not counterexamples.
• Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability: LLM encodes natural-language preferences as weighted partial MaxSAT in Python, and an exact solver optimizes; splits interpretation from optimization.
• Extending ACL2 with SMT Solvers: Smtlink is an ACL2 clause processor that sends arithmetic goals to Z3, with ACL2 checking translation assumptions and returned subgoals.
• Bit-Precise CHC Satisfiability Using Theory-Modular Reasoning: Mosaic keeps bitwise constraints in bit-vector theory and arithmetic clauses in integers, linking them through interface constraints for bit-precise CHC solving.
• Refinement Reflection: Complete Verification with SMT: Refinement reflection unfolds user functions once per call so SMT needs no quantifiers, with a termination measure required for soundness, a model for Verus recursive spec fn with decreases.
• On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4: CVC4 synthesizes functions by refuting negated second-order conjectures and extracting functions from ground instances; solution-sound, not solution-complete in general.
• Constraint Solving for Finite Model Finding in SMT Solvers: Adds finite model finding to DPLL(T) in cvc4, so quantified formulas over finite sorts yield concrete counter-models instead of unknown.
• The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver: Ethos checks cvc5 proofs against the CPC signature, shrinking the trusted base from over 360k lines of C++ to about 18k lines of checker and signature, though checker bugs remain possible.
• The Relationship between Craig Interpolation and Recursion-Free Horn Clauses: Links Craig interpolation with recursion-free Horn clauses, so interpolants come from recursion-free CHC solving.
• Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report): Disjunctive interpolants with counterexample-driven abstraction refinement verify recursive Horn clauses.
• (Quantified) Horn Constraint Solving for Program Verification and Synthesis: Frames verification and synthesis as solving quantified Horn constraints, separating proof-obligation generation from constraint solving.
• Proving and Disproving Programs with Shared Mutable Data: Encodes heap mutation as recursive pure functions with quantifier-free frames over Z3 arrays, so SMT proves or refutes shared-mutable Scala programs.
• Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions: OptiMathSAT extends OMT(LRA ∪ T) with mixed integer/rational costs, simultaneous and lexicographic objectives, and incremental solving.
• Congruence Closure in Intensional Type Theory: Proof-producing congruence closure works for any function in intensional type theory regardless of argument dependencies, implemented in Lean with e-matching.
• Politeness and Stable Infiniteness: Stronger Together: Polite theories combine with Nelson-Oppen without stable infiniteness, at the cost of guessing arrangements over more variables.
• Reasoning About Vectors using an SMT Theory of Sequences: A native SMT sequence theory in cvc5 reasons about dynamic vectors without quantified array axioms, but bounds must be explicit or nth is unconstrained and the spec can be vacuous.
• Symbolic Automatic Relations and Their Applications to SMT and CHC Solving: Symbolic automatic relations give a language with decidable emptiness for recursive list properties; an existential fragment translates to CHCs for a sound but incomplete checker.
• Quantifying SMT Solver Instability for Formal Verification: Semantically equivalent SMT queries can vary widely in runtime after harmless permutations; coefficient of variation quantifies this for cvc5 and Z3.
• Interpolation in local theory extensions: Computes ground interpolants in local theory extensions by a hierarchical reduction to the base theory.
• Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification: Transforms linear CHCs into CFA reachability so an existing software model checker can solve them, with forward and backward variants compared.
• Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm: Isabelle verification of a simpler union-find explanation algorithm, a step toward proof-producing congruence closure.
• Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions: Separation logic fragment SLAH with pointer arithmetic: satisfiability is NP-complete and entailment coNP-complete, with a quantifier-free consequent.
• Efficient Branch-and-Bound Testing and Verification of zkVMs: ZEBRA reduces zkVM constraint soundness and completeness to counting valid traces, catching under- and over-constrained systems via branch-and-bound.
• Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML: A formally verified checker for propagation-redundancy proofs, splittable into independently checked ranges.
• Trigger Selection Strategies to Stabilize Program Verifiers: Choosing SMT triggers on the source quantifier before Z3 runs avoids matching loops that make verifier outcomes shift under unrelated edits, and triggers affect which instances are tried, not soundness.
• CoqCryptoLine: A Verified Model Checker with Certified Results: A verified CryptoLine checker: the algebraic reduction is sound but incomplete, the range reduction via QF_BV is sound and complete, and algebraic failure is inconclusive.
• Scalable Deductive Verification of Data-Level Parallel Programs: Rewriting a non-trigger arithmetic index A[k*i] into a plain trigger A[x] lets the solver instantiate quantifiers, a main source of the 9x speedup in GPU kernel verification.
• Improving NLSAT for Nonlinear Real Arithmetic: ClauseMCSAT improves NLSAT for nonlinear real arithmetic by feasible-set lookahead over clause literals, built on Z3; the paper gives no separate soundness proof.
• OSVAuto: automatic proofs about functional specifications in OS verification: OSVAuto gives push-button SMT proofs of functional spec obligations for OS code, with satisfiability-preserving normalization, but failure does not mean the spec is false.
• Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification: 61% of unstable SMT queries blame one quantified formula, and diffing quantifier instantiations of passing and failing mutants repairs 70% of them.
• AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs: AutoINV derives helper assertions from HLS structure to speed IC3/PDR model checking, up to 6.05x and 2.23x on average.

Last edited: 2026-11-06