Inductive Approach to Spacer
TAKESHI TSUKADA, Chiba University, JapanHIROSHI UNNO, Tohoku University, JapanThe constrained Horn clause satisfiability problem is at the core of many automated verification methods, andSpacer is one of the most efficient solvers of this problem. The standard description of Spacer is based on an
abstract transition system, dividing the whole procedure into small rules. This division makes individual rules
easier to understand but, conversely, makes it difficult to discuss the procedure as a whole. As evidence ofthe difficulty in understanding the whole procedure, we point out that the claimed refutational completenessactually fails for several reasons, some of which were not present in the original version and subsequently
added. It is also difficult to grasp the differences between Spacer and another procedure, such as GPDR.
This paper aims to provide a better understanding of Spacer by developing a Spacer-like procedure definedby structural induction. We first formulate the problem to be solved inductively, then give its naïve solver
and transform it to obtain a Spacer-like procedure. Interestingly, our inductive approach almost unifies
Spacer and GPDR, which differ in only one respect in our understanding. To demonstrate the usefulness of
our inductive approach in understanding Spacer, we examine Spacer variants in the literature in terms of
inductive procedures and discuss why they are not refutationally complete and how to fix them. We also
implemented the proposed procedure and evaluated it experimentally.
CCS Concepts: • Theory of computation → Logic and verification; Program verification; Invariants.
Additional Key Words and Phrases: constrained Horn clause, model-based projection, tree interpolation,
refutational completeness
ACM Reference Format:
Takeshi Tsukada and Hiroshi Unno. 2024. Inductive Approach to Spacer. Proc. ACM Program. Lang. 8, PLDI,
Article 227 (June 2024), 24 pages. https://doi.org/10.1145/3656457

1 INTRODUCTION
The satisfiability problem for constrained Horn clauses (or CHCs) is the problem of asking whether
a given finite set of logical formulas with predicate variables has a solution, i.e. an assignment
to predicate variables that makes all formulas in the given set valid. Many verification problems
are reducible to this problem. The most important problem is the safety verification of a while
language and a language with first-order functions, which is actually equivalent to the satisfiability
problem for CHCs. Other more complicated problems may not be completely reducible to the
CHC satisfiability problem, but many sound though incomplete translations have been proposed
and implemented: Examples include refinement type inference [Rondon et al. 2008; Unno andKobayashi 2009] and validity checking of fixpoint logic formulas [Kobayashi et al. 2019].
Because of its practical significance, the study of efficient solvers is quite vast, particularly if asoftware model checker is regarded as a CHC solver through the above-mentioned equivalence.
As for the subclass known as linear CHC, an approach called property-directed reachability [Bradley2011; Een et al. 2011] (or PDR) has been recognized as a quite efficient procedure. PDR was originally
Authors’ addresses: Takeshi Tsukada, Chiba University, Chiba, Japan, t.tsukada@acm.org; Hiroshi Unno, Tohoku University,
Sendai, Japan, hiroshi.unno@acm.org.

This work is licensed under a Creative Commons Attribution 4.0 International License.
© 2024 Copyright held by the owner/author(s).
ACM 2475-1421/2024/6-ART227
https://doi.org/10.1145/3656457
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:2

Takeshi Tsukada and Hiroshi Unno

proposed as a solver of finite model-checking that corresponds to linear CHCs over finite data
domain, and Hoder and Bjørner [2012] applied the idea to non-linear CHCs over infinite data
domain. Their procedure is often referred to as GPDR.
Furthering these ideas, Komuravelli et al. [2014, 2016] developed Spacer, which is currently oneof the most efficient CHC solvers. A motivation for the development is the lack of refutational
completeness of GPDR. Spacer is based on several new ideas, but the key to refutational completeness is a technique called model-based projection. It is used to divide the set of local candidatesof counterexamples into a finite number of classes, and the finiteness of the classes allows an
exhaustive search for candidates of global counterexamples in a finite number of steps.
Unfortunately, the behavior of Spacer is quite difficult to understand properly. This fact isindicated by the confusion about its refutational completeness. First, Spacer has been proved
to be refutationally complete independent of the choice of the backend model-based projection
procedure in Komuravelli et al. [2016], but Tsukada and Unno [2022] have shown that Spacer
is not refutationally complete for a badly chosen model-based projection procedure.1 Second,
Komuravelli et al. [2015] discussed a variant of Spacer and claimed its refutational completenesswithout examining the differences, but the procedure of Komuravelli et al. [2015] has other sourcesof incompleteness in addition to that of the original spacer [Komuravelli et al. 2014, 2016] as weshall see later. These problems and related subtleties of Spacer have been overlooked even though
the Spacer papers [Komuravelli et al. 2014, 2016] had many followers.
This paper aims to improve our understanding of Spacer. The ultimate goal is to improve
the performance of Spacer, but this ambitious goal is left for future work. We demonstrate theusefulness of our approach by making the aforementioned arguments on refutational completenessunderstandable to readers who are not necessarily familiar with Spacer.
Our approach. Whereas Spacer is usually described as an abstract transition system, this paper
describes Spacer as an inductive procedure. In the traditional description, Spacer is expressed
as a collection of transition rules, each of which has an intuitive exposition. However, the understandability of each rule does not necessarily imply the understandability of the entire system. We
provide an inductive description, from which one can grasp the entire structure.
Our development proceeds as follows. We first formulate the problem that our procedures
solve by induction. The CHC solving does not suit induction (as is perhaps well-known; see
Section 4.1), so we introduce an alternative, named the generalized refinement problem, suitablefor inductive produces. It has a naïve inductive solver (Algorithm 3), and other more efficient
procedures (Algorithm 5 and Algorithm 6) can be obtained by rewriting the naïve one. In therewriting, we replace the quantifier elimination in the naïve solver with model-based projection andthen make the procedure as lazy as possible (i.e. deferring computations that are not immediately
necessary to later). The deferring process needs much care since we exchange effectful instructions.
The resulting procedures (Algorithm 5 and Algorithm 6), in particular Algorithm 5, is close
to Spacer [Komuravelli et al. 2015, 2014, 2016]. The correspondence is discussed in Section 5 at
the intuitive level. A more formal argument may be possible by deriving a transition system for
Algorithm 5, but we omit the details by the space limitation.
Our procedure (Algorithm 5) still differs from existing implementations of Spacer in many
respects. First, our procedure only captures the “skeleton” of Spacer and lacks various optimizationsof practical significance. This point will be discussed in Section 5.3. Second, our procedure is
1 They only showed that there exists a model-based projection procedure with which Spacer is not refutationally complete.

An implementation of Spacer employs a particular model-based projection procedure, and the current implementation ofSpacer may be refutationally complete due to a still unrevealed property of the model-based projection procedure employedby the current implementation.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:3

refutationally complete, but Spacer is not. The refutational completeness proof of Spacer requires
quite subtle arguments: in our setting, the keys are (1) the loop invariance of the arguments ofthe model-based projection and (2) the finiteness of the variety of possible return values.2 We
discuss the refutational (in)completeness of the original Spacer [Komuravelli et al. 2014, 2016] anda variant [Komuravelli et al. 2015] from our inductive perspective.
Contributions. The contributions of this paper can be summarized as follows.
• This paper provides a novel description of Spacer-like procedures based on structural induction. A refutationally complete variant of Spacer can be obtained as a modification of a naïve
procedure based on quantifier elimination. Interestingly, our procedure unifies Spacer and
GPDR [Hoder et al. 2011] (Remark 16).
• We discuss the completeness of Spacer implementations in the literature from the viewpointof our inductive description. Our inductive approach clarifies the subtleties of completenessof Spacer, which even experts have overlooked for a decade.
• We discuss optimizations to fill the gaps between our theoretical development and Spacer.
• We give an implementation of proposed procedures and empirically evaluate solvers using
CHC-comp benchmarks. In particular, we discuss the practical significance of tricks to retain
refutational completeness.
2 PRELIMINARIESThis section defines the CHC satisfiability problem and introduces the notion of model-based
projection, a key technique for refutationally complete CHC solving.
2.1

Constraint Language and Constrained Horn Clauses

We assume a first-order signature 𝜎 and a structure S of the signature 𝜎, fixed in the sequel. Let L
be a fragment of first-order logic (over the signature 𝜎), called the constraint language. We shallstudy logical formulas with predicate variables, but formulas in L are assumed to have no predicate
variables. As usual, we assume L consists of quantifier-free formulas.
The language L admits quantifier elimination if for every 𝜑 (𝑥,® 𝑦)® ∈ L with free variables 𝑥® and𝑦,® one can effectively construct a formula 𝜓 (𝑦)® ∈ L such that S |= 𝜓 ⇔ ∃®
𝑥 .𝜑. We assume that theconstraint language L is closed under boolean operations and admits quantifier elimination.
For formulas 𝜑 (𝑥,® 𝑦)® and 𝜓 (𝑥,® 𝑧®) such that |= 𝜑 ⇒ 𝜓 , an interpolation is a formula 𝜗 (𝑥)® such that(1) the free variables {𝑥®} of 𝜗 are free variables of both 𝜑 and 𝜓 and (2) |= 𝜑 ⇒ 𝜗 and |= 𝜗 ⇒ 𝜓 .
We assume a procedure Itp(𝜑,𝜓 ) that returns an interpolation of 𝜑 and 𝜓 .
A constrained Horn clause (or CHC) is a formula of one of the following forms∀®
𝑥.

𝑃1 (𝑡®1 ) ∧ · · · ∧ 𝑃𝑛 (𝑡®𝑛 ) ∧ 𝜑 =⇒ 𝑄 (®
𝑠)

∀®
𝑥.

𝑃 1 (𝑡®1 ) ∧ · · · ∧ 𝑃𝑛 (𝑡®𝑛 ) ∧ 𝜑 =⇒ ⊥,where 𝑥® is the sequence of object variables appearing in the formula, 𝑡®1, . . . , 𝑡®𝑛 and 𝑠® are sequencesof terms, 𝜑 is a formula in the constraint language, and 𝑃1, . . . , 𝑃𝑛 and 𝑄 are predicate variables.
The position of 𝑄 is called the head position. We often omit the quantifiers and just write as
𝑃1 (𝑡®1 ) ∧ · · · ∧ 𝑃𝑛 (𝑡®𝑛 ) ∧ 𝜑 =⇒ 𝑄 (®
𝑠 ) and 𝑃1 (𝑡®1 ) ∧ · · · ∧ 𝑃𝑛 (𝑡®𝑛 ) ∧ 𝜑 =⇒ ⊥.
A CHC system is a finite set of CHCs, regarded as their conjunction. A solution of a CHC system
is an interpretation of predicate variables that makes all formulas in the system true. For a solution
𝜉, we write 𝜉 (𝑃) for the interpretation of 𝑃 under 𝜉. The solutions are naturally ordered: 𝜉 ≤ 𝜁 if
and only if ∀®
𝑥 .𝜉 (𝑃)(𝑥)® =⇒ 𝜁 (𝑃)(𝑥)® for every predicate variable 𝑃. The problem of deciding if agiven CHC system has a solution is called the CHC satisfiability problem.
2 These points have already been presented in the (wrong) proof of the termination of Spacer [Komuravelli et al. 2016]. The

flaw was that an argument of model-based projection was, in fact, not a loop invariant (in terms of our framework).
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:4

Takeshi Tsukada and Hiroshi Unno

Under a mild condition on L and S, a given CHC system can be effectively transformed into

𝜄 (𝑥,
® 𝑦)
® =⇒ 𝑃 (𝑥),®
𝑃 (𝑥)® ∧ 𝑃 (𝑦)® ∧ 𝜏 (𝑥,® 𝑦,® 𝑧®, 𝑢)® =⇒ 𝑃 (®
𝑧 ),
𝑃 (𝑥)
® ∧ 𝛽 (𝑥,® 𝑦)® =⇒ ⊥ ,where 𝜄, 𝜏, 𝛽 ∈ L, without changing the satisfiability of CHC systems. We shall often refer 𝜄, 𝜏, 𝛽 as
the inital states, transition relation and bad states. For the above CHC system, 𝛼 (𝑥)® := ¬∃®
𝑦.𝛽 (𝑥,® 𝑦)®
is called the assertion in this paper.
2.2 Model Based Projection
Model-based projection [Komuravelli et al. 2014, 2016] is a way to handle quantified formulas. It isclosely related to quantifier elimination, which asks to find a formula 𝜓 (𝑦)® equivalent to a given
existentially quantified formula ∃®
𝑥 .𝜑 (𝑥,® 𝑦)® (where 𝜑 (𝑥,® 𝑦)® ∈ L). Model-based projection is, in asense, a partial calculation of quantifier elimination.
Definition 1 (Model-based projection [Komuravelli et al. 2014, 2016]). Let 𝜑 (𝑥,® 𝑦)® be a quantifierfree formula with free variables 𝑥,® 𝑦.
® A function Mbp( 𝑥®.𝜑 (𝑥,® 𝑦),® −) from models M |= 𝜑 of 𝜑 to aquantifier-free formula 𝜓 M (𝑦)® := Mbp( 𝑥®.𝜑 (𝑥,® 𝑦),® M) over {𝑦}® is a model-based projection (of 𝜑w.r.t. 𝑥)® if it satisfies, for every M |= 𝜑,EE|= 𝜓 M (𝑦)® ⇒ ∃®
𝑥 .𝜑 (𝑥,® 𝑦)®

