Weird edge names in map during simulation

[alberdingk-thijm]

The following example has unusual output when I simulate it and am presented with the dictionary keys, which appear to be the correct edge number multiplied by 4096. The code doesn't actually do what it's intended to do at the moment, but that's another matter.

Input:

(* vim: set syntax=ocaml: *)

type attribute = (int, dict[tedge, int])

let nodes = 4

let edges = {
  0=1;
  1=2;
  1=3;
}

let trans e x = 
  let (d, es) = x in
  let old_count = es[e] in
  (d + 1, es[e := old_count + 1])

let merge n x1 x2 =
  let (d1, es1) = x1 in
  let (d2, es2) = x2 in
  if d1 < d2 then (d1, es1) else (d2, es2)

let init node =
  let es = createDict 0 in
  match node with
  | 0n -> (0, es)
  | _ -> (15, es)

(* Assert that no edge is used more than once by any transfer *)
let assert node x =
  let (_, es) = x in
  foldEdges (fun e x acc -> x < 2 && acc) es true

Output of ./nv -s -v examples/disjoint-paths.nv:

Processing examples/disjoint-paths.nv
Interpreted simulation took: 0.002488 secs to complete
No counterexamples found

Label(0):(0u32,[default:=0u32])
Label(1):(1u32,[0~4096:=1u32,default:=0u32])
Label(2):(2u32,[1~8192:=1u32,0~4096:=1u32,default:=0u32])
Label(3):(2u32,[1~12288:=1u32,0~4096:=1u32,default:=0u32])
Success: all assertions passed

Entire Program took: 0.003664 secs to complete

[DKLoehr]

It was an issue with our BDD encoding. We previously hardcoded the bit-size of node values, and missed a constant when we generalized, so we were encoding nodes using a different number of bits than we were using to decode.