Inlining a foldEdges expression appears to blow up

[alberdingk-thijm]

Given the network below, NV currently appears to get stuck during the second round of inlining, following map unrolling.

(* Benchmark testing fault tolerance reachability to the destination. *)
type attribute = bool

symbolic failed : set[tedge]

let cardinality s =
  foldEdges (fun e b x -> if b then x + 1 else x) s 0

require ((cardinality failed) <= 2)

let dest = 10n

let nodes = 20

let edges = {
  3-16; (*core-0,Serial0 --> aggregation-8,Serial0*)
  13-12; (*aggregation-5,Serial3 --> edge-7,Serial1*)
  8-1; (*aggregation-16,Serial1 --> core-1,Serial3*)
  6-7; (*aggregation-17,Serial3 --> core-2,Serial1*)
  19-16; (*edge-10,Serial0 --> aggregation-8,Serial2*)
  14-3; (*aggregation-4,Serial0 --> core-0,Serial2*)
  6-4; (*aggregation-17,Serial0 --> core-3,Serial1*)
  4-13; (*core-3,Serial2 --> aggregation-5,Serial1*)
  9-18; (*edge-14,Serial0 --> aggregation-12,Serial2*)
  17-0; (*aggregation-13,Serial3 --> edge-15,Serial1*)
  8-2; (*aggregation-16,Serial2 --> edge-18,Serial0*)
  3-14; (*core-0,Serial2 --> aggregation-4,Serial0*)
  18-3; (*aggregation-12,Serial0 --> core-0,Serial1*)
  1-8; (*core-1,Serial3 --> aggregation-16,Serial1*)
  7-15; (*core-2,Serial0 --> aggregation-9,Serial3*)
  15-5; (*aggregation-9,Serial2 --> edge-11,Serial1*)
  18-0; (*aggregation-12,Serial3 --> edge-15,Serial0*)
  10-8; (*edge-19,Serial0 --> aggregation-16,Serial3*)
  5-16; (*edge-11,Serial0 --> aggregation-8,Serial3*)
  6-2; (*aggregation-17,Serial1 --> edge-18,Serial1*)
  7-17; (*core-2,Serial3 --> aggregation-13,Serial0*)
  15-4; (*aggregation-9,Serial0 --> core-3,Serial0*)
  0-18; (*edge-15,Serial0 --> aggregation-12,Serial3*)
  7-6; (*core-2,Serial1 --> aggregation-17,Serial3*)
  16-5; (*aggregation-8,Serial3 --> edge-11,Serial0*)
  13-7; (*aggregation-5,Serial0 --> core-2,Serial2*)
  16-19; (*aggregation-8,Serial2 --> edge-10,Serial0*)
  14-11; (*aggregation-4,Serial2 --> edge-6,Serial0*)
  11-13; (*edge-6,Serial1 --> aggregation-5,Serial2*)
  3-18; (*core-0,Serial1 --> aggregation-12,Serial0*)
  9-17; (*edge-14,Serial1 --> aggregation-13,Serial2*)
  6-10; (*aggregation-17,Serial2 --> edge-19,Serial1*)
  13-4; (*aggregation-5,Serial1 --> core-3,Serial2*)
  2-6; (*edge-18,Serial1 --> aggregation-17,Serial1*)
  18-1; (*aggregation-12,Serial1 --> core-1,Serial1*)
  15-19; (*aggregation-9,Serial1 --> edge-10,Serial1*)
  1-14; (*core-1,Serial2 --> aggregation-4,Serial1*)
  2-8; (*edge-18,Serial0 --> aggregation-16,Serial2*)
  8-3; (*aggregation-16,Serial0 --> core-0,Serial3*)
  17-4; (*aggregation-13,Serial1 --> core-3,Serial3*)
  18-9; (*aggregation-12,Serial2 --> edge-14,Serial0*)
  0-17; (*edge-15,Serial1 --> aggregation-13,Serial3*)
  7-13; (*core-2,Serial2 --> aggregation-5,Serial0*)
  4-17; (*core-3,Serial3 --> aggregation-13,Serial1*)
  14-1; (*aggregation-4,Serial1 --> core-1,Serial2*)
  8-10; (*aggregation-16,Serial3 --> edge-19,Serial0*)
  10-6; (*edge-19,Serial1 --> aggregation-17,Serial2*)
  1-18; (*core-1,Serial1 --> aggregation-12,Serial1*)
  15-7; (*aggregation-9,Serial3 --> core-2,Serial0*)
  11-14; (*edge-6,Serial0 --> aggregation-4,Serial2*)
  12-13; (*edge-7,Serial1 --> aggregation-5,Serial3*)
  17-7; (*aggregation-13,Serial0 --> core-2,Serial3*)
  3-8; (*core-0,Serial3 --> aggregation-16,Serial0*)
  17-9; (*aggregation-13,Serial2 --> edge-14,Serial1*)
  13-11; (*aggregation-5,Serial2 --> edge-6,Serial1*)
  16-1; (*aggregation-8,Serial1 --> core-1,Serial0*)
  16-3; (*aggregation-8,Serial0 --> core-0,Serial0*)
  4-15; (*core-3,Serial0 --> aggregation-9,Serial0*)
  19-15; (*edge-10,Serial1 --> aggregation-9,Serial1*)
  12-14; (*edge-7,Serial0 --> aggregation-4,Serial3*)
  14-12; (*aggregation-4,Serial3 --> edge-7,Serial0*)
  1-16; (*core-1,Serial0 --> aggregation-8,Serial1*)
  4-6; (*core-3,Serial1 --> aggregation-17,Serial0*)
  5-15; (*edge-11,Serial1 --> aggregation-9,Serial2*)
}