M |= 𝜓 M (𝑦),®

andand furthermore it satisfies the image finiteness, i.e. {Mbp( 𝑥®.𝜑, M) | M |= 𝜑 } is a finite set.

□E

A model-based projection can be performed linear in time and space for certain theories [Komuravelli et al. 2014, 2016] such as linear real arithmetic (LRA) and linear integer arithmetic (LIA).
Hereafter we assume that a model-based projection Mbp( 𝑥®.𝜑, −) exists for every 𝜑 ∈ L and 𝑥®
and that the mapping (𝜑, 𝑥,® M) ↦→ Mbp( 𝑥®.𝜑, M) is computable (where M |= 𝜑).
E

E

Example 2. Consider the theory of real arithmetic and let 𝜑 (𝑏, 𝑥) := (𝑥 2 + 𝑏𝑥 + 1 = 0). Then(∃𝑥 .𝜑 (𝑏, 𝑥)) ⇔ (𝑏 2 − 4 ≥ 0) ⇔ (𝑏 ≤ −2 ∨ 2 ≤ 𝑏) ⇔ (𝑏 ≤ −2 ∨ (2 ≤ 𝑏 ≤ 7) ∨ 3 ≤ 𝑏). So the map𝜓 ′ if M (𝑏) < 0𝜓 1′ (𝑏) := (𝑏 ≤ −2)

 1

′
M ↦→ 𝜓 2 if 0 ≤ M (𝑏) < 4
where 𝜓 2′ (𝑏) := (2 ≤ 𝑏 ≤ 7)′
𝜓 3′ (𝑏) := (3 ≤ 𝑏).
𝜓 if 4 ≤ M (𝑏) 3
is a model-based projection Mbp( 𝑥 .𝜑 (𝑏, 𝑥), −) for 𝜑 (note that −2 < M (𝑏) < 2 is impossible since
M |= 𝜑). Of course, this is not a unique choice: one can provide a model-based projection based on(∃𝑥 .𝜑 (𝑏, 𝑥)) ⇔ (𝑏 ≤ −2 ∨ 2 ≤ 𝑏) (yielding 𝑏 ≤ −2 or 2 ≤ 𝑏 depending on the input model) or on(∃𝑥 .𝜑 (𝑏, 𝑥)) ⇔ (𝑏 2 − 4 ≥ 0) (yielding 𝑏 2 − 4 ≥ 0 independent of the input model).
□E

Example 3. Assume that L admits quantifier elimination. Then, the following procedure provides
a model-based projection. Given a formula 𝜑 (𝑥,® 𝑦)® and variables 𝑥,® the procedure first performsÔ
quantifier elimination for ∃®
𝑥 .𝜑 (𝑥,® 𝑦),® yielding 𝜓 (𝑦)® = 𝑛𝑖=1 𝜓𝑖 (𝑦).
® Then, given a model M |= 𝜑, theprocedure chooses 𝑖 such that M |= 𝜓𝑖 and returns 𝜓𝑖 .3 However, this procedure is inefficient, andthe procedures by Komuravelli et al. [2014, 2016] do not invoke quantifier elimination.
□
There are many ways of understanding what a model-based projection does: (a) It computes anunder-approximation of ∃®
𝑥 .𝜑, guided by a model M |= 𝜑; (b) It is a lazy quantifier-elimination; (c) It® in the denotation of ∃®
𝑥 .𝜑. The viewpoints (a) and (b) can
compute a generalization of a point M (𝑦)be found in the Spacer paper [Komuravelli et al. 2014, 2016], and (c) will be discussed in Remark 16
comparing Spacer with GPDR [Hoder and Bjørner 2012].
3 There is also a simpler model-based projection procedure that returns 𝜓 independent of the input model M. However, theintuition of the model-based projection is closer to choosing a disjunct from the formula obtained by quantifier elimination.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:5

Algorithm 1 Quantifier elimination by model-based projection
1: function Qe(𝜑 (𝑥,® 𝑦),® {𝑥®})2:𝜓 (𝑦)® := ⊥
3:
while ∃M. M |= 𝜑 (𝑥,® 𝑦)® ∧ ¬𝜓 (𝑦)
® do
4:
𝜗 (𝑦)
® := Mbp( 𝑥®.𝜑, M)
5:
𝜓 := 𝜓 ∨ 𝜗E

