# Unrolling¶

The first tool that Imandra makes available in our verification toolbox is recursive function unrolling, a form of bounded model checking backed by Satisfiability Modulo Theories (SMT) solving. This technique is completely automatic, and is in general not influenced by the presence of proved rules or enabled/disabled functions (except with used in conjunction with the [@@simp] attribute).

## Completeness¶

For many classes of problems, unrolling is "complete" in various senses. For example, for goals involving only non-recursive functions, algebraic datatypes and linear arithmetic, unrolling will always be able to prove a true goal or refute a false goal in a finite amount of time and space. Moreover, for an even wider class of problems involving recursive functions, datatypes and arithmetic, unrolling is "complete for counterexamples." This means that if a counterexample to a goal exists, unrolling will in principle always be able to synthesize one. This relies on Imandra's "fair" strategy for incrementally expanding the "interpretation call-graph" of a goal.

That said, part of the beauty of unrolling is that you don't need to understand it to apply it!

## Strategy¶

In general, it's recommended to apply unrolling to a goal before you attempt other methods such as the inductive waterfall ([@@auto]). It's amazing how often seemingly true goals are false due to subtle edge cases, and the ability of unrolling to construct concrete counterexamples can be an invaluable filter on your conjectures.

## Examples¶

To use unrolling, we simply use the verify or instance commands.

Let's use unrolling to find an instance of two lists of integers, whose sum equals the length of the two lists concatenated. We shall constrain the total length of the two lists to be positive (for fun, at least 10), so we obtain something more interesting than the simple x=[],y=[] solution!

In :
instance
(fun x y -> List.length (x@y) > 10
&& List.fold_left (+) 0 (x@y) = List.length (x@y))

Out:
- : Z.t list -> Z.t list -> bool = <fun>
module CX : sig val x : int list val y : int list end

Instance (after 31 steps, 0.087s):
let (x : int list) = 
let (y : int list) =
[8855; 3609; 1796; (-1); 0; 4679; (-5828); (-13966); 2455; (-3916)]

Instance
proof attempt
ground_instances31
definitions0
inductions0
search_time
0.087s
details
Expand
smt_stats
 arith offset eqs 9 num checks 63 arith assert lower 377 arith pivots 202 rlimit count 64516 mk clause 580 datatype occurs check 647 mk bool var 2583 arith assert upper 280 datatype splits 375 decisions 1144 arith add rows 1263 arith bound prop 9 propagations 1688 interface eqs 36 conflicts 106 arith fixed eqs 294 datatype accessor ax 340 minimized lits 2 arith conflicts 29 arith assert diseq 94 datatype constructor ax 386 num allocs 1.28676e+06 final checks 132 added eqs 4040 del clause 506 arith eq adapter 330 memory 6.53 max memory 6.53
Expand
• start[0.087s]
List.length (List.append :var_0: :var_1:) > 10
&& List.fold_left + 0 (List.append :var_0: :var_1:) =
List.length (List.append :var_0: :var_1:)
• #### simplify

 into not (List.length (List.append :var_0: :var_1:) <= 10) && List.fold_left + 0 (List.append :var_0: :var_1:) = List.length (List.append :var_0: :var_1:) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|List.fold_left +_1216| 0 (|List.append_1208| x_14 y_15)) expansions
• unroll
 expr (|List.append_1208| x_14 y_15) expansions
• unroll
 expr (|List.length_1213| (|List.append_1208| x_14 y_15)) expansions
