pith. sign in

arxiv: 2605.16820 · v2 · pith:Q4EHHSGGnew · submitted 2026-05-16 · 💻 cs.LO

Satisfiability Modulo Extensional Constant Arrays (Extended Version)

Mathias Preiner , Aina Niemetz , Clark Barrett This is my paper

Pith reviewed 2026-05-20 15:28 UTC · model grok-4.3

classification 💻 cs.LO
keywords satisfiability modulo theoriesarraysconstant arraysdecision procedureextensional arraysSMT solvingverificationabstract calculus
0
0 comments X

The pith

A decision procedure for arrays with constant values supports arbitrary index domains including finite ones.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents a novel decision procedure for the theory of extensional arrays augmented with constant arrays. This extension allows succinct representation of arrays initialized to a default value, which is common in verification tasks. The procedure works for any index domain, not just infinite ones, and is formalized as an abstract calculus shown to be sound for both refutation and satisfiability. It has been implemented in the Bitwuzla SMT solver and tested on various benchmarks.

Core claim

We present a novel decision procedure for the theory of arrays with constant arrays that supports arbitrary index domains and is not limited to the infinite case. We present our procedure as an abstract calculus and show its refutational and satisfiability soundness.

What carries the argument

An abstract calculus extending the extensional array theory with rules for constant arrays and their interactions with reads, writes, and extensionality.

If this is right

  • Verification tasks involving arrays with default values can be decided without restrictions on index domains.
  • The procedure enables complete handling of finite index domains such as those using machine integers.
  • Existing SMT solvers can be extended with this calculus to improve support for constant arrays.
  • Performance evaluations show benefits on diverse benchmarks from hardware and software verification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This approach might generalize to other SMT theories with default value constructs.
  • Combining it with bit-vector theories could enhance verification of low-level array operations.
  • Further optimizations could focus on efficient implementation for specific finite domains like 32-bit integers.

Load-bearing premise

The abstract calculus accurately models the semantics of constant arrays for finite index domains and can be implemented efficiently.

What would settle it

A formula with a constant array over a finite index domain that is satisfiable but the procedure declares unsatisfiable, or vice versa.

Figures

Figures reproduced from arXiv: 2605.16820 by Aina Niemetz, Clark Barrett, Mathias Preiner.