6:return 𝜓Here, we explain the perspective (b). This is essentially explained in Example 3: a model-based projection procedure produces a disjunct of the formula obtained by quantifier elimination. Conversely,a model-based projection procedure provides a quantifier elimination procedure (cf. Algorithm 1).
The formula 𝜓 (𝑦)® records the current under-approximation of ∃®
𝑥 .𝜑. Line 3 checks if the current
approximation is exhaustive, and if not, a new under-appoximation 𝜗 is computed and added(lines 4 and 5). The procedure terminates because {𝜗 | M |= 𝜑 and 𝜗 = Mbp( 𝑥®.𝜑, M)} is a finite
set and the same 𝜗 does not appear twice in the computation.
It is worth noting that the use of model-based projection in Algorithm 1 is far from typical.
® 𝑦),® M) generates a formula 𝜗 (𝑦),® which is a part of theModel-based projection Mbp( 𝑥®.𝜑 (𝑥,formula 𝜓 obtained by quantifier elimination, i.e. 𝜓 (𝑦)® = 𝜗 (𝑦)® ∨ · · · with an unknown part · · ·. The
unknown part · · · can be obtained by further calling Mbp with different models as in Algorithm 1,
but typically, one suspends the calculation of · · · and infers of consequences of the fact that 𝜃 is𝑥 .𝜑. The calculation of the · · · part will be resumed if necessary or
an under-approximation of ∃®
discarded (and we would be in trouble if a discarded part was actually necessary).
EE

3 A BASIC STRATEGY AND PROCEDURES FOR CHC SOLVING
This section briefly reviews a common strategy to solve CHCs based on finite approximations of
CHCs and tree interpolation. This is a fairly common strategy used in GPDR [Hoder and Bjørner
2012], Spacer [Komuravelli et al. 2015, 2014, 2016] and a procedure proposed by Unno and Kobayashi[2009] among others. Our procedures also follow this strategy.
For simplicity, let us focus on the following non-linear CHC system
𝑆 = { 𝜄 (𝑥) ⇒ 𝑃 (𝑥),𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ⇒ 𝑃 (𝑧),𝑃 (𝑧) ⇒ 𝛼 (𝑧) }(1)which has a single predicate variable 𝑃 and a unique non-linear clause 𝑃 (𝑥)∧𝑃 (𝑦)∧𝜏 (𝑥, 𝑦, 𝑧) ⇒ 𝑃 (𝑧)with two occurrences of the predicate variable on the left-hand-side of ⇒.
3.1

Finite Approximation and Tree Interpolation

This subsection presents an approach to CHC solving based on finite approximations, which isanalogous to bounded model-checking in program verification. Let us first explain the idea in terms
of program verification, which we believe is more intuitive.
We consider the safety verification problem for transition systems. Formally, a transition system
is a quadruple X = (𝑋, 𝐼, 𝑅, 𝐴) where 𝑋 is the set of states, 𝐼 ⊆ 𝑋 is the inital states, 𝑅 ⊆ 𝑋 × 𝑋 isthe transition relation and 𝐴 ⊆ 𝑋 is the assertion that we expect to hold for all reachable states. A
state 𝑥 ∈ 𝑋 is reachable if there exists a sequence 𝑥 0, 𝑥 1, . . . , 𝑥𝑘 of states 𝑥𝑖 ∈ 𝐷 such that 𝑥 0 ∈ 𝐼 ,𝑥𝑘 = 𝑥 and (𝑥𝑖 , 𝑥𝑖+1 ) ∈ 𝑅 for every 𝑖 < 𝑘. A state 𝑥 ∈ 𝑋 is a bad state if 𝑥 ∉ 𝐴, and the transition
system X is safe if no bad state is reachable. The safety checking is undecidable in general due tothe unboundedness of the lengths of transitions. However, if the length of transitions is bounded,
the problem becomes decidable. That means, for every 𝑘 ∈ N, whether there exists a bad statereachable within 𝑘 steps is decidable (provided that 𝐼 , 𝑅 and 𝐴 are definable in L). A classic idea in
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:6

Takeshi Tsukada and Hiroshi Unno

verification [McMillan 2003] is to solve bounded problems by gradually increasing the bound 𝑘 andto use the solutions for bounded problems as a hint to solve the unbounded problem.
Example 4. The transition system X = (Z, {𝑥 | 2 ≤ 𝑥 ≤ 8}, {(𝑥, 2𝑥 − 3) | 𝑥 ∈ Z}, {𝑥 | 𝑥 ≥ −5})is unsafe. This system is safe within 𝑘 steps for 𝑘 ≤ 3 and unsafe within 𝑘 steps for 𝑘 > 3. The
bounded unsafety of X (for 𝑘 > 3) shows the (undounded) unsafety of X.
□
Example 5. The transition system X ′ = (Z, {𝑥 | 2 ≤ 𝑥 ≤ 8}, {(𝑥, 2𝑥) | 𝑥 ∈ Z}, {𝑥 | 𝑥 ≥ −5}) issafe (and safe within 𝑘 steps for every 𝑘). The safety of X ′ within 5 steps can be witnessed by an
overapproximation of the set of states reachable within 5 steps, such as {𝑥 | 2 ≤ 𝑥 ≤ 256} and{𝑥 | 0 ≤ 𝑥 }. The latter is closed under the transition, so it shows the unbounded safety of X ′. □The CHC systems corresponding to safety verification of transition systems are of the form
𝐿 = { 𝜄 (𝑥) ⇒ 𝑃 (𝑥),𝑃 (𝑥) ∧ 𝜏 (𝑥, 𝑦) ⇒ 𝑃 (𝑦),𝑃 (𝑥) ⇒ 𝛼 (𝑥) }.

(2)

The satisfiability of 𝐿 in Equation (2) is equivalent to the safety of X = (𝐷, 𝐼, 𝑅, 𝐴) where 𝐷 is therange of the variables 𝑥 and 𝑦, 𝐼 = { 𝑑 ∈ 𝐷 | |= 𝜄 (𝑑) }, 𝑅 = { (𝑑, 𝑑 ′) ∈ 𝐷 × 𝐷 | |= 𝜏 (𝑑, 𝑑 ′) } and𝐴 = { 𝑑 ∈ 𝐷 | |= 𝛼 (𝑑) }. The bounded version also has a CHC representation. For example, theCHC system 𝐿 (2) corresponding to the bounded version with 𝑘 = 2 is given by
𝑃2 (𝑥) ∧ 𝜏 (𝑥, 𝑦) ⇒ 𝑃1 (𝑦),𝑃1 (𝑥) ∧ 𝜏 (𝑥, 𝑦) ⇒ 𝑃 0 (𝑦),

𝜄 (𝑥) ⇒ 𝑃2 (𝑥),

𝜄 (𝑥) ⇒ 𝑃 1 (𝑥),

𝜄 (𝑥) ⇒ 𝑃 0 (𝑥),𝑃 2 (𝑥) ⇒ 𝛼 (𝑥),𝑃 1 (𝑥) ⇒ 𝛼 (𝑥),𝑃 0 (𝑥) ⇒ 𝛼 (𝑥).

(3)

The first and second lines require that 𝑃 2 to be an overapproximation of initial states, 𝑃 1 to be an
overapproximation of states reachable by 0 or 1 step, and 𝑃 0 to be an overapproximation of states
reachable within 2 steps. The third line requires that 𝑃2 , 𝑃1 and 𝑃 0 contain no bad state. For general𝑘 ∈ N, the CHC system 𝐿 (𝑘) is the set of constraints over predicate variables 𝑃𝑘 , . . . , 𝑃 0 given by
𝐿 (𝑘) = { 𝑃𝑖+1 (𝑥) ∧ 𝜏 (𝑥, 𝑦) ⇒ 𝑃𝑖 (𝑦) | 0 ≤ 𝑖 < 𝑘 } ∪ { 𝜄 (𝑥) ⇒ 𝑃𝑖 (𝑥), 𝑃𝑖 (𝑥) ⇒ 𝛼 (𝑥) | 0 ≤ 𝑖 ≤ 𝑘 }.
The CHC system 𝐿 (𝑘) , which we call the 𝑘-th approximation of 𝐿, has some remarkable properties.
The most notable property is the decidability of satisfiability, coming from the acyclicity of thedependencies between predicate variables. The dependency graph of a CHC system has predicate
variables as nodes, and it has an edge from 𝑃 to 𝑄 if the system has a CHC of the form (· · · ∧ 𝑄 ∧· · · ) ⇒ 𝑃. For example, the dependency graphs of 𝐿 and of 𝐿 (𝑘) are𝑃 ee

and 𝑃0 → 𝑃 1 → · · · → 𝑃𝑘 ,respectively. Intuitively, the infinite path in the former graph causes the unboundedness of transitions, and the length of the longest path in the latter is the bound 𝑘.4 The acyclicity allows us toconstruct a solution by induction, going from leaf to root (see Sections 4.1 and 4.2). A solution 𝜁 of
𝐿 (𝑘) may provide a solution of 𝐿. So, we can apply the same strategy as in verification: it solves 𝐿 (𝑘)with increasing 𝑘, expecting that solutions of approximations help to solve the original problem 𝐿.
Example 6. The CHC system 𝐿 ′ corresponding to X ′ in Example 5 consists of 2 ≤ 𝑥 ≤ 8 ⇒ 𝑃 (𝑥),𝑃 (𝑥) ⇒ 𝑃 (2𝑥) and 𝑃 (𝑥) ⇒ 𝑥 ≥ −5. Then 𝐿 ′ (5) is{ 𝑃𝑖+1 (𝑥) ⇒ 𝑃𝑖 (2𝑥) | 0 ≤ 𝑖 < 5 } ∪ { 2 ≤ 𝑥 ≤ 8 ⇒ 𝑃𝑖 (𝑥), 𝑃𝑖 (𝑥) ⇒ 𝑥 ≥ −5 | 0 ≤ 𝑖 ≤ 5 },and a solution 𝜉 is 𝜉 (𝑃5 )(𝑥) = (0 ≤ 𝑥 ≤ 10), 𝜉 (𝑃 4 )(𝑥) = (0 ≤ 𝑥 ≤ 100), 𝜉 (𝑃 3 )(𝑥) = (0 ≤ 𝑥 ≤ 1000),𝜉 (𝑃2 )(𝑥) = (0 ≤ 𝑥 ≤ 10000) and 𝜉 (𝑃1 ) = 𝜉 (𝑃0 ) = (0 ≤ 𝑥). In this case, 𝜑 (𝑥) := 𝜉 (𝑃 0 )(𝑥) is asolution of 𝐿.
□
4 However, the direction of the edges is opposite to the direction of the transition.

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:7

This strategy is applicable to 𝑆 in Equation (1) as well. The difference from 𝐿 in Equation (2)is that the rule 𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ⇒ 𝑃 (𝑧) has two occurrences of 𝑃 in the left-hand side of⇒. In order to precisely track the occurrences, an approximation of 𝑆 has predicate variables 𝑃 𝑤
indexed by words 𝑤 ∈ {𝐿, 𝑅}∗ over 𝐿 and 𝑅. We write 𝜖 for the empty word and |𝑤 | for the lengthof the word 𝑤 ∈ {𝐿, 𝑅}∗ . The 𝑘-th approximation of 𝑆, written 𝑆 (𝑘) , is a CHC system over predicate
variables {𝑃 𝑤 | 𝑤 ∈ {𝐿, 𝑅}∗, |𝑤 | ≤ 𝑘 } given by
𝑆 (𝑘)

:=

{ 𝑃 𝑤𝐿 (𝑥) ∧ 𝑃 𝑤𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ⇒ 𝑃 𝑤 (𝑧) | 𝑤 ∈ {𝐿, 𝑅}∗, |𝑤 | < 𝑘 }∪{ 𝜄 (𝑥) ⇒ 𝑃 𝑤 (𝑥), 𝑃 𝑤 (𝑥) ⇒ 𝛼 (𝑥) | 𝑤 ∈ {𝐿, 𝑅}∗, |𝑤 | ≤ 𝑘 }.

Similar to the above cases, a solution 𝜉 of an approximation 𝑆 (𝑘) can provide a solution of theoriginal problem 𝑆, for example, if 𝜉 (𝑃𝜖 ) = 𝜉 (𝑃𝐿 ) = 𝜉 (𝑃𝑅 ).5 So, our basic strategy is to solve
approximations 𝑆 (𝑘) with increasing 𝑘 and then to use solutions of 𝑆 (𝑘) to construct a solution of 𝑆.
The dependency graph of 𝑆 (𝑘) is a complete binary tree, namely,
44 𝑃𝐿

11 𝑃𝐿𝐿 · · ·-- 𝑃 · · ·𝑃𝑅

11 𝑃𝑅𝐿 · · ·-- 𝑃 · · ·
𝑅𝑅

𝑃𝜖
**

𝐿𝑅

A CHC system is called tree-like by Rümmer et al. [2014] if its dependency graph is a tree,6 and asolution of a tree-like CHC system coincides with a tree interpolant [Heizmann et al. 2010].7 In thisterminology, our strategy is to solve CHCs by iteratively computing tree interpolations.
3.2

Interpolation-Based CHC Solving

The basic strategy invokes subprocedures solving tree-like CHC systems 𝑆 (0) , 𝑆 (1) , . . .. These subproblems can be solved independently, but a more efficient approach exploits the similarity between
𝑆 (𝑘−1) and the subset of 𝑆 (𝑘) consisting of the constraints for {𝑃𝐿𝑤 | 𝑤 ∈ {𝐿, 𝑅}∗, |𝑤 | < 𝑘 }.
Suppose that we have solved 𝑆 (𝑘−1) , yielding a solution 𝜉. Let 𝜁 be an assignment to predicate
variables {𝑃 𝑤 | 𝑤 ∈ {𝐿, 𝑅}∗, |𝑤 | ≤ 𝑘 } for 𝑆 (𝑘) given by
𝜁 (𝑃𝜖 ) := ⊤and 𝜁 (𝑃 𝑤 ) := 𝜉 (𝑃 𝑣 )if 𝑤 = 𝐿𝑣 or 𝑤 = 𝑅𝑣.

The assignment 𝜁 is almost a solution of 𝑆 (𝑘) ; the assignment 𝜁 satsifies all constraints in 𝑆 (𝑘)except for 𝑃𝜖 (𝑥) ⇒ 𝛼 (𝑥). So, we do not need to find a solution of 𝑆 (𝑘) from scratch. It suffices toadjust the “almost-solution” 𝜁 so that 𝑃𝜖 (𝑥) ⇒ 𝛼 (𝑥) is satisfied.
Such “almost-solutions” are called traces in IC3/PDR [Bradley 2011] and their relatives (e.g. [Hoderand Bjørner 2012]). Formally, a trace Φ for 𝑆 (𝑘) is an assignment to {𝑃 𝑤 | 𝑤 ∈ {𝐿, 𝑅}∗, |𝑤 | ≤ 𝑘 }satisfying 𝑆 (𝑘) \ {𝑃𝜖 ⇒ 𝛼 (𝑥)}. The value Φ(𝑃 𝑤 ) for 𝑃 𝑤 shall be written as Φ(𝑤) and 𝜑 𝑤 . The domain
dom(Φ) of the trace Φ of 𝑆 (𝑘) is {𝑤 ∈ {𝐿, 𝑅}∗ | |𝑤 | ≤ 𝑘 }. For 𝑤 ∈ dom(Φ), the subtrace Φ𝑤 is a
trace of 𝑆 (𝑘− |𝑤 |) defined by Φ𝑤 (𝑣) := Φ(𝑤𝑣). The immediate subtraces Φ𝐿 and Φ𝑅 often appear in
the description of algorithms. For traces Φ and Φ′ of 𝑆 (𝑘−1) such that 𝜑𝜖 ⇒ 𝛼 and 𝜑𝜖′ ⇒ 𝛼, we write(⊤, Φ, Φ′) for the trace Ψ of 𝑆 (𝑘) such that Ψ(𝜖) = ⊤, Ψ𝐿 = Φ and Ψ𝑅 = Φ′.
Recall that it suffices for solving 𝑆 (𝑘) to adjust a trace Φ so that 𝑃𝜖 ⇒ 𝛼 is satisfied. The main
problem addressed in this paper is a slight generalization, which we call refinement problem:
Given a trace Φ of 𝑆 (𝑘) and an assertion ¬𝛽, find a trace Φ′ of 𝑆 (𝑘) that satisfies
𝜑𝜖′ (𝑥) ⇒ ¬𝛽 (𝑥) and 𝜑 𝑤′ (𝑥) ⇒ 𝜑 𝑤 (𝑥) (for every 𝑤 ∈ dom(Φ)).
5 A weaker condition suffices. See the next subsection.
6 Strictly speaking, the class of tree-like CHCs in this sense is slightly wider than the original (for the simplicity ofpresentation). An approximation 𝑆 (𝑘 ) is tree-like in the sense of Rümmer et al. [2014] as well.
7 Heizmann et al. [2010] called this notion nested interpolant.

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:8

Takeshi Tsukada and Hiroshi Unno

Algorithm 2 CHC solving by using a refinement procedure
1: function CHCSolve(𝜄, 𝜏, 𝛼)2:
Φ = (); 𝑛 := 03:while true do4:
Φ := (⊤, Φ, Φ); 𝑛 := 𝑛 + 1
5:
𝑅 ∈ Refine(Φ, 𝛼; 𝜄, 𝜏)
6:
7:
8:
9:
10:
11:

if 𝑅 = None thenreturn UNSATΦ := 𝑅for 𝑖 := 0, . Ó. . , 𝑛 −Ó1 do
Ó
if |= ∀𝑥 . Ó𝑗 ≤𝑖 Ó
|𝑤 |=𝑗 𝜑 𝑤 (𝑥) ⇒|𝑣 |=𝑖+1 𝜑 𝑣 (𝑥) thenreturn 𝑗 ≤𝑖 |𝑤 |=𝑗 𝜑 𝑤 (𝑥)A trace that satisfies the above condition is called a refinement of Φ w.r.t. ¬𝛽 (borrowing theterminology of [McMillan 2006]). Let Refine(Φ, ¬𝛽; 𝜄, 𝜏) (or more simply Refine(Φ, ¬𝛽) when 𝜄 and𝜏 are clear from the context) be the set of refinements (or symbol None if there is no refinement):
Refine(Φ, ¬𝛽) := { Φ′ | Φ′ is a refinement of Φ w.r.t. ¬𝛽 }∪ { None | there is no refinement of Φ w.r.t. ¬𝛽 }.
The refinement problem itself is a tree interpolation problem, so it is computable. The main interestof this paper is an efficient refinement procedure.
Once a refinement procedure is given, a procedure for the CHC satisfiability can be given by
Algorithm 2. Starting from the trivial trace Φ = (), the procedure iterates the following process.
(1) Line 4 extends the trace by adding a new root ⊤.
(2) Lines 5–7 refine the trace Φ with respect to 𝛼 (i.e. performing the bounded model-checking).
If an error is found (i.e. if 𝑅 = None), then the CHC system is unsatisfiable.
(3) Line 8 updates the trace Φ.
(4) Lines 9–11 try to extract an invariant from the current trace.
Theorem 7. Algorithm 2 is sound. That is, if it returns UNSAT, then the CHC system 𝑆 in Equation (1)is unsatisfiable, and if it returns a formula, then it is a solution of the CHC system. It is refutationallycomplete if Line 5 always terminates.
Remark 8. Here, we note some differences from the standard setting. First, a trace in our setting
has the tree structure (i.e. a branching structure) instead of the linear structure. To get a trace
depending only on the depth, simply take the conjunction of all the nodes at that depth. Second, inthe standard setting, a trace is monotone (i.e. 𝜑 𝑤𝐿 ⇒ 𝜑 𝑤 and 𝜑 𝑤𝑅 ⇒ 𝜑 𝑤 in our notation), whereas
we do not require monotonicity. Third, the root in our setting is the deepest part in the standard
setting. Hence the condition in line 9 (Algorithm 2) is usually written as O𝑛−𝑖 ⇒ O𝑛−𝑖−1 in thestandard setting, where O𝑚 is the component of the trace O at depth 𝑚.
□
3.3

SpacerSpacer [Komuravelli et al. 2015, 2014, 2016] is a well-known and highly efficient procedure for CHC
solving. This paper aims to give an inductive description of Spacer to make it easier to reason about
and develop its variant. Here, we briefly review the procedure using the traditional description
based on abstract transition systems. The details of Spacer vary slightly in the literature, and thediscussion here is based on Komuravelli et al. [2015].
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:9(Candidate) [|= 𝜓 (𝑧) ⇒ (𝜑 0 (𝑧) ∧ ¬𝛼 (𝑧))]Q := Q ∪ {(𝜓, 0)}(DecideMust) (𝜓, 𝑛) ∈ Q
M |= 𝜑𝑛+1 (𝑥) ∧ U (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧)let 𝜗 (𝑥) = Mbp( 𝑦𝑧.𝜑𝑛+1 (𝑥) ∧ U (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧), M) in
Q := Q ∪ {(𝜗, 𝑛 + 1)}
(DecideMay) (𝜓, 𝑛) ∈ Q
M |= 𝜑𝑛+1 (𝑥) ∧ 𝜑𝑛+1 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧)let 𝜗 (𝑦) = Mbp( 𝑥𝑧.𝜑𝑛+1 (𝑥) ∧ 𝜑𝑛+1 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧), M) in
Q := Q ∪ {(𝜗, 𝑛 + 1)}(Conflict) (𝜓, 𝑛) ∈ Q|= 𝜑𝑛+1 (𝑥) ∧ 𝜑𝑛+1 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ⇒ ¬𝜓 (𝑧)let 𝜗 (𝑧) = Itp(𝜑𝑛+1 (𝑥) ∧ 𝜑𝑛+1 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧), ¬𝜓 (𝑧)) in𝜑𝑖 (𝑧) := 𝜑𝑖 (𝑧) ∧ 𝜗 (𝑧) for 𝑖 ≥ 𝑛
EE(Leaf) [(𝜓, 𝑛) ∈ Q, |= 𝜑𝑛+1 (𝑥) ∧ 𝜑𝑛+1 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ⇒ ¬𝜓 (𝑧)]Q := Q ∪ {(𝜓, 𝑛 + 1)}(Successor) (𝜓, 𝑛) ∈ Q
M |= U (𝑥) ∧ U (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧)let 𝛾 (𝑧) = Mbp( 𝑥𝑦.U (𝑥) ∧ U (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧), M) in
U := U ∨ 𝛾(Induction) 𝜑𝑛 = (· · · ∧ (𝜓 ∨ 𝜓 ′) ∧ · · · )|= (𝜑𝑛 (𝑥) ∧ 𝜓 (𝑥)) ∧ (𝜑𝑛 (𝑦) ∧ 𝜓 (𝑥)) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ⇒ 𝜓 (𝑧)𝜑𝑖 := 𝜑𝑖 ∧ 𝜓 for 𝑖 = 𝑛 − 1, 𝑛, 𝑛 + 1, . . . , 𝑁
E(Unfold) [|= 𝜑𝜖 (𝑧) ⇒ 𝛼 (𝑧)]𝜑𝑛+1 := 𝜑𝑛 for 𝑛 = 𝑁 , 𝑁 − 1, . . . , 0
𝜑 0 := ⊤, 𝑁 := 𝑁 + 1
Fig. 1. Transtion rules for Spacer [Komuravelli et al. 2015, 2014, 2016]. The rules (Safe) and (Unsafe) in theoriginal system, which perform output, are not regarded as transition rules in our formalism.

