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 [1]:
instance
  (fun x y -> List.length (x@y) > 10
    && List.fold_left (+) 0 (x@y) = List.length (x@y))
Out[1]:
- : 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.110s):
 let (x : int list) = [2328]
 let (y : int list) =
   [8855; 3609; 1796; (-1); 0; 4679; (-5828); (-13966); 2455; (-3916)]
Instance
proof attempt
ground_instances31
definitions0
inductions0
search_time
0.111s
details
Expand
smt_stats
arith offset eqs9
num checks63
arith assert lower377
arith pivots202
rlimit count64516
mk clause580
datatype occurs check647
mk bool var2583
arith assert upper280
datatype splits375
decisions1144
arith add rows1263
arith bound prop9
propagations1688
interface eqs36
conflicts106
arith fixed eqs294
datatype accessor ax340
minimized lits2
arith conflicts29
arith assert diseq94
datatype constructor ax386
num allocs932572683
final checks132
added eqs4040
del clause506
arith eq adapter330
memory18.700000
max memory20.750000
Expand
  • start[0.111s]
      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 +[0]`_1482| 0 (|List.append_1474| x_989 y_990))
        expansions
        • unroll
          expr
          (|List.append_1474| x_989 y_990)
          expansions
          • unroll
            expr
            (|List.length_1479| (|List.append_1474| x_989 y_990))
            expansions
            • unroll
              expr
              (|`List.fold_left +[0]`_1482|
                (+ 0 (|get.::.0_1472| (|List.append_1474| x_989 y_990)))
                (|get.::.…
              expansions
              • unroll
                expr
                (|List.append_1474| (|get.::.1_1473| x_989) y_990)
                expansions
                • unroll
                  expr
                  (|List.length_1479| (|get.::.1_1473| (|List.append_1474| x_989 y_990)))
                  expansions
                  • unroll
                    expr
                    (let ((a!1 (+ 0
                                  (|get.::.0_1472| (|List.append_1474| x_989 y_990))
                                  (|get…
                    expansions
                    • unroll
                      expr
                      (|List.length_1479|
                        (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474| x_989 y_990))))
                      expansions
                      • unroll
                        expr
                        (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                          …
                        expansions
                        • unroll
                          expr
                          (|List.append_1474| (|get.::.1_1473| (|get.::.1_1473| x_989)) y_990)
                          expansions
                          • unroll
                            expr
                            (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                              …
                            expansions
                            • unroll
                              expr
                              (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                …
                              expansions
                              • unroll
                                expr
                                (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                  …
                                expansions
                                • unroll
                                  expr
                                  (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                    …
                                  expansions
                                  • unroll
                                    expr
                                    (|List.append_1474|
                                      (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| x_989)))
                                      y_990)
                                    expansions
                                    • unroll
                                      expr
                                      (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                        …
                                      expansions
                                      • unroll
                                        expr
                                        (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                          …
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                            …
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                              …
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| x_989))))))
                                                (|List.…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                  …
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                    …
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                      …
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                        …
                                                      expansions
                                                      • unroll
                                                        expr
                                                        (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| x_989))))))
                                                          (|List.…
                                                        expansions
                                                        • unroll
                                                          expr
                                                          (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                            …
                                                          expansions
                                                          • unroll
                                                            expr
                                                            (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                              …
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                                …
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (let ((a!1 (|get.::.0_1472| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                                  …
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| x_989))))))
                                                                    (|List.…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (|get.::.1_1473| (|get.::.1_1473| (|get.::.1_1473| (|List.append_1474|
                                                                                      …
                                                                    expansions
                                                                    • Sat (Some let (x : int list) = [2328] 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 [2]:
                                                                    List.length (CX.x@CX.y);;
                                                                    List.fold_left (+) 0 (CX.x@CX.y);;
                                                                    
                                                                    Out[2]:
                                                                    - : 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 [3]:
                                                                    let rec f x =
                                                                      if x <= 0 then
                                                                        1
                                                                      else
                                                                        f (x - 1)
                                                                    
                                                                    Out[3]:
                                                                    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.018s
                                                                    details
                                                                    Expand
                                                                    smt_stats
                                                                    num checks3
                                                                    arith assert lower8
                                                                    arith pivots2
                                                                    rlimit count1027
                                                                    mk clause4
                                                                    datatype occurs check2
                                                                    mk bool var20
                                                                    arith assert upper3
                                                                    decisions2
                                                                    arith add rows3
                                                                    propagations2
                                                                    conflicts2
                                                                    arith fixed eqs2
                                                                    datatype accessor ax2
                                                                    arith conflicts1
                                                                    num allocs986359492
                                                                    final checks1
                                                                    added eqs6
                                                                    del clause4
                                                                    arith eq adapter2
                                                                    memory19.220000
                                                                    max memory20.750000
                                                                    Expand
                                                                    • start[0.018s]
                                                                        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.<<_116| (|Ordinal.Int_107| (ite (>= x_1493 1) (+ (- 1) x_1493) 0))
                                                                                            (|Ord…
                                                                          expansions
                                                                          • unsat
                                                                            (let ((a!1 (not (= x_1493 (ite (>= x_1493 0) x_1493 0))))
                                                                                  (a!2 (+ x_1493 (* (- 1) (ite (>= x_1…

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

                                                                          In [4]:
                                                                          verify (fun x -> x < 100 ==> f x = 1)
                                                                          
                                                                          Out[4]:
                                                                          - : int -> bool = <fun>
                                                                          
                                                                          Proved
                                                                          proof
                                                                          ground_instances100
                                                                          definitions0
                                                                          inductions0
                                                                          search_time
                                                                          0.378s
                                                                          details
                                                                          Expand
                                                                          smt_stats
                                                                          num checks201
                                                                          arith assert lower99
                                                                          rlimit count59930
                                                                          mk clause300
                                                                          mk bool var504
                                                                          arith assert upper1
                                                                          propagations297
                                                                          conflicts101
                                                                          arith fixed eqs2
                                                                          num allocs1070611148
                                                                          final checks100
                                                                          added eqs300
                                                                          del clause297
                                                                          memory21.690000
                                                                          max memory23.960000
                                                                          Expand
                                                                          • start[0.378s] :var_0: < 100 ==> f :var_0: = 1
                                                                          • simplify

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

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