Figure 1
Figure 1. Figure 1: Visualization of the interpretation satisfying formula φ∧v ̸≈ w from Example 2. indices. In other words, interpretation I satisfies formula sv ≈ sw ∧v ̸≈ w if and only if σ I = {i I 1 , . . . , iI l , jI 1 , . . . , jI k }. For any number of array stores l + k < n, the equality does not hold since sv and sw differ on at least n − (l + k) indices. Thus, the main challenge of deciding the equality of two sto… view at source ↗
Figure 2
Figure 2. Figure 2: AEXT rules for non-extensional arrays. RowU I |= i ̸≈ j a⟨j ◁ u⟩ ∈ T(A) π(a, b[i]) ̸= () π(a⟨j ◁ u⟩, b[i]) = () π(a⟨j ◁ u⟩, b[i]) := (i ̸≈ j, a) EqR I |= a ≈ c a, c ∈ TA(A) a ≈ c ∈ T(A) π(a, b[i]) ̸= () π(c, b[i]) = () π(c, b[i]) := (a ≈ c, a) EqL I |= a ≈ c a, c ∈ TA(A) a ≈ c ∈ T(A) π(c, b[i]) ̸= () π(a, b[i]) = () π(a, b[i]) := (a ≈ c, c) DisEq I |= a ̸≈ c a, c ∈ TA(A) a ≈ c ∈ T(A) k{a,c} ̸∈ T(A) A := A,… view at source ↗
Figure 3
Figure 3. Figure 3: AEXT rules for extensional arrays [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: CAEXT rule for non-extensional constant arrays. InitC ⟨v⟩ ∈ T(A) π(⟨v⟩,⟨v⟩) := (⊤,⟨v⟩) CowD π(a⟨j ◁ u⟩,⟨v⟩) ̸= () π(a,⟨v⟩) = () I |= ∃i : σ. ^ k∈I(a⟨j◁u⟩,⟨v⟩)∪{j} i ̸≈ k π(a,⟨v⟩) := (⊤, a⟨j ◁ u⟩) CowU π(a,⟨v⟩)̸= () π(a⟨j ◁ u⟩,⟨v⟩)= () a⟨j ◁ u⟩ ∈ T(A) I |= ∃i : σ. ^ k∈I(a,⟨v⟩)∪{j} i ̸≈ k π(a⟨j ◁ u⟩,⟨v⟩) := (⊤, a) CEqR I |= a ≈ c a, c ∈ TA(A) a ≈ c ∈ T(A) π(a,⟨v⟩) ̸= () π(c,⟨v⟩) = () π(c,⟨v⟩) := (a ≈ c, a) C… view at source ↗
Figure 5
Figure 5. Figure 5: CAEXT rules for extensional constant arrays. at the same index. Recall that with π(a, b[i]) ̸= () and π(a, c[k]) ̸= (), we have that b[i] is a representative of a[i] and c[k] is a representative of a[k] under the current interpretation I. However, if I |= i ≈ k ∧ b[i] ̸≈ c[k], the congruence axiom of TE is violated since i ≈ k ∧b[i] ≈ a[i]∧c[k] ≈ a[k] =⇒ b[i] ≈ c[k]. As a result, CongR adds a lemma to A to… view at source ↗
read the original abstract

Reasoning about array data structures is a key requirement for many applications in hardware and software verification, especially in combination with machine integers. The Satisfiability Modulo Theories (SMT) theory of extensional arrays provides array read and write operators and allows extensionality over arrays. This is sufficient to express many aspects of computer-aided verification, but lacks succinctness to efficiently deal with arrays that are initialized with a default value. Existing procedures for extending the SMT-LIB theory of arrays with support for constant arrays are limited to arrays with infinite index domains, and existing implementations in SMT solvers only support a fragment of the theory for finite index domains. In this paper, we present a novel decision procedure for the theory of arrays with constant arrays that supports arbitrary index domains and is not limited to the infinite case. We present our procedure as an abstract calculus and show its refutational and satisfiability soundness. We implement a decision procedure based on our calculus in the state-of-the-art SMT solver Bitwuzla and evaluate its performance on a diverse collection of benchmarks and use cases.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper presents a novel decision procedure for the SMT theory of extensional arrays extended with constant arrays. The procedure supports arbitrary index domains (including finite ones) and is given as an abstract calculus for which refutational and satisfiability soundness are claimed. An implementation in Bitwuzla is described together with benchmark evaluations on diverse use cases.

Significance. If the soundness claims hold, the work removes a long-standing restriction in array decision procedures to infinite index domains, enabling more succinct encodings for arrays initialized to a default value in hardware and software verification. The explicit abstract calculus, soundness arguments, and practical implementation in a state-of-the-art solver constitute clear strengths; the benchmark results further indicate that the approach is viable beyond the theoretical setting.

major comments (1)
  1. [§4] §4, Definition of the abstract calculus rules: the rules for handling constant arrays over finite index domains are stated without an explicit cardinality guard or reduction step; it is therefore unclear whether the rules remain complete when the index domain has size smaller than the number of distinct constants appearing in the formula (this is load-bearing for the central claim of support for arbitrary finite domains).
minor comments (2)
  1. [§2] The paper would benefit from an explicit statement of the SMT-LIB array theory signature used (including the exact sort declarations for constant arrays) in §2 to facilitate comparison with prior work.
  2. [Figure 3] Figure 3 (benchmark results) lacks error bars or variance information across the 10 runs; adding this would strengthen the performance claims.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of our manuscript, the positive recommendation for minor revision, and the insightful comment on the abstract calculus. We address the major comment point by point below and will incorporate clarifications in the revised version.

read point-by-point responses

  1. Referee: [§4] §4, Definition of the abstract calculus rules: the rules for handling constant arrays over finite index domains are stated without an explicit cardinality guard or reduction step; it is therefore unclear whether the rules remain complete when the index domain has size smaller than the number of distinct constants appearing in the formula (this is load-bearing for the central claim of support for arbitrary finite domains).

    Authors: We thank the referee for identifying this point of potential unclarity. The abstract calculus in §4 is defined as a set of rules to be used in combination with a decision procedure for the index theory (which may be finite). When the index domain is finite, its cardinality constraints are enforced by the index theory solver itself; any attempt to introduce more distinct index elements or value distinctions than the domain permits leads to a conflict detected in the index theory, which is then propagated to derive unsatisfiability in the combined procedure. Thus the array rules do not require an additional explicit cardinality guard, as completeness follows from the modular combination. Nevertheless, we agree that the current presentation could be clearer on this interaction. In the revised manuscript we will add a short explanatory paragraph and a small illustrative example in §4 showing how finite-domain cardinality is handled via the index theory, thereby making the support for arbitrary finite domains fully explicit. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper presents a novel abstract calculus for deciding satisfiability in the theory of extensional arrays extended with constant arrays over arbitrary index domains (including finite ones). It supplies independent refutational and satisfiability soundness arguments for the calculus itself. No load-bearing step reduces by construction to a fitted parameter, a self-citation chain, or an ansatz imported from prior work by the same authors; the central claims rest on the explicit soundness proofs and the implementation/evaluation in Bitwuzla rather than on renaming or re-deriving inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard background from SMT array theory but introduces no new free parameters or invented entities; the contribution is the decision procedure itself.

axioms (1)
  • standard math The base SMT theory of extensional arrays with read and write operators is well-defined and decidable in the relevant fragments.
    Invoked as the foundation being extended with constant arrays.

pith-pipeline@v0.9.0 · 5719 in / 1071 out tokens · 44800 ms · 2026-05-20T15:28:43.686806+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

35 extracted references · 35 canonical work pages

  1. [1]

    https://fmv.jku.at/hwmcc19/ (2019)

    Hardware Model Checking Competition 2019. https://fmv.jku.at/hwmcc19/ (2019)

    work page 2019

  2. [2]

    https://hwmcc.github.io/2020/ (2020)

    Hardware Model Checking Competition 2020. https://hwmcc.github.io/2020/ (2020)

    work page 2020

  3. [3]

    https://github.com/bitwuzla/bitwuzla/ (2026)

    Bitwuzla on GitHub. https://github.com/bitwuzla/bitwuzla/ (2026)

    work page 2026

  4. [4]

    hevm symbolic execution engine SMT queries (2026), https://github.com/SMT-LIB/pending-benchmarks/commit/ 0a87f2c7581a3df7ad0f2d7b57621b6ecf4637ad

    work page 2026

  5. [5]

    https://github.com/Z3Prover/z3/ (2026)

    Z3 on GitHub. https://github.com/Z3Prover/z3/ (2026)

    work page 2026

  6. [6]

    ACM Comput

    Baldoni, R., Coppa, E., D’Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv.51(3), 50:1–50:39 (2018). https://doi.org/10.1145/3182657

    work page doi:10.1145/3182657 2018

  7. [7]

    In: Fisman, D., Rosu, G

    Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., N¨ otzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems...

    work page doi:10.1007/978-3-030-99524-9 2022

  8. [8]

    Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.7. Tech. rep., Department of Computer Science, The University of Iowa (2025), available at http://smt-lib.org

    work page 2025

  9. [9]

    In: Brinksma, E., Larsen, K.G

    Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Den- mark, July 27-31, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2404, pp. 236–249. Springer (2002)....

    work page doi:10.1007/3-540-45657-0 2002

  10. [10]

    In: Narodytska, N., R¨ ummer, P

    Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2024. In: Narodytska, N., R¨ ummer, P. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024. p. 1. IEEE (2024). https://doi.org/10.34727/2024/ISBN.978-3-85448-065-5 6

    work page doi:10.34727/2024/isbn.978-3-85448-065-5 2024

  11. [11]

    In: Irfan, A., Kaufmann, D

    Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition 2025. In: Irfan, A., Kaufmann, D. (eds.) Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, Octo- ber 6-10, 2025. TU Wien Academic Press (2025). https://doi.org/10.34727/2025/ ISBN.978-3-85448-084-6 6

    work page doi:10.34727/2025/ 2025

  12. [12]

    Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of ar- rays. J. Satisf. Boolean Model. Comput.6(1-3), 165–201 (2009). https://doi.org/ 10.3233/SAT190067

    work page doi:10.3233/sat190067 2009

  13. [13]

    In: Donaldson, A.F., Parker, D

    Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A.F., Parker, D. (eds.) Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7385, pp. 248–254. Springer (2012). https://doi.org/10. 1007/978-3-642-31759-0 19

    work page 2012

  14. [14]

    In: Piterman, N., Smolka, S.A

    Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Con- struction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Soft- ware, ETAPS 2013, Rome, Italy, March 16-24,...

    work page 2013

  15. [15]

    (eds.): Handbook of Model Checking

    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8, ISBN 978- 3-319-10574-1

    work page doi:10.1007/978-3-319-10575-8 2018

  16. [16]

    In: Biere, A., Bloem, R

    Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer Aided Ver- ification - 26th International Conference, CAV 2014, Held as Part of the Vi- enna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceed- ings. pp. 737–744. Lecture Notes in Computer Science, Springer (2014). https: //doi.org/10.1007/978-3-319-08867-9 49

    work page doi:10.1007/978-3-319-08867-9 2014

  17. [17]

    In: Gurfinkel, A., Ganesh, V

    Dxo, Soos, M., Paraskevopoulou, Z., Lundfall, M., Brockman, M.: Hevm, a fast symbolic execution framework for EVM bytecode. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 453–465. Spri...

    work page 2024

  18. [18]

    Academic Press (1972), ISBN 978-0-12-238450-9

    Enderton, H.B.: A mathematical introduction to logic. Academic Press (1972), ISBN 978-0-12-238450-9

    work page 1972

  19. [19]

    In: Bouajjani, A., Maler, O

    Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in sat- isfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 306–320. Springer (2009). https://doi....

    work page doi:10.1007/978-3-642-02658-4 2009

  20. [20]

    In: Enea, C., Piskac, R

    Hoenicke, J., Schindler, T.: Solving and interpolating constant arrays based on weak equivalences. In: Enea, C., Piskac, R. (eds.) Verification, Model Check- ing, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings. Lecture Notes in Com- puter Science, vol. 11388, pp. 297–317. Spring...

    work page 2019

  21. [21]

    In: Silva, A., Leino, K.R.M

    Mann, M., Irfan, A., Lonsing, F., Yang, Y., Zhang, H., Brown, K., Gupta, A., Barrett, C.W.: Pono: A flexible and extensible smt-based model checker. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760,...

    work page doi:10.1007/978-3-030-81688-9 2021

  22. [22]

    In: Many-sorted logic and its applications, pp

    Manzano, M.: Introduction to many-sorted logic. In: Many-sorted logic and its applications, pp. 3–86. John Wiley & Sons, Inc., New York, NY, USA (1993), https://dl.acm.org/doi/10.5555/165446.165450, ISBN 0-471-93485-2

    work page doi:10.5555/165446.165450 1993

  23. [23]

    In: Information Processing, Proceedings of the 2nd IFIP Congress 1962, Munich, Germany, August 27 - September 1, 1962

    McCarthy, J.: Towards a mathematical science of computation. In: Information Processing, Proceedings of the 2nd IFIP Congress 1962, Munich, Germany, August 27 - September 1, 1962. pp. 21–28. North-Holland (1962)

    work page 1962

  24. [24]

    In: The 5th International Symposium on the Theory and Applications of Satisfiability Testing, SAT 2002, Cincinnati, USA (2002), https://leodemoura.github.io/files/sat02.pdf

    Moura, L.D., Rueß, H.: Lemmas on demand for satisfiability solvers. In: The 5th International Symposium on the Theory and Applications of Satisfiability Testing, SAT 2002, Cincinnati, USA (2002), https://leodemoura.github.io/files/sat02.pdf

    work page 2002

  25. [25]

    In: Ramakrishnan, C.R., Rehof, J

    de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedi...

    work page 2008

  26. [26]

    In: Proceedings of 9th International Conference on Formal Methods in Computer- Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA

    de Moura, L.M., Bjørner, N.S.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer- Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA. pp. 45–

    work page 2009

  27. [27]

    https://doi.org/10.1109/FMCAD.2009.5351142

    IEEE (2009). https://doi.org/10.1109/FMCAD.2009.5351142

    work page doi:10.1109/fmcad.2009.5351142 2009

  28. [28]

    In: Enea, C., Lal, A

    Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 3–17. Springer (2023). https://doi.org/10.1007/978-3-031-37703-7 1

    work page doi:10.1007/978-3-031-37703-7 2023

  29. [29]

    In: Chockler, H., Weissenbacher, G

    Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2 , BtorMC and Boolec- tor 3.0. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verifica- tion - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, p...

    work page doi:10.1007/978-3-319-96145-3 2018

  30. [30]

    In: Gurfinkel, A., Ganesh, V

    Niemetz, A., Preiner, M., Zohar, Y.: Scalable bit-blasting with abstractions. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 178–200. Springer (2024). https://doi.org/10.1007/978-3-031...

    work page doi:10.1007/978-3-031-65627-9 2024

  31. [31]

    Preiner, M.: Lambdas, Arrays and Quantifiers. Ph.D. thesis, Informatik, Johannes Kepler University Linz (2017), https://resolver.obvsg.at/urn:nbn:at:at-ubl:1-14897

    work page 2017

  32. [32]

    In: Ganai, M.K., Sen, A

    Preiner, M., Niemetz, A., Biere, A.: Lemmas on demand for lambdas. In: Ganai, M.K., Sen, A. (eds.) Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems, Portland, OR, USA, October 19, 2013. CEUR Workshop Proceedings, vol. 1130. CEUR-WS.org (2013), https: //ceur-ws.org/Vol-1130/paper 7.pdf

    work page 2013

  33. [33]

    https://doi.org/10.5281/ ZENODO.15493095

    Preiner, M., Schurr, H., Barrett, C.W., Fontaine, P., Niemetz, A., Tinelli, C.: SMT- LIB release 2025 (incremental benchmarks) (May 2025). https://doi.org/10.5281/ ZENODO.15493095

    work page 2025

  34. [34]

    https://doi.org/10

    Preiner, M., Schurr, H., Barrett, C.W., Fontaine, P., Niemetz, A., Tinelli, C.: SMT- LIB release 2025 (non-incremental benchmarks) (Aug 2025). https://doi.org/10. 5281/ZENODO.15493089

    work page 2025

  35. [35]

    In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings

    Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an ex- tensional theory of arrays. In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. pp. 29–37. IEEE Computer Society (2001). https://doi.org/10.1109/LICS.2001.932480 Appendix In this appendix, we prove refutat...

    work page doi:10.1109/lics.2001.932480 2001