A state is a tuple (𝑁 , Φ, Q, U). We explain the meaning of each component.
• 𝑁 is the depth of the current approximation.
• Φ = (𝜑𝑛 )0≤𝑛 ≤𝑁 is a trace with the linear structure. The trace must be monotone, i.e. 𝜑𝑛+1 (𝑧) ⇒𝜑𝑛 (𝑧) for every 𝑛.
• Q is a collection of pairs (𝜓, 𝑖) of a formula 𝜓 and 0 ≤ 𝑖 ≤ 𝑁 . A pair (𝜓, 𝑖) is called a queryand expresses a request to strengthen 𝜑𝑖 so that |= 𝜑𝑖 (𝑧) ⇒ ¬𝜓 (𝑧).
• U ⊆ S is an under-approximation of the minimum solution of {𝜄 (𝑥) =⇒ 𝑃 (𝑥), 𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧𝜏 (𝑥, 𝑦, 𝑧) =⇒ 𝑃 (𝑧)}. Hence, if 𝛾 intersects with ¬𝛼, the CHC system is unsatisfiable.
What is new about Spacer compared to its predecessors such as [Bradley 2011; Een et al. 2011] and
GPDR [Hoder and Bjørner 2012] is that it also manages under-approximations.
The initial state is (0, Φ0, ∅, ∅) where Φ0 consists only of the root 𝜑 0 = ⊤. The procedure willterminate with SAT (resp. UNSAT) when the transition system reaches a state where |= 𝜑𝑛 (𝑧) ⇒𝜑𝑛+1 (𝑧) for some 𝑛 (resp. where U ∧ ¬𝛼 ≠ ∅).
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:10

Takeshi Tsukada and Hiroshi Unno

The transition rules are shown in fig. 1. Each rule can be invoked only if all conditions in [· · · ]are satisfied. The rule (Unfold) corresponds to Line 4 of Algorithm 2 and other rules compute arefinement. The rules (Candidate), (DecideMay), (DecideMust) and (Leaf) are for query generation. (Candidate) requires that ¬𝜑 0 (𝑐) for a bad state 𝑐. (DecideMay) and (DecideMust) generate
a query for level 𝑛 + 1 from a query for level 𝑛: (DecideMay) generates a sufficient conditionand (DecideMust) generates a necessarily condition to resolve the query for level 𝑛. Note that
(DecideMust) utilizes the under-approximation U to generate a query that is a necessary condition
for (𝜓, 𝑛). The rule (Leaf) propagates a query that has been successfully resolved to the adjacentlevel. The rule (Conflict) resolves a query by strengthening 𝜑𝑛 . If a query (𝜓, 𝑛) is found to be
unresolvable, (Successor) produces an under-approximation, which witnesses that the query isunresolvable. The rule (Induction) strengthens the trace by conjoining a subformula in the trace.
This rule is heuristics to improve the efficiency.
Variation and refutational completeness. The transition system in fig. 1 comes from Komuravelli et al. [2015] and differs from the original procedure [Komuravelli et al. 2014, 2016] in somedetails.8 Here, we summarize the variants and the status of their refutational completeness.
Spacer is parameterized by two procedures: an interpolating theorem prover and a modelbased projection. Refutational completeness depends on the choices of background theory andthese procedures,9 and Komuravelli et al. [2016] claimed refutational completeness independentof the choice of these procedures. So, we focus on refutational completeness independent of the
choice of subprocedures. As mentioned in Section 1, Tsukada and Unno [2022, Section 6.6] gave acounterexample (for details, see Appendix C in the arXiv version [Tsukada and Unno 2021]).
Theorem 9 (Tsukada and Unno [2022]). The procedure described in Komuravelli et al. [2016] diverges
on a CHC system over linear integer arithmetic, for a specific choice of an interpolating theorem proverand a model-based projection. So, the refutational completeness independent of subprocedures fails.
There is a further subtlety. The transition system in fig. 1 coming from Komuravelli et al. [2015]
differs from the original procedure [Komuravelli et al. 2014, 2016]: (1) the original procedure
manages the under-approximation U by level, so U = (U𝑖 )0≤𝑖 ≤𝑁 ; and (2) the argument formulasfor Mbp are different. For example, in (Successor) in the original procedure, the argument formula
is U𝑛 (𝑥) ∧ U𝑛 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧), which does not involve the query 𝜓 . Despite these differences, thecounterexample in Theorem 9 also applies to Komuravelli et al. [2015]. Rather, these changes madeby Komuravelli et al. [2015] introduce two additional sources of incompleteness (cf. Section 5).
The implementation of Spacer10 is based on the description in Komuravelli et al. [2015] but
has some differences. The biggest difference is that the transition system in fig. 1 does not specify
the order of rules to apply, whereas the implementation adopts a specific order. The counterexample in Theorem 9 also applies to the implementation since the order of rule applications in theimplementation coincides with that is adopted in Tsukada and Unno [2021, Appendix C].
These incompleteness issues have been overlooked even by experts, and our inductive approachclarifies this issue so that non-specialists can easily understand it.
4 INDUCTIVE APPROACH TO REFINEMENT
This section develops a refinement procedure defined by induction. The inductive structure that
we exploit is the tree structure of an approximation of the input CHC system.
8 We choose Komuravelli et al. [2015] because it seems to serve as a basis for the implementation and subsequent studies

such as Krishnan et al. [2020]. Furthermore, two of the three authors of the original paper [Komuravelli et al. 2014, 2016]
are also authors of Komuravelli et al. [2015]. These facts justify our choice.
9 For example, it is refutationally complete if quantifier elimination is used as model-based projection.
10 See https://github.com/Z3Prover/z3. The code related to Spacer is in the directory src/muz/spacer.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:11This section starts by clarifying the problem that we should solve by induction. Just as proof
by induction often requires proving a stronger proposition than the one you wish to show, solving a problem by induction sometimes requires solving a more general problem. We propose ageneralization of the refinement problem suitable for induction.
The generalized problem has a naïve inductive solver using quantifier elimination (or equivalently,
manipulation of quantified formulas). We will then modify this solver. The idea is to replace thequantifier elimination procedure with Algorithm 1, which iteratively applies the model-based
projection procedure Mbp, and then to make calls to Mbp as lazy as possible, while keeping theinductive structure of the solver unchanged. The idea of making quantifier elimination lazy can befound in the original Spacer paper [Komuravelli et al. 2016], but this section differs in that we do
not change the inductive structure nor properties of the procedure.
4.1 Generalizing the Refinement Problem
This subsection explains a difficulty in inductively solving the non-linear CHC refinement problem
and proposes a generalization appropriate for an inductive solver.
For the subclass of CHC systems known as linear CHC systems, one can easily provide an
inductive refinement procedure. A CHC 𝑃1 (𝑥 1 ) ∧ · · · ∧ 𝑃𝑛 (𝑥𝑛 ) ∧ 𝜏 (𝑥,® 𝑦) ⇒ 𝑄 (𝑦) is linear if 𝑛 ≤ 1.
For example, consider a linear CHC system𝜄 (𝑥) =⇒ 𝑃 (𝑥),𝑃 (𝑥) ∧ 𝜏 (𝑥, 𝑦) =⇒ 𝑃 (𝑦),𝑃 (𝑥) =⇒ 𝛼 (𝑥)and a trace Φ = (𝜑𝑘 , . . . , 𝜑 1, 𝜑 0 ) (so 𝜑𝑖+1 (𝑥) ∧𝜏 (𝑥, 𝑦) ⇒ 𝜑𝑖 (𝑥) for 0 ≤ 𝑖 < 𝑘, 𝜄 (𝑥) ⇒ 𝜑𝑖 (𝑥) for 0 ≤ 𝑖 ≤𝑘, and 𝜑𝑖 (𝑥) ⇒ 𝛼 (𝑥) for 0 < 𝑖 ≤ 𝑘). The refinement problem asks to strengthen the trace Φ to satisfy
𝜑 0 (𝑥) ⇒ 𝛼 0 (𝑥) for a given property 𝛼 0 . It is easy to solve the refinement problem by induction: we
first refine the subtrace Φ1 = (𝜑𝑘 , . . . , 𝜑 1 ) against the assertion 𝛼 1 (𝑥) := ¬(∃𝑦.𝜏 (𝑥, 𝑦) ∧ ¬𝛼 0 (𝑦)),yielding Φ1′ = (𝜑𝑘′ , . . . , 𝜑 1′ ), and then find 𝜑 0′ that satisfies (𝜄 (𝑥) ∨ (𝜑 1′ (𝑥) ∧ 𝜏 (𝑥, 𝑦))) ⇒ 𝜑 0′ (𝑦) and𝜑 0′ (𝑥) ⇒ 𝛼 0 (𝑥) using an interpolating theorem prover. The assertion 𝛼 1 is canonical in the sensethat the refinement problem (Φ, 𝛼 0 ) has a solution if and only if (Φ1, 𝛼 1 ) has a refinement.
The difficulty of non-linear CHC solving is that there is no canonical choice of the assertion.
Example 10. Consider the CHC system(𝑥 = 3) =⇒ 𝑃 (𝑥), 𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ (𝑧 = |𝑥 − 𝑦|) =⇒ 𝑃 (𝑧),𝑃 (𝑧) ⇒ (𝑧 ≤ 5)

and a trace 𝜑𝐿 (𝑥) = 𝜑𝑅 (𝑥) = (𝑥 ≤ 5) and 𝜑𝜖 = ⊤ for its approximation of depth 1. An inductive
refinement procedure IndRefine needs to strengthen 𝜑𝐿 and/or 𝜑𝑅 so that𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ (𝑧 = |𝑥 − 𝑦|) =⇒ (𝑧 ≤ 5)
by invoking recursive calls IndRefine(𝜑𝐿 , 𝛼 𝐿 ) and/or IndRefine(𝜑𝑅 , 𝛼 𝑅 ) for appropriate 𝛼 𝐿 , 𝛼 𝑅 . So
the procedure should appropriately choose a direction 𝑑 ∈ {𝐿, 𝑅} and an assertion 𝛼𝑑 , but there isno canonical choice. A candidate is the pair (𝐿, 𝛼 𝐿 ) where𝛼𝐿:=¬∃𝑦𝑧.𝜑𝑅 (𝑦) ∧ (𝑧 = |𝑥 − 𝑦|) ∧ (𝑧 > 5),

