kind2-mc/kind2 — pull request #106 by kevinclancy (2014-07-16 21:45:13+00:00)
Title: Error/Bug Fix for Stateless Variable Reconstruction

Removed list_zip and list_unzip. Used List.combine and List.split instead.

Fixed a runtime error where lists of unequal length were being passed into List.combine; the problem is that I was pairing up all actuals (including oracles) with a list of formals that did not include oracles. I fixed this by appending formal oracles onto this list.

After that, there were some more errors in reconstruction. One problem was that Output streams were being reconstructed even if they were stateful. Those streams appeared in the model, but only in the calling node instance, so I fixed this by duplicating the output model in the caller and callee. The other approach would have been to remove outputs from callees, but I think this approach is probably more helpful to the user.

Another problem was that called nodes sometimes need models from callers/call ancestors in order to reconstruct their nodes. I fixed this by tracking models of all of the reconstructed node's ancestor's streams in a map called ancestors_stream_map.