Inlining a foldEdges expression appears to blow up #76
Description
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 trueInlining 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 2u32but then does not appear to ever finish.