which is sufficiently strong in the sense that if IndRefine(𝜑𝐿 , 𝛼 𝐿 ) succeeded, we would finish
the whole refinement procedure. However 𝛼 𝐿 is too strong so IndRefine(𝜑𝐿 , 𝛼 𝐿 ) fails. A similar
approach for 𝑑 = 𝑅 fails for the same reason.
□
The above example shows that a natural choice of an assertion for a recursive call may beunnecessarily strong. This observation motivates us to generalize the refinement problem so thatthe procedure performs best, even if no solution exists.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:12

Takeshi Tsukada and Hiroshi Unno

Definition 11. Let Φ be a trace and ¬𝛽 be an assertion. The counterexample 𝛾 for the refinement
problem (Φ, ¬𝛽) is defined by 𝛾 := min{ 𝛾 ′ | Refine(Φ, (¬𝛽) ∨ 𝛾 ′) ≠ None }. The generalizedrefinement problem asks, given a trace Φ and an assertion ¬𝛽, to find a pair (Φ′, 𝛾) such that 𝛾 isthe counterexample of (Φ, ¬𝛽) and Φ′ ∈ Refine(Φ, ¬𝛽 ∨ 𝛾).
□
For implementational reasons, we often slightly weaken the requirement for 𝛾. A predicate 𝛾 is acounterexample in the weak sense if (1) Refine(Φ, ¬𝛽) ≠ None and 𝛾 = ⊥ or (2) Refine(Φ, ¬𝛽) =None and 𝛾 ∧ 𝛽 is a counterexample in the proper sense.
4.2Naïve Procedure

Algorithm 3 presents a naïve procedure for the generalized refinement problem.
• Line 2: The procedure immediately returns without making any change to the input Φ if therequirement is trivially satisfied.
• Lines 4–6: If the initial state 𝜄 (𝑧) intersects with ¬𝛼 (𝑧), the requirement is trivially unachievable. The requirement 𝛼 must be weakened at least to 𝛼 (𝑧) ∨𝛾 (𝑧) where 𝛾 (𝑧) = (𝜄 (𝑧) ∧¬𝛼 (𝑧)).
The following part checks if 𝛼 should be further weakened.
• Line 7: The condition checks if one can refine the input trace Φ without changing thesubtraces Φ𝐿 and Φ𝑅 . If it is not the case, i.e. one needs to change at least one of Φ𝐿 and Φ𝑅 ,lines 8–15 are executed.
• Lines 8 and 9: We first try to refine the trace without changing the left subtrace (i.e. changing
only the subtrace Φ𝑅 ). The condition required for the refinement subtrace Φ𝑅′ is that 𝜑𝐿 (𝑥) ∧𝜑𝑅′ (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) does not intersects with ¬𝛼 (𝑧). Line 8 lets ¬𝜓𝑅 be the weakest predicatethat satisfies this requirement. Line 9 checks if Φ𝑅 can be refined so that 𝜑𝑅′ (𝑦) |= ¬𝜓𝑅 (𝑦).
• Lines 10–12: If 𝛾𝑅 ≠ ⊥, we need to change Φ𝐿 . The refinement procedure for Φ𝐿 is similar
to that of Φ𝑅 (lines 8 and 9).
• Lines 13–15: If 𝛾𝐿 ≠ ⊥, there is no refinement of Φ satisfying 𝛼. The counterexample foundat this step comes from 𝛾𝐿 and 𝛾𝑅 .
• Lines 16 and 17: Now 𝛼 is sufficiently weakened and 𝜑𝐿 and 𝜑𝑅 are sufficiently strengthened.
We calculate an appropriate 𝜑𝜖 .
Proposition 12. Algorithm 3 always terminates and solves the generalized refinement problem. □4.3

Handling Quantification by Model-Based Projection

Algorithm 3 is simple but it uses quantified formulas. The quantifiers can be removed by using
quantifier elimination, but a quantifier elimination procedure is computationally expensive.
Algorithm 4 is a refinement procedure using model-based projection for reasoning about quantified formulas. It is basically obtained by replacing the quantified formulas 𝜑𝑅 , 𝜑𝐿 and 𝛾 in lines 8,
11 and 14 in Algorithm 3 with the quantifier-elimination based on model-based projection (Algorithm 1). Intuitively lines 8–9 (resp. lines 11–12 and lines 14–15) perform quantifier elimination of𝜑𝐿 (𝑥) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧) (resp. 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧) and 𝛾𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧)).
It is worth noting an important twist in Algorithm 4 for its termination. Line 7 records the valueof 𝜑𝐿 at that point, and model-based projection uses the recorded values. This twist makes theformulas for model-based projection loop invariants, and the loop invariance plays a crucial role in
the termination proof. Note that the image finiteness of model-based projection is applied only tothe case where the argument formula is unchanged.
Algorithm 4 enjoys nice properties that the naïve algorithm (Algorithm 3) has. The proof isessentially the same as that for Algorithm 3 except for the above-mentioned twist.
Theorem 13. Algorithm 4 always terminates and solves the generalized refinement problem.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:13

Algorithm 3 Naïve refinement procedure
1: function Naïve(Φ, 𝛼)2:if dom(Φ) = ∅ or 𝜑𝜖 (𝑥) |= 𝛼 (𝑥) then return (Φ, ⊥)3:
𝛾 := ⊥
4:
if |= ∃𝑧.𝜄 (𝑧) ∧ ¬𝛼 (𝑧) then5:𝛾 (𝑧) := 𝜄 (𝑧) ∧ ¬𝛼 (𝑧)
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:

𝛼 (𝑧) := 𝛼 (𝑧) ∨ 𝛾 (𝑧)if |= ∃𝑥 .∃𝑦.∃𝑧.𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧) then𝜓𝑅 (𝑦) := ∃𝑥 .∃𝑧.𝜑𝐿 (𝑥) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧)(Φ𝑅 , 𝛾𝑅 ) := Naïve(Φ𝑅 , ¬𝜓𝑅 )if 𝛾𝑅 ≠ ⊥ then𝜓𝐿 (𝑥) := ∃𝑦.∃𝑧.𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧)(Φ𝐿 , 𝛾𝐿 ) := Naïve(Φ𝐿 , ¬𝜓𝐿 )if 𝛾𝐿 ≠ ⊥ then𝛾 (𝑧) := 𝛾 (𝑧) ∨ ∃𝑥 .∃𝑦.𝛾𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧)𝛼 (𝑧) := 𝛼 (𝑧) ∨ 𝛾 (𝑧)𝜑𝜖 (𝑧) := Itp 𝜄 (𝑧) ∨ 𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) , 𝜑𝜖 (𝑧) ∧ 𝛼 (𝑧))return (Φ, 𝛾)

Algorithm 4 Naïve procedure with model-based projection
1: function NaïveMbp(Φ, 𝛼)

17:
18:

E

13:
14:
15:
16:

E

7:
8:
9:
10:
11:
12:

if dom(Φ) = ∅ or 𝜑𝜖 (𝑥) |= 𝛼 (𝑥) then return (Φ, ⊥)Γ(𝑧) := ⊥if |= ∃𝑧.𝜄 (𝑧) ∧ ¬𝛼 (𝑧) then𝛾 (𝑧) := 𝜄 (𝑧) ∧ ¬𝛼 (𝑧)Γ(𝑧) := 𝛾 (𝑧)const 𝜑 0,𝐿 := 𝜑𝐿
while ∃M𝑅 . M𝑅 |= 𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬(𝛼 (𝑧) ∨ Γ(𝑧)) do𝜓𝑅 (𝑦) := Mbp( 𝑥𝑧.𝜑 0,𝐿 (𝑥) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧), M𝑅 )(Φ𝑅 , 𝛾𝑅 ) := NaïveMbp(Φ𝑅 , ¬𝜓𝑅 )while ∃M𝐿 . M𝐿 |= 𝜑𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬(𝛼 (𝑧) ∨ Γ(𝑧)) do𝜓𝐿 (𝑥) := Mbp( 𝑦𝑧.𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧), M𝐿 )(Φ𝐿 , 𝛾𝐿 ) := NaïveMbp(Φ𝐿 , ¬𝜓𝐿 )while ∃M. M |= 𝛾𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬(𝛼 (𝑧) ∨ Γ(𝑧)) do
𝛾 (𝑧) := Mbp( 𝑥𝑦.𝛾𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧), M)
Γ(𝑧) := Γ(𝑧) ∨ 𝛾 (𝑧)𝜑𝜖 (𝑧) := Itp 𝜄 (𝑧) ∨ (𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧)), 𝜑𝜖 (𝑧) ∧ (𝛼 (𝑧) ∨ Γ(𝑧))return (Φ, Γ)
E

2:
3:
4:
5:
6:

Proof sketch. We prove the termination; the soundness is relatively easy to see. The point isthat the arguments for Mbp in lines 9, 12, and 15 are invariants of the loops starting from lines 8, 11,
and 14, respectively. Hence, 𝜓𝑅 , 𝜓𝐿 , and 𝛾 can only take on a finite variety of values. So, it suffices
to show that the same value does not occur twice, which follows from the progress property. □Algorithm 5 is a further lazy version of Algorithm 4. Recall that the counterexample Γ generated
by Algorithm 4 is the disjunction Γ = 𝛾 1 ∨ · · · ∨𝛾𝑛 of formulas given by Mbp in line 15 (where 𝑛 is theProc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:14

Takeshi Tsukada and Hiroshi Unno

Algorithm 5 A Spacer-like refinement procedure
1: function IndSpacer(Φ, 𝛼)2:if dom(Φ) = ∅ or 𝜑𝜖 (𝑥) |= 𝛼 (𝑥) then return (Φ, ⊥)3:
Γ(𝑧) := ⊥; Γ𝑅 (𝑦) := ⊥4:
if |= ∃𝑧.𝜄 (𝑧) ∧ ¬𝛼 (𝑧) then5:𝛾 (𝑧) := 𝜄 (𝑧) ∧ ¬𝛼 (𝑧)

16:
17:
18:
19:

E

10:
11:
12:
13:
14:
15:

E

7:
8:
9:

return (Φ, 𝛾)const 𝜑𝐿,0 := 𝜑𝐿
while ∃M𝑅 . M𝑅 |= 𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬(𝛼 (𝑧) ∨ Γ(𝑧)) do𝜓𝑅 (𝑦) := Mbp( 𝑥𝑧.𝜑𝐿,0 (𝑥) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧), M𝑅 )(Φ𝑅 , 𝛾𝑅 ) := IndSpacer(Φ𝑅 , (¬𝜓𝑅 ) ∨ Γ𝑅 )
Γ𝑅 (𝑦) := Γ𝑅 (𝑦) ∨ 𝛾𝑅 (𝑦)while ∃M𝐿 . M𝐿 |= 𝜑𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬(𝛼 (𝑧) ∨ Γ(𝑧)) do𝜓𝐿 (𝑥) := Mbp( 𝑦𝑧.𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧), M𝐿 )(Φ𝐿 , 𝛾𝐿 ) := IndSpacer(Φ𝐿 , ¬𝜓𝐿 )while M |= 𝛾𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬(𝛼 (𝑧) ∨ Γ(𝑧)) do
𝛾 (𝑧) := Mbp( 𝑥𝑦.𝛾𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧), M)
return (Φ, 𝛾)𝜑𝜖 (𝑧) := Itp 𝜄 (𝑧) ∨ (𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧)), 𝜑𝜖 (𝑧) ∧ (𝛼 (𝑧) ∨ Γ(𝑧))return (Φ, ⊥)E

6:number of executions of Line 15 and 𝛾𝑖 is the result of Mbp in the 𝑖-th iteration). Algorithms 4 and 5
behave similarly until the first disjunct 𝛾 1 of the counterexample is found, but then Algorithm 5
returns 𝛾 1 without calculating the remaining part 𝛾 2 ∨ · · · ∨ 𝛾𝑛 of the counterexample Γ = 𝛾 1 ∨ 𝛾 2 ∨· · · ∨ 𝛾𝑛 . Basically Algorithm 5 is obtained by replacing Γ(𝑧) := Γ(𝑧) ∨ 𝛾 (𝑧) with return 𝛾.11
Because of this change, Algorithm 5 is no longer a procedure for the generalized refinement
problem. It just returns a piece of the counterexample, so one needs to invoke IndSpacer manytimes to obtain the whole counterexample as in the following program:Γ(𝑧) := ⊥(Φ, 𝛾) := IndSpacer(Φ, 𝛼)while 𝛾 ≠ ⊥ doΓ(𝑧) := Γ(𝑧) ∨ 𝛾 (𝑧)(∗)(Φ, 𝛾) := IndSpacer(Φ, 𝛼 ∨ Γ)
return (Φ, Γ).
The variable Γ𝑅 in Algorithm 5 originates from Γ in this program.
Theorem 14. The procedure (∗) using Algorithm 5 always terminates and solves the generalizedrefinement problem.
Proof sketch. We prove the termination; the soundness is relatively easy to show.
The most important property of IndSpacer is that the number of values possibly returned as 𝛾
is finite. This claim can be easily proved by induction. The return value 𝛾 is generated in line 16,
which invokes Mbp, so the variety of 𝛾 is finite for a fixed 𝛾𝐿 and 𝛾𝑅 . The induction hypothesisshows that 𝛾𝐿 and 𝛾𝑅 range over a finite set. Hence, the variety of 𝛾 is finite.
In the program (∗), the returned 𝛾 is accumulated in Γ and IndSpacer(Φ, 𝛼 ∨ Γ) will never return
𝛾 such that 𝛾 ⇒ Γ. So, the while loop in (∗) terminates, provided that each iteration terminates.
11 The variable Γ will never be updated in Algorithm 5 and thus can be removed, but it is left for comparison with Algorithm 4.

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:15

