run models/dijkstra.als

when run with both -r and -u options
(-r is template detection and -u is skolemization inside
 universal quantifiers), a solution is returned that
 does not satisfy the original formula.
either of these options by itself works fine.

FIXED: not a real bug.  the boolean formula evaluation visitor (alloy.bool.Eval_V)
did not correctly handle switchable constants; now does (hopefully).
so, the assertion was failing, but there was no real bug.

UPDATE: bug reappears when scope is set to 3
