Pieces of solution values that should have node types are frequently printed as integers instead -- run the below program with the -v flag for an example. This is presumably because Z3 returns integer values for everything, and we never convert them to back to nodes. Notice that key values DO print as nodes, since they are replaced during map unrolling rather than obtained from SMT.
type attribute = dict[tnode, tnode]
let nodes = 1
let edges = { }
let merge node x y = x
let trans edge x = x
let init node = createDict 0n
Pieces of solution values that should have node types are frequently printed as integers instead -- run the below program with the -v flag for an example. This is presumably because Z3 returns integer values for everything, and we never convert them to back to nodes. Notice that key values DO print as nodes, since they are replaced during map unrolling rather than obtained from SMT.