The while loops in Algorithm 5 terminate for the same reason as Algorithm 4, namely that thearguments of Mbp are loop invariants. So, the progress ensures the termination.
□
Remark 15. In fact, Algorithms 4 and 5 enjoy termination even without line 7 (and replace 𝜑𝐿,0with 𝜑𝐿 ), but the termination proof is fairly sublte. For example, for the termination of the variants
without line 7, it is necessary to store 𝜑𝐿 and 𝜑𝑅 separately, and it is not the case in Spacer
implementations (as the traces are managed by levels). In such cases, 𝜑𝐿,0 is essential for termination.
More subtly, 𝜑𝐿,0 need not be a constant for the whole procedure. One can freely update 𝜑𝐿,0 to
the current value of 𝜑𝐿 during the execution of the body of the middle loop (Lines 12-16 and 13–17
in Algorithms 4 and 5, respectively) without losing refutational completeness. This claim can beproved by providing a termination measure reduced by entry into the body of the middle loop. The
construction of a termination measure is, however, crucially relies on details of Algorithms 4 and 5.
5 COMPARING OUR PROCEDURES WITH SPACER
This section compares Algorithm 5 with procedures in Komuravelli et al. [2014, 2016] and Komuravelli et al. [2015], as well as GPDR [Hoder and Bjørner 2012]. Section 5.1 discusses the similarily;
Section 5.2 discusses the dissimilarity mainly focusing on the refutational completeness. Section 5.3
deals with other differences and ways to fill the gap.
5.1 Similarity
The simplest way to formally show the similarity is to provide a transition system corresponding
to Algorithm 5. Algorithm 5 is a first-order program and thus executable by a stack machine. The
transition rules for the induced stack machine resemble the rules in fig. 1.
Unfortunately, we cannot discuss this in detail here due to space constraints, so we explain
the correspondence between the rules in fig. 1 and the procedure in Algorithm 5 at an intuitive
level. (DecideMust) is performed in lines 12–14 (recall that 𝛾𝑅 corresponds to U). (DecideMay)
is performed in lines 8–10. (Conflict) corresponds to lines 18–19. (Successor) is lines 15–17.
(Candidate) and (Unfold) can be found in the top level function (Algorithm 2). (Candidate) is
the function call IndSpacer(Φ, 𝛼) in line 5, and (Unfold) is line 4. (Leaf) and (Induction) haveno corresponding part in Algorithm 5. These rules shall be discussed below.
Remark 16. Algorithm 5 with a special choice of Mbp yields a procedure like GPDR [Hoder andBjørner 2012]. The choice is given by
Mbp( 𝑥®.𝜗 (𝑥,
® 𝑦),
® M)

:=

(𝑦1 = 𝑐 1 ) ∧ · · · ∧ (𝑦𝑛 = 𝑐𝑛 )E

where 𝑦1 . . . 𝑦𝑛 = 𝑦® and 𝑐𝑖 = M (𝑦𝑖 ). In other words, this procedure returns the logical representationof the model M restricted to 𝑦.
® This function satisfies most conditions for model-based projection
except for the image finiteness.
The naïve procedure (Algorithm 3) is also obtained by choosing Mbp as the quantifier elimination.
In this sense, Algorithm 5 unifies Spacer, GPDR, and the naïve algorithm.
5.2

Dissimilarity

There are three major differences between Algorithm 5 and Spacer presented in fig. 1. Each of thesedifferences may cause the divergence of the procedure, breaking the refutational completeness.
The first difference is the arguments of Mbp in lines 9 and 13. The arguments in Algorithm 5 areloop invariants, and this fact plays a crucial role in the termination proof. In the corresponding
rules (DecideMust), (DecideMay) and (Successor) in fig. 1, the arguments are not “invariants”.
For example, the argument of Mbp in (DecideMust) (corresponding to lines 12–14 in Algorithm 5)
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:16

Takeshi Tsukada and Hiroshi Unnois 𝜑𝑛+1 (𝑥) ∧ U (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧), which is 𝜑𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧) written in thesymbols in Algorithm 5. This is not an invariant of the middle loop because of 𝜑𝐿 (𝑥).
The second difference is the argument of Mbp in line 16. This Mbp is called at most once, so theloop invariance does not matter here. However, the finiteness of possible return values 𝛾, which is
the key to the termination proof of Algorithm 5 (Theorem 14), essentially relies on the choice ofthe formula in line 16. The corresponding formula U (𝑥) ∧ U (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧) in (Successor)
in fig. 1 contains the query formula 𝜓 , of which the variety cannot be finitely bound.
The third difference is the management of the counterexamples. Whereas Algorithm 5 deals thecounterexamples 𝛾𝑅 and 𝛾𝐿 locally, the transition system in fig. 1 manipulates their cumulative
union U. This change also breaks the finiteness of 𝛾 possibly returned by the procedure, as weshall see below.
Interestingly, the second and third points were changes made in Komuravelli et al. [2015]. The
original Spacer [Komuravelli et al. 2014, 2016] is closer to ours, except for the argument of Mbp inline 9: in the original Spacer, the argument of Mbp in (DecideMay)12 is 𝜑𝑛+1 (𝑥) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ 𝜓 (𝑧),which involves a non-invariant 𝜑𝑛+1 (corresponding to 𝜑𝐿 in Algorithm 5). In our understanding,this difference is the unique source of possible divergence in the original Spacer.
5.3

Optimizations

This subsection discusses how to fill the gaps between our algorithms and actual implementations
by modifying our algorithms. We refer to the implementational tricks discussed in this section
optimizations in the hope that such tricks will improve performance. Some optimizations are
implemented and empirically evaluated in Section 7.
Let us first discuss a criterion for ensuring the termination property for a modification of
Algorithm 5. The points of the termination proof are (1) the arguments of model-based projection
are loop invariants, (2) the same countermodel M does not appear twice in Line 8 (resp. in Line 12,
in Line 15). Point (1) is achieved by saving the necessary values to local variables (as in Line 7), so
any change to Φ does not affect this point, but a change to 𝛾𝐿 and/or 𝛾𝑅 would need care. Point (2)is not affected if an optimization only strengthens the trace, and optimizations below satisfy thiscriterion.
We discuss five optimizations. The first four do not break the termination, but the last one needs
care since it is about 𝛾𝐿 and 𝛾𝑅 .
Predicate Sharing. We use a trace Φ with dom(Φ) = {𝐿, 𝑅} ≤𝑘 , which has a tree structure. Many
existing procedures use a trace (𝜑𝑖 )0≤𝑖 ≤𝑘 of the linear structure, that means, from our viewpoint,
they maintain additional constraints { 𝜑 𝑤 = 𝜑 𝑤′ | 𝑤, 𝑤 ′ ∈ {𝐿, 𝑅} ≤𝑛 , |𝑤 | = |𝑤 ′ | }.
This difference can be bridged by turning traces into trees of references to logical formulas rather
than trees of logical formulas. The tree (ℓ𝑤 )𝑤 ∈ {𝐿,𝑅 } ≤𝑘 of references to formulas is constructed sothat the nodes ℓ𝑤 and ℓ𝑤′ point to the same reference cell whenever |𝑤 | = |𝑤 ′ |. Then Line 18 in
Algorithm 5 updates, in effect, all the formulas at the same level simultaneously.
Monotone Trace. Another difference in the structure of trace is monotonicity. That means, many
existing solvers maintain 𝜑𝑖+1 ⇒ 𝜑𝑖 . This gap can be filled by changing Line 18 in Algorithm 5 toconjoin the interpolant to every formula 𝜑 𝑤 in the trace Φ.
Induction Rule. Roughly speaking, the induction rule checks whether a property 𝜓 establishedat a level (i.e. 𝜑 𝑤 contains 𝜓 as a subformula) can be promoted to the adjacent level (and promotes
the property if possible). This rule can be used at any time in the definition of the transition system,
and it is difficult to incorporate the behavior of such a flexible rule into Algorithm 5. However,
12 The rule is called (Query) in Komuravelli et al. [2016].

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:17

as Hoder and Bjørner [2012] noted in their description of the induction rule, there are typicallytwo situations where this rule can be used effectively, namely, (1) when a refinement process of arecursive call finishes (i.e. at the end of each iteration of the outer and middle loops in Algorithm 5),
and (2) when the trace is expanded at Line 4 in Algorithm 2. It is not difficult to perform theinduction rule applied only for these moments: Simply analyze 𝜑𝐿 and/or 𝜑𝑅 at that moment, andconjoin to 𝜑𝜖 the properties that also hold at the root 𝜖. The analysis of 𝜑𝐿 and 𝜑𝑅 may take time, so
our implementation records candidate properties for the induction rule in the refinement process
and returns the list of candidates in addition to the frame and the counterexample.
Query Reuse. A version of Spacer given in Komuravelli et al. [2015] poses a query that has
been successfully resolved to the adjacent level. This behavior can be simulated by inserting(Φ, _) := IndSpacer(Φ,𝜓𝐿 )at the end of the middle loop in Algorithm 5 and similar code at the end of the outer loop.
Counterexample Sharing. Algorithm 5 passes only the counterexamples relevant to eachquery, but many procedures often remember only the cumulative union of the counterexamples
found. To simulate this behavior, one can use a global variable, which stores the cumulative unionof the counterexamples, and replace 𝛾’s in Algorithm 5 with the dereference of the global variable.
As we mentioned in Section 3.3, the original Spacer [Komuravelli et al. 2014, 2016] managed thecounterexamples by levels, whereas fig. 1 and Komuravelli et al. [2015] unifies the counterexamples
of all the levels. The former change is harmless, but the latter is not.
To see the point, let us recall the proof of the termination of Algorithm 5 (Theorem 14). The
key is the fact that 𝛾 returned by Algorithm 5 has only a finite variety, and this fact is proved byinduction. In the former style of counterexample sharing, the variety of the cumulated values U𝑖
is finite (by induction on 𝑁 − 𝑖). However, since the cumulated value U is not indexed by levels,
the inductive argument to prove the finiteness of possible values for U fails. This is the second
additional source of incompleteness introduced by the changes made in [Komuravelli et al. 2015].
6 A TERMINATING PROCEDURE USING COROUTINES
Although Algorithm 5 enjoys the termination property, it essentially relies on the finiteness of thevariety of possible return values 𝛾. The finiteness of return values is not a procedure-local property(i.e. it requires an analysis of scenarios where the procedure is invoked more than once), so it is hard
to maintain. Indeed, we have just seen that the counterexample sharing across levels (as is done in
Komuravelli et al. [2015]) breaks this property and cannot be incorporated into Algorithm 5.
This section presents another approach to termination guarantee. The termination guaranteeof Algorithm 5 is hard because this procedure discards the remaining computation of the counterexample when it generates the first piece 𝛾 of the counterexample. A desirable procedure should
return the control to the caller as soon as a piece 𝛾 of the counterexample is found but, at the sametime, allow us to resume the continuation if necessary. These apparently incompatible requirements
are achieved using a rich control mechanism known as coroutine.
Algorithm 6 shows the proposed algorithm. The structure is close to Algorithm 5 but it uses
yield instead of return. Similar to return, the yield construct suspends the procedure and returns
the control to the caller. But yield allows the caller to resume the continuation if necessary.
Let us first explain the behavior of the procedure. The procedure call McrCoroutine(Φ, 𝛼) is
immediately returned. Its value cor can be used to enumerate counterexamples. To get the next
counterexample, call cor.next(𝛼 ′), where 𝛼 ′ is the latest assertion, which may be weaker thanthe original assertion 𝛼. This call returns a counterexample for 𝛼 ′ if it exists. If there is no morecounterexample, this call raises an exception StopIteration(Φ′), where Φ′ is the refinement.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:18

Takeshi Tsukada and Hiroshi Unno

Algorithm 6 A Spacer-like procedure with early return using coroutine
1: function McrCoroutine(Φ, 𝛼)2:if dom(Φ) = ∅ or 𝜑𝜖 (𝑥) |= 𝛼 (𝑥) then return Φ3:
if |= ∃𝑧.𝜄 (𝑧) ∧ ¬𝛼 (𝑧) then4:𝛾 (𝑧) := 𝜄 (𝑧) ∧ ¬𝛼 (𝑧)5:𝛼 := yield 𝛾

21:
22:
23:
24:
25:
26:

E

16:
17:
18:
19:
20:

E

10:
11:
12:
13:
14:
15:

const 𝜑 0,𝐿 := 𝜑𝐿 ; 𝛼 0 := 𝛼while ∃M𝑅 . M𝑅 |= 𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧) do𝜓𝑅 (𝑦) := Mbp( 𝑥𝑧.𝜑 0,𝐿 (𝑥) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 0 (𝑧), M𝑅 )cor 𝑅 := McrCoroutine(Φ𝑅 , ¬𝜓𝑅 )try loop𝛾𝑅 := cor 𝑅 .next(¬𝜓𝑅 )𝛼 1 := 𝛼while ∃M𝐿 . M𝐿 |= 𝜑𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧) do𝜓𝐿 (𝑥) := Mbp( 𝑦𝑧.𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 1 (𝑧), M𝐿 )cor 𝐿 := McrCoroutine(Φ𝐿 , ¬𝜓𝐿 )try loop𝛾𝐿 := cor 𝐿 .next(¬𝜓𝐿 )while ∃M. M |= 𝛾𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) ∧ ¬𝛼 (𝑧) do
𝛾 (𝑧) := Mbp( 𝑥𝑦.𝛾𝐿 (𝑥) ∧ 𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧), M)
𝛼 := yeild 𝛾
𝜓𝐿 (𝑥) := 𝜓𝐿 (𝑥) ∧ ¬Itp(𝛾𝐿 (𝑥), (𝛾𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧)) ⇒ 𝛼 (𝑧))with StopIteration(Φ𝐿′ ) → Φ𝐿 := Φ𝐿′
E

6:
7:
8:
9:

𝜓𝑅 (𝑦) := 𝜓𝑅 (𝑦) ∧ ¬Itp(𝛾𝑅 (𝑦), (𝜑𝐿 (𝑥) ∧ 𝜏 (𝑥, 𝑦, 𝑧)) ⇒ 𝛼 (𝑧))with StopIteration(Φ𝑅′ ) → Φ𝑅 := Φ𝑅′𝜑𝜖 (𝑧) := Itp 𝜄 (𝑧) ∨ (𝜑𝐿 (𝑥) ∧ 𝜑𝑅 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧)), 𝜑𝜖 (𝑧) ∧ 𝛼 (𝑧)return Φ

We explain the implementation (Algorithm 6). When the refinement procedure finds a partial
counterexample (lines 18 and 19), it is passed to the yield construct (line 20). The yield constructsuspends the rest of the computation of the counterexample, and the suspension is reported to thecaller, with the information of the found partial counterexample 𝛾 (as the return value to the nextcall). The suspended procedure will be resumed with the information of a weakened requirement(passed as the argument to next), when the caller’s calculation of the weakening will be finished.
This additional information is obtained as the “return value” of yeild, and the procedure updates 𝛼
to the weakened one (line 19). This weakening is propagated to the left and right subtraces by therecalculations (lines 21 and 23). (In line 22, the strengthening of 𝜑𝐿′ is also propagated.) When therefinement is completed, the procedure returns the refinement (line 26). The execution of return
Φ raises the exception StopIteration(Φ), which could be caught by the caller.
Although the control flow of Algorithm 6 is quite complicated, it is still defined by induction on
the structure of the trace. This inductive structure helps us to reason about the algorithm.
Theorem 17. The following procedure (Algorithm 6 with a wrapper) terminates and solves thegeneralized refinement problem.
𝛾 := ⊥; cor := McrCoroutine(Φ, 𝛼)
try loop
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:19𝛾 := 𝛾 ∨ cor.next(𝛼 ∨ 𝛾)with StopIteration(Φ′) → return (Φ′, 𝛾).
Algorithm 6 can accomodate the cross-level counterexample sharing. Its termination proof only
relies on the loop-invariance of arguments of Mbp, so it suffices to keep 𝛾𝐿 and 𝛾𝑅 invariant of theloop starting from line 18 by storing these values before the loop as in line 6.
7 IMPLEMENTATION AND EXPERIMENTS
We implemented variants of Spacer as a new tool called MuCyc13 based on the inductive formalization of the paper and conducted a comparative evaluation on them as well as the state-of-the-art
CHC solvers Spacer, Golem, and Eldarica that earned top scores in CHC-COMP’23.14 We also
evaluate the practical significance of the tricks to retain the refutational completeness (RC) discussed
in the previous sections.
7.1

Implementation

MuCyc is implemented in the functional programming language OCaml 5 and supports, asbackground theories, Booleans and linear integer and real arithmetic. We adopted Z3 (version
4.12.6) [de Moura and Bjørner 2008] as the backend SMT solver for satisfiability checking and Craig
interpolation. We implemented and adopted an original MBP procedure in OCaml, despite being
inefficient, because Z3 does not seem to provide APIs for this feature.
It is worth mentioning that, instead of separately implementing different refinement strategies,
we used the language feature known as algebraic effects and handlers, recently introduced to OCaml
5 [Sivaramakrishnan et al. 2021], so that we can modularly implement refinement strategies basedon various control structures including return, yield, and more.15 We also tried to keep otherparts of the implementation as pure functional as possible, by avoiding destructive updates andnon-determinism (except for the one exhibited by Z3). We believe that the inductive, modular, andfunctional implementation makes it easy to understand, reason about, and extend MuCyc.
7.2 Experiments
We now report on the comparative evaluation with various configurations of MuCyc and existing
CHC solvers Spacer [Komuravelli et al. 2016], Golem,16 and Eldarica [Hojjat and Rümmer 2018].
In the experiments, we used a version of Spacer that is bundled with Z3 (version 4.12.6)17 and theconfiguration of Golem used in the LIA-nonlin category of CHC-COMP’23 (where a verificationengine that implements a Spacer-like algorithm is adopted) and the configuration of Eldarica usedin CHC-COMP’22. For MuCyc, we write Ret(b, cex) and Yld(b, cex) to denote its configurations
based on return and yield, respectively. The boolean parameter b of Ret is either T or F andrepresents whether the counterexample accumulation (see Line 11 in Algorithm 5) is enabled.
The boolean parameter b of Yld represents whether the query weakening via Craig interpolation(see Lines 21 and 23 in Algorithm 6) is enabled. The parameter cex represents the counterexample
enumeration method used. MuCyc supports QE, MBP(n), and Model. The experiment results using
QE are omitted in the paper because it significantly degraded the performance. The parameter
13 Available from https://github.com/hiroshi-unno/coar.
14 https://chc-comp.github.io/
15 Our modular implementation allows us to switch yield and return even during verification depending on, for example,

the level of the current trace and the number of queries occurred so far at the level, though an evaluation of the advanced
capability is left as a future work.
16 https://verify.inf.usi.ch/golem
17 The version is different from GSpacer [Krishnan et al. 2020] that further extends Spacer with various optimization
techniques. It is an interesting future direction to incorporate them to MuCyc and perform an experimental comparison.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:20

Takeshi Tsukada and Hiroshi Unno

Table 1. Experimental Results
configuration
Ret(F, Model)
Ret(T, Model)
Ret(F, MBP(0))
Ret(T, MBP(0))
Ret(F, MBP(1))
Ret(T, MBP(1))
Ret(F, MBP(2))
Ret(T, MBP(2))

sat
605
604
795
770
787
770
676
753

unsat
486
484
521
525
519
526
495
525

configuration
Yld(F, Model)
Yld(T, Model)
Yld(F, MBP(0))
Yld(T, MBP(0))
Yld(F, MBP(1))
Yld(T, MBP(1))
Yld(F, MBP(2))
Yld(T, MBP(2))

sat
588
599
729
772
723
786
729
775

unsat
479
481
521
525
519
525
520
526

configuration
Ind(Ret(F, MBP(0)))
Cex(Ret(F, MBP(0)))
Que(Ret(F, MBP(0)))
Mon(Ret(F, MBP(0)))
Ind(Yld(T, MBP(1)))
Cex(Yld(T, MBP(1)))
Que(Yld(T, MBP(1)))
Mon(Yld(T, MBP(1)))

sat
909
788
762
796
915
773
669
778

unsat
519
524
506
518
526
529
280
518

𝑛 ∈ {0, 1, 2} of MBP(n) represents whether the saved frame and query are used (see Lines 7 and
9 in Algorithm 5 and Lines 6, 8, 12, and 14 in Algorithm 6) for RC (𝑛 = 1, 2) or not (𝑛 = 0). The
difference between 𝑛 = 1 and 𝑛 = 2 is that the former uses more recent information while RC holds
by appropriately updating 𝜑𝐿,0 (see the second paragraph of Remark 15).
MuCyc also supports optimizations discussed in Section 5.3: induction Ind(config), counterexample sharing Cex(config), query reuse Que(config), and monotone trace Mon(config). MuCyc
also implements predicate sharing but does not support disabling it, and hence no corresponding
notation. For example, the configuration of MuCyc closest to Spacer is described as Ind(Cex(F,Que(Mon(Ret(F, MBP(0)))))).18 The configuration closest to GPDR [Hoder and Bjørner 2012] isInd(Cex(F, Mon(Ret(F, Model)))). Besides Yld and Ret, MuCyc supports a Solve configurationthat employs an existing method for solving non-linear CHCs [Unno and Kobayashi 2009]. Thismethod aligns with Algorithm 2, but with the Refine step replaced by a recursion-free CHC solverthat disregards the current trace Φ. Specifically, Solve iteratively expands the given CHCs, solves
the result by invoking Spacer as a recursion-free CHC solver, and checks whether the solution is
inductive. We use this as a baseline in the experiments.
Table 1 summarizes the number of solved SAT and UNSAT instances. We here used a benchmark
set consisting of 1,972 CHCs satisfiability problem instances obtained from the benchmark setsof the LIA-lin and LIA-nonlin categories of CHC-COMP from 2018 to 2022: we here implemented
and applied a CHC preprocessor to them a priori and filtered out easy instances that were solved
by just preprocessing. Our intention here is to weaken the effect on the experiment results ofdifferent preprocessors implemented in the existing CHC solvers and focus on the strengths andweaknesses of their main algorithms. Our preprocessor repeatedly applies the resolution rule toeliminate redundant predicate variables and apply an existing algorithm for reducing unnecessary
arguments of predicate variables [Leuschel and Sørensen 1997]. All the experiments were conducted
on StarExec (CentOS Linux release 7.7.1908, Intel(R) Xeon(R) CPU E5-2609 @ 2.40GHz with 27 GiBRAM) with 600 seconds time limit.
7.2.1 Model vs. MBP(0) vs. MBP(1) vs. MBP(2). By comparing Ret(F, MBP(0)) (corresponding to Spacer without optimizations) with Ret(F, Model) (GPDR without optimizations), we cansee that the use of MBP significantly improves the numbers. Recall that the use of the saved queryand frame in the Spacer algorithm (indicated by Ret(F, MBP(2))) loses the progress property (andcauses an infinite loop without refinement) and hence substantially reduces the performance. By
contrast, the configuration Ret(T, MBP(2)) satisfies the progress property again and is even RC.
By comparing Ret(T, MBP(1)) and Ret(T, MBP(2)) that are both RC, we can see that the use of
18 Note here that implementation details of the four optimizations in MuCyc can be different from those of Spacer since

they are only exposed as non-deterministically applied rules in the papers of Spacer.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:21more recent information contributes the performance. By comparing Ret(T, MBP(1)) and Ret(F,MBP(1)), we can also see that the counterexample accumulation that is necessary for RC affects
negatively to the number of solved SAT instances but positively to that of UNSAT. It is worth notingthat the non-RC configuration Ret(F, MBP(0)) that uses the latest information outperformed thebest RC configuration Ret(T, MBP(1)) with respect to the number of solved SAT instances.
However, in the setting of the yield-based strategies, the experimental results showed a different trend, with Yld(T, MBP(1)), which utilizes the most recent information while RC holds,
outperforming the other configurations.
7.2.2 Query weakening. By comparing the two variants Yld(T, MBP(n)) and Yld(F, MBP(n)),
which are RC, we can see that enabling query weakening via Craig interpolation improves theperformance of yield-based strategies.
7.2.3 Optimizations. We now discuss the effect of the optimizations: induction, counterexample
sharing, query reuse, and monotone trace. Thanks to the modular and functional implementationof MuCyc, we were able to easily implement the optimizations. However, we found it non-trivial toobtain performance improvements with them, as discussed below. We compared Ret(F, MBP(0))
and Yld(T, MBP(1)) with their optimized versions. The induction rule largely contributed to theperformance. The sharing of counterexamples also had a positive effect on the number of solved
UNSAT instances, though it had a negative effect on that of SAT instances. We believe that the
reduction in SAT instances is due to additional overhead, and it seems that reducing this overhead
through tuning could make it a useful optimization.
By contrast, query reuse and monotone trace downgraded the performance. In particular, it issurprising that monotone trace reduced the performance since many existing PDR-based verifiers
employ monotone trace. A possible reason why query reuse was not effective is that our implementation that follows the explanation in Section 5.3 is different from that of Spacer [Komuravelli et al.
2015] and could result in too many extra queries, the cost of which is not compensated by the gains.

