In some cases the parenthesis don't match up in the goals for the VC. This happens in both the web interface and when outputting to .asrt files. Here is an example:
VC: 0_2:
Requires Clause of Push in Procedure Do_Nothing: Do_Nothing_Realiz.rb(8)
Goal:
(|S'| + 1) <= Max_Depth)
Given:
1: (Last_Char_Num > 0)
2: (min_int <= 0)
3: (0 < max_int)
4: (1 <= Max_Depth)
5: (min_int <= Max_Depth) and (Max_Depth <= max_int)
6: (|S| <= Max_Depth)
7: (|S| > 0)
8: S = (<Next_Entry'> o S')
Notice the right paren after Max_Depth with no matching left paren. I ran this test on Do_Nothing_Realiz.rb with the flags -vcs and -listvcs. It happens on both realizations and facilities.
Works on my branch of the compiler using the Netbeans WebUI setup... It could be that I changed something on my end to make that work. Will test my jar using the Old-Resolve machine to be sure.