let init n = if n = dest then true else false

let trans e x = if failed[e] then false else x

let merge n x y = x || y

let assert_node node x = x

 (* {edge-15=0, core-1=1, edge-18=2, core-0=3, core-3=4, edge-11=5,
aggregation-17=6, core-2=7, aggregation-16=8, edge-14=9, edge-19=10, edge-6=11,
edge-7=12, aggregation-5=13, aggregation-4=14, aggregation-9=15,
aggregation-8=16, aggregation-13=17, aggregation-12=18,
edge-10=19}*)
let sol = solution {init = init; trans = trans; merge = merge}

assert foldNodes (fun k v acc -> acc && assert_node k v) sol true

Inlining starts on the following expression:

require ((match failed~161 with
 | (UnrollingFoldVar~198,UnrollingFoldVar~199,UnrollingFoldVar~200,UnrollingFoldVar~201,UnrollingFoldVar~202,UnrollingFoldVar~203,UnrollingFoldVar~204,UnrollingFoldVar~205,UnrollingFoldVar~206,UnrollingFoldVar~207,UnrollingFoldVar~208,UnrollingFoldVar~209,UnrollingFoldVar~210,UnrollingFoldVar~211,UnrollingFoldVar~212,UnrollingFoldVar~213,UnrollingFoldVar~214,UnrollingFoldVar~215,UnrollingFoldVar~216,UnrollingFoldVar~217,UnrollingFoldVar~218,UnrollingFoldVar~219,UnrollingFoldVar~220,UnrollingFoldVar~221,UnrollingFoldVar~222,UnrollingFoldVar~223,UnrollingFoldVar~224,UnrollingFoldVar~225,UnrollingFoldVar~226,UnrollingFoldVar~227,UnrollingFoldVar~228,UnrollingFoldVar~229,UnrollingFoldVar~230,UnrollingFoldVar~231,UnrollingFoldVar~232,UnrollingFoldVar~233,UnrollingFoldVar~234,UnrollingFoldVar~235,UnrollingFoldVar~236,UnrollingFoldVar~237,UnrollingFoldVar~238,UnrollingFoldVar~239,UnrollingFoldVar~240,UnrollingFoldVar~241,UnrollingFoldVar~242,UnrollingFoldVar~243,UnrollingFoldVar~244,UnrollingFoldVar~245,UnrollingFoldVar~246,UnrollingFoldVar~247,UnrollingFoldVar~248,UnrollingFoldVar~249,UnrollingFoldVar~250,UnrollingFoldVar~251,UnrollingFoldVar~252,UnrollingFoldVar~253,UnrollingFoldVar~254,UnrollingFoldVar~255,UnrollingFoldVar~256,UnrollingFoldVar~257,UnrollingFoldVar~258,UnrollingFoldVar~259,UnrollingFoldVar~260,UnrollingFoldVar~261) -> (((((fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) )) 19~16 ) UnrollingFoldVar~261 ) (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 19~15  UnrollingFoldVar~260  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 18~9  UnrollingFoldVar~259  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 18~3  UnrollingFoldVar~258  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 18~1  UnrollingFoldVar~257  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 18~0  UnrollingFoldVar~256  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 17~9  UnrollingFoldVar~255  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 17~7  UnrollingFoldVar~254  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 17~4  UnrollingFoldVar~253  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 17~0  UnrollingFoldVar~252  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 16~19  UnrollingFoldVar~251  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 16~5  UnrollingFoldVar~250  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 16~3  UnrollingFoldVar~249  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 16~1  UnrollingFoldVar~248  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 15~19  UnrollingFoldVar~247  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 15~7  UnrollingFoldVar~246  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 15~5  UnrollingFoldVar~245  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 15~4  UnrollingFoldVar~244  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 14~12  UnrollingFoldVar~243  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 14~11  UnrollingFoldVar~242  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 14~3  UnrollingFoldVar~241  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 14~1  UnrollingFoldVar~240  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 13~12  UnrollingFoldVar~239  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 13~11  UnrollingFoldVar~238  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 13~7  UnrollingFoldVar~237  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 13~4  UnrollingFoldVar~236  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 12~14  UnrollingFoldVar~235  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 12~13  UnrollingFoldVar~234  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 11~14  UnrollingFoldVar~233  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 11~13  UnrollingFoldVar~232  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 10~8  UnrollingFoldVar~231  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 10~6  UnrollingFoldVar~230  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 9~18  UnrollingFoldVar~229  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 9~17  UnrollingFoldVar~228  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 8~10  UnrollingFoldVar~227  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 8~3  UnrollingFoldVar~226  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 8~2  UnrollingFoldVar~225  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 8~1  UnrollingFoldVar~224  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 7~17  UnrollingFoldVar~223  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 7~15  UnrollingFoldVar~222  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 7~13  UnrollingFoldVar~221  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 7~6  UnrollingFoldVar~220  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 6~10  UnrollingFoldVar~219  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 6~7  UnrollingFoldVar~218  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 6~4  UnrollingFoldVar~217  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 6~2  UnrollingFoldVar~216  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 5~16  UnrollingFoldVar~215  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 5~15  UnrollingFoldVar~214  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 4~17  UnrollingFoldVar~213  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 4~15  UnrollingFoldVar~212  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 4~13  UnrollingFoldVar~211  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 4~6  UnrollingFoldVar~210  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 3~18  UnrollingFoldVar~209  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 3~16  UnrollingFoldVar~208  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 3~14  UnrollingFoldVar~207  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 3~8  UnrollingFoldVar~206  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 2~8  UnrollingFoldVar~205  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 2~6  UnrollingFoldVar~204  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 1~18  UnrollingFoldVar~203  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 1~16  UnrollingFoldVar~202  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 1~14  UnrollingFoldVar~201  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 1~8  UnrollingFoldVar~200  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 0~18  UnrollingFoldVar~199  (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then
x~175 +u32 1u32 else
x~175 ) ) ) 0~17  UnrollingFoldVar~198  0u32                                                                )
)) <=u32 2u32

but then does not appear to ever finish.