Time in seconds (600 seconds time limit)

Fig. 2. MuCyc vs. existing CHC solvers.
7.2.4 MuCyc vs. State-of-The-Art CHC
Solvers. Finally, we compare MuCyc with ourSpacerRC configuration Ind(Yld(T, MBP(1))) withGolem
MuCyc [Ind(Yld(T,MBP(1)))]the state-of-the-art CHC solvers as well as
2
10
MuCyc [Ind(Ret(F,MBP(0)))]the configuration Ind(Ret(F, MBP(0))) that
Eldarica
MuCyc [Solve]
is close to Spacer and the baseline Solve of
MuCyc. The cactus plot shown in Figure 2 plots
101
the number of solved instances (x-axis) against
the time taken to solve the instances (y-axis),
non-cumulatively, comparing the solvers. The
baseline configuration Solve solved 738 SAT
100
and 504 UNSAT, Eldarica solved 893 SAT and
482 UNSAT, Golem solved 971 SAT and 529
UNSAT, and Spacer solved 987 SAT and 547
10−1
UNSAT instances. The results show that the
0
200
400
600
800
1000 1200 1400 1600
mature tool Spacer outperforms the others. DeBenchmarks passed (out of 1972)
spite being new and not yet mature, MuCyc is already as competitive as Eldarica and significantly
outperforms the baseline configuration Solve. Note also that Ind(Yld(T, MBP(1))) slightly outperformed Ind(Ret(F, MBP(0))), despite the observed fact that Yld(T, MBP(1)) and Ret(F, MBP(0))
were incomparable in the absence of optimizations. We believe the gap between the performanceof MuCyc and Golem, which is also based on the Spacer algorithm, could be partly explained asProc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:22

Takeshi Tsukada and Hiroshi Unno

follows: (1) MuCyc does not fully utilize caching and incremental SMT, instead repeatedly calling
Z3 with similar, related queries; (2) The implementation language of MuCyc employs garbage
collection and is generally not as efficient as C++ used to implement Golem and Spacer. Notethat the curves of the MuCyc configurations are more gradual compared to the others. We thus
believe that by increasing the time limit or addressing the two aforementioned issues to speed up
the process, MuCyc could solve an even greater number of problems.
8 RELATED WORKPDR has been applied to verification problems that go beyond CHCs such as symbolic model
checking of Markov decision processes [Batz et al. 2020], verification of relational properties [Shemer
et al. 2019], and verification of distributed protocols [Goel and Sakallah 2021; Karbyshev et al. 2017].
It would be interesting to extend our inductive approach to their PDR algorithms.
There have been proposed extensions of the class of CHCs: existentially quantified CHCs [Beyene
et al. 2013], universally quantified CHCs [Bjørner et al. 2013], pCSP that extends CHCs with headdisjunctions [Satake et al. 2020], pfwCSP that extends pCSP with well-foundedness and functional
constraints [Unno et al. 2021], and higher-order CHCs [Burn et al. 2018]. Also, note that the classof CHCs can be seen as a fragment of first-order fixpoint logic without greatest fixpoints. Recently,
several authors have applied fixpoint logics [Kobayashi et al. 2019, 2018; Unno et al. 2023] as a
generalization of the class of CHCs for formal verification. However, to our knowledge, there exists
no PDR algorithm proposed for the extended classes. It is interesting to investigate whether our
inductive approach can be applied to systematically derive PDR algorithms for them.
As for the CHC solving in the standard setting, Krishnan et al. [2020] and Blicha et al. [2022]
proposed ideas to improve the performance of Spacer. A typical challenge with Spacer that these
papers address is that to find a counterexample of length 𝑛, one has to deal with the 𝑛-fold expansionof the input CHC, which tends to be huge. Krishnan et al. [2020] proposed several heuristics, mainly
a kind of inspection and manipulation of logical formulas. The idea of Blicha et al. [2022] can be
explained in terms of higher-order CHCs [Burn et al. 2018; Kobayashi et al. 2018]. Blicha et al.
[2022] translate an input CHC system in the standard sense, say a first-order CHC, into a secondorder CHC. By making good use of the expressive power of second-order CHC, the number ofdevelopment steps required to find a counterexample is logarithmically shortened.
The above-mentioned work studied PDR mainly from a practical perspective. Recently, analysis
of PDR from a theoretical perspective was given by Feldman et al. [2019, 2022] and Feldman andShoham [2022]. They analyzed PDR using logical and/or computational theoretic ideas.
Model-based projection, which is a key technology for Spacer, is also applied to decide quantified
first-order logic formulas by Bjorner and Janota [2015] and Farzan and Kincaid [2016].
9 CONCLUSION
We have developed an inductive description of Spacer and discussed the behavior of Spacer variantsin the literature based on an intuition from our inductive description. We have implemented andevaluated our procedures. Our experiment has confirmed that some tricks to retain refutational
completeness have a practical impact.
An interesting direction for future work is to find a better naïve algorithm. Our procedures arederived from the naïve algorithm (Algorithm 3), a procedure with quantified formulas, by removing
the quantifications using model-based projection and making the procedure as lazy as possible.
A different choice of the naïve algorithm results in a different procedure. Examples of particular
choices include the iterative deepening version, whereas Algorithm 3 is the depth-first version.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

Inductive Approach to Spacer

227:23

ACKNOWLEDGMENTS
We are grateful to the anonymous reviewers for their insightful comments. Additionally, we would
like to express our appreciation to the anonymous reviewers who provided feedback on the earlier
version submitted to POPL. In particular, a technical comment from a POPL reviewer significantly
affected the structure of our paper. We thank the StarExec initiative for providing the computational
resources necessary for our experiments in this paper. This work was supported by JSPS KAKENHI
Grant Numbers JP20H05703, JP22H03564, JP20H04162, and JP19H04084.
REFERENCES
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schröer. 2020.
PrIC3: Property Directed Reachability for MDPs. In Lecture Notes in Computer Science. Springer International Publishing,
512–538. https://doi.org/10.1007/978-3-030-53291-8_27
Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In
CAV ’13 (LNCS), Vol. 8044. Springer, 869–882.
Nikolaj Bjorner and Mikolas Janota. 2015. Playing with Quantified Satisfaction. In LPAR ’15 (EPiC Series in Computing),
Vol. 35. EasyChair, 15–27.
Nikolaj Bjørner, Ken McMillan, and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS ’13(LNCS), Vol. 7935. Springer, 105–125.
Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, and Natasha Sharygina. 2022. Transition Power Abstractions for
Deep Counterexample Detection. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International
Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022,
Munich, Germany, April 2-7, 2022, Proceedings, Part I (Lecture Notes in Computer Science), Dana Fisman and Grigore Rosu
(Eds.), Vol. 13243. Springer, 524–542. https://doi.org/10.1007/978-3-030-99524-9_29
Aaron R. Bradley. 2011. SAT-Based Model Checking without Unrolling. In Lecture Notes in Computer Science. Springer
Berlin Heidelberg, 70–87. https://doi.org/10.1007/978-3-642-18275-4_7
Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay. 2018. Higher-order constrained horn clauses for verification.
Proceedings of the ACM on Programming Languages 2, POPL (2018), 11:1–11:28.
Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS ’08 (Budapest, Hungary, March29 –April 6) (LNCS), Vol. 4963. Springer, 337–340.
Niklas Een, Alan Mishchenko, and Robert Brayton. 2011. Efficient implementation of property directed reachability. In 2011
Formal Methods in Computer-Aided Design (FMCAD). 125–134.
Azadeh Farzan and Zachary Kincaid. 2016. Linear Arithmetic Satisfiability via Strategy Improvement. In IJCAI ’16. AAAI
Press, 735–743.
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, and Sharon Shoham. 2019. Complexity and Information in Invariant
Inference. 4, POPL, Article 5 (dec 2019), 29 pages.
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox. 2022. Property-Directed Reachability as Abstract
Interpretation in the Monotone Theory. 6, POPL, Article 15 (jan 2022), 31 pages.
Yotam M. Y. Feldman and Sharon Shoham. 2022. Invariant Inference with Provable Complexity from the Monotone Theory.
Springer, Cham, 201–226.
Aman Goel and Karem A. Sakallah. 2021. On Symmetry and Quantification: A New Approach to Verify Distributed Protocols.
In NFM ’21. 131–150.
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2010. Nested interpolants. ACM SIGPLAN Notices 45, 1 (jan2010), 471–482. https://doi.org/10.1145/1707801.1706353
Kryštof Hoder and Nikolaj Bjørner. 2012. Generalized Property Directed Reachability. In Theory and Applications ofSatisfiability Testing – SAT 2012. Springer Berlin Heidelberg, 157–171. https://doi.org/10.1007/978-3-642-31612-8_13
Kryštof Hoder, Nikolaj Bjørner, and Leonardo de Moura. 2011. 𝜇Z: An Efficient Engine for Fixed Points with Constraints. In
CAV ’11 (Snowbird, UT) (LNCS), Vol. 6806. Springer, 457–462.
Hossein Hojjat and Philipp Rümmer. 2018. The Eldarica Horn Solver. In FMCAD ’18. IEEE, 1–7.
Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham. 2017. Property-Directed
Inference of Universal Invariants or Proving Their Absence. J. ACM 64, 1, Article 7 (mar 2017), 33 pages.
Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno. 2019. Temporal Verification of Programs via
First-Order Fixpoint Logic. In SAS ’19. Springer, 413–436.
Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. 2018. Higher-Order Program Verification via HFL Model Checking.
In ESOP ’18. Springer, 711–738.

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.

227:24

Takeshi Tsukada and Hiroshi Unno

Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, and Kenneth L. Mcmillan. 2015. Compositional verification ofprocedural programs using horn clauses over integers and arrays. In 2015 Formal Methods in Computer-Aided Design(FMCAD). IEEE. https://doi.org/10.1109/fmcad.2015.7542257
Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-Based Model Checking for Recursive Programs. In
Computer Aided Verification (CAV). Springer International Publishing, 17–34. https://doi.org/10.1007/978-3-319-08867-9_2
Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2016. SMT-based model checking for recursive programs. Formal
Methods in System Design 48, 3 (jun 2016), 175–205. https://doi.org/10.1007/s10703-016-0249-4
Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, and Arie Gurfinkel. 2020. Global Guidance for Local
Generalization in Model Checking. In CAV ’20 (LNCS), Vol. 12225. Springer, 101–125.
Michael Leuschel and Morten Heine Sørensen. 1997. Redundant argument filtering of logic programs. In LOPSTR ’97.
Springer, 83–103.
K. L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In Computer Aided Verification (CAV 2003) (Lecture
Notes in Computer Science), Vol. 2725. Springer Berlin Heidelberg, 1–13. https://doi.org/10.1007/978-3-540-45069-6_1
Kenneth L. McMillan. 2006. Lazy Abstraction with Interpolants. In Computer Aided Verification. Springer Berlin Heidelberg,
123–136. https://doi.org/10.1007/11817963_14
Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid Types. In PLDI ’08. ACM, 159–169.
Philipp Rümmer, Hossein Hojjat, and Viktor Kuncak. 2014. Classifying and Solving Horn Clauses for Verification. In Verified
Software: Theories, Tools, Experiments. Springer Berlin Heidelberg, 1–21. https://doi.org/10.1007/978-3-642-54108-7_1
Yuki Satake, Hiroshi Unno, and Hinata Yanagi. 2020. Probabilistic Inference for Predicate Constraint Satisfaction. AAAI ’20
34, 02 (Apr. 2020), 1644–1651.
Ron Shemer, Arie Gurfinkel, Sharon Shoham, and Yakir Vizel. 2019. Property Directed Self Composition. In CAV ’19 (LNCS),
Vol. 11561. Springer, 161–179.
KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, and Anil Madhavapeddy. 2021. Retrofitting EffectHandlers onto OCaml. In PLDI ’21 (Virtual, Canada) (PLDI 2021). ACM, 206–221.
Takeshi Tsukada and Hiroshi Unno. 2021. Software Model-Checking as Cyclic-Proof Search. https://doi.org/10.48550/
ARXIV.2111.05617
Takeshi Tsukada and Hiroshi Unno. 2022. Software model-checking as cyclic-proof search. Proceedings of the ACM on
Programming Languages 6, POPL (jan 2022), 1–29. https://doi.org/10.1145/3498725
Hiroshi Unno and Naoki Kobayashi. 2009. Dependent Type Inference with Interpolants. In PPDP ’09. ACM, 277–288.
Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. 2023. Modular Primal-Dual Fixpoint Logic Solving for Temporal
Verification. 7, POPL, Article 72 (jan 2023), 30 pages.
Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021. Constraint-Based Relational Verification. In CAV ’21. Springer,
742–766.

Received 2023-11-16; accepted 2024-03-31

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 227. Publication date: June 2024.