• unroll
 expr (|List.fold_left +_1216| (+ 0 (|get.::.0_1206| (|List.append_1208| x_14 y_15))) (|get.::.1_… expansions
• unroll
 expr (|List.append_1208| (|get.::.1_1207| x_14) y_15) expansions
• unroll
 expr (|List.length_1213| (|get.::.1_1207| (|List.append_1208| x_14 y_15))) expansions
• unroll
 expr (let ((a!1 (+ 0 (|get.::.0_1206| (|List.append_1208| x_14 y_15)) (|get.:… expansions
• unroll
 expr (|List.length_1213| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| x_14 y_15)))) expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (|List.append_1208| (|get.::.1_1207| (|get.::.1_1207| x_14)) y_15) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (|List.append_1208| (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| x_14))) y_15) expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| x_14)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| x_14)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.0_1206| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| x_14)))))) (|List.a… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1207| (|get.::.1_1207| (|get.::.1_1207| (|List.append_1208| … expansions
• Sat (Some let (x : int list) =  let (y : int list) = [8855; 3609; 1796; (-1); 0; 4679; (-5828); (-13966); 2455; (-3916)] )

Imandra was able to find a solution instantly, and reflected it into our runtime in the CX module. Let's compute with it to better understand it:

In :
List.length (CX.x@CX.y);;
List.fold_left (+) 0 (CX.x@CX.y);;

Out:
- : Z.t = 11
- : Z.t = 11


## Unrolling limits¶

Unrolling works by creating a symbolic call graph for the negation of the goal we've asked Imandra to verify (or dually the positive version of the goal in the case of instance), and by iteratively extending this graph with incremental interpretations of recursive functions, up to a given unrolling bound, checking at each step for satisfiability.

The unrolling bound defaults to 100 and can be controlled globally using the #unroll <n> directive, or local to a given verify or instance call using the ~upto:<n> parameter.

If at any step of the unrolling process the negation of our original goal is satisfiable w.r.t. the interpreted approximations of the recursive functions, then Imandra has found a counterexample for our original goal, which has thus been refuted. In this case, Imandra will report Counterexample (after m steps) and install the found counterexample in the CX module.

If, on the other hand, Imandra is able to prove that there is no counterexample in a manner that is independent of the bound on the approximations, then our original goal is indeed a theorem valid for all possible inputs, and Imandra will report Theorem Proved. This can always be done for a wide class of theorems on catamorphisms (e.g., List.fold_right), for example.

Otherwise, if Imandra failed to find a counterexample or proof and stopped unrolling at the unrolling bound, we obtain a weaker result of the form Unknown (verified up to depth k), which effectively means: this may or may not be a theorem, but there are no counterexamples up to depth k. Such bounded results can nevertheless be very useful.

Let's try to understand in practice how the unrolling bound plays into unrolling. Consider this simple function that recursively decreases an integer until it reaches 0, then returns 1:

In :
let rec f x =
if x <= 0 then
1
else
f (x - 1)

Out:
val f : int -> Z.t = <fun>

termination proof

### Termination proof

call f (x - 1) from f x
originalf x
subf (x - 1)
original ordinalOrdinal.Int (if x >= 0 then x else 0)
sub ordinalOrdinal.Int (if (x - 1) >= 0 then x - 1 else 0)
path[not (x <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.017s
details
Expand
smt_stats
 num checks 3 arith assert lower 8 arith pivots 2 rlimit count 1027 mk clause 4 datatype occurs check 2 mk bool var 20 arith assert upper 3 decisions 2 arith add rows 3 propagations 2 conflicts 2 arith fixed eqs 2 datatype accessor ax 2 arith conflicts 1 num allocs 5.23053e+06 final checks 1 added eqs 6 del clause 4 arith eq adapter 2 memory 9.77 max memory 9.77
Expand
• start[0.017s]
not (x <= 0)
&& (if x >= 0 then x else 0) >= 0
&& (if (x - 1) >= 0 then x - 1 else 0) >= 0
==> (x - 1) <= 0
|| Ordinal.( << ) (Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0))
(Ordinal.Int (if x >= 0 then x else 0))
• ##### simplify
 into (not ((not (x <= 0) && (if x >= 0 then x else 0) >= 0) && (if x >= 1 then -1 + x else 0) >= 0) || x <= 1) || Ordinal.( << ) (Ordinal.Int (if x >= 1 then -1 + x else 0)) (Ordinal.Int (if x >= 0 then x else 0)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (ite (>= x_1227 1) (+ (- 1) x_1227) 0)) (|Ordi… expansions
• ##### unsat
(let ((a!1 (not (= x_1227 (ite (>= x_1227 0) x_1227 0))))
(a!2 (+ x_1227 (* (- 1) (ite (>= x_1…

Let's verify that for all x < 100, the function will return 1:

In :
verify (fun x -> x < 100 ==> f x = 1)

Out:
- : int -> bool = <fun>

Proved
proof
ground_instances100
definitions0
inductions0
search_time
0.303s
details
Expand
smt_stats
 num checks 201 arith assert lower 99 rlimit count 59930 mk clause 300 mk bool var 504 arith assert upper 1 propagations 297 conflicts 101 arith fixed eqs 2 num allocs 1.86287e+07 final checks 100 added eqs 300 del clause 297 memory 12.22 max memory 12.32
Expand
• start[0.303s] :var_0: < 100 ==> f :var_0: = 1
• #### simplify

 into 100 <= :var_0: || f :var_0: = 1 expansions [] rewrite_steps forward_chaining
• unroll
 expr (f_17 x_19) expansions
• unroll
 expr (f_17 (+ (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) x_19)) expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• unroll
 expr (f_17 (+ (- 1) (- 1) (- 1) (- 1) (- 1) (- 1) (… expansions
• #### unsat

(let ((a!1 (= (ite (<= x_19 99) 1 (f_17 (+ (- 100) x_19))) 1))
(a!3 (not (or (<= 100 x_19) (= …