Rewrite_star in pbessolve prints different output than before

[maramiulescu]

In the debug output of pbessolve, in the second iteration, the rewrite_star step seems to have changed. We now see some values named "@rewr_var ..." in the output and the other equation parameters are not "filled in" like before.

Do we want to print this output?

To reproduce
Run (using proc.txt):

txt2pbes proc.txt proc.pbes
pbessolve proc.pbes -d

In the debug output, when the second iteration begins, see

Removing unnecessary example information for other player.
[debug]   X = Y(1, 0, true), psi = (val(!(s1_P == @rewr_var)) || Y(@rewr_var1, n_P, !b_P) && Zpos_0_a3(s1_P, n_P, b_P, @rewr_var1, n_P, !b_P)) && (val(!(s1_P == @rewr_var1)) || Y(@rewr_var, n_P, b_P) && Zpos_1_a2(s1_P, n_P, b_P, @rewr_var, n_P, b_P)) && (val(!(s1_P == @rewr_var1)) || Y(@rewr_var1, (n_P + @rewr_var1) mod @rewr_var2, b_P) && Zpos_2_a1(s1_P, n_P, b_P, n_P, @rewr_var1, (n_P + @rewr_var1) mod @rewr_var2, b_P)) && (val(s1_P == @rewr_var) && Zpos_0_a3(s1_P, n_P, b_P, @rewr_var1, n_P, !b_P) || val(s1_P == @rewr_var1) && Zpos_1_a2(s1_P, n_P, b_P, @rewr_var, n_P, b_P) || val(s1_P == @rewr_var1) && Zpos_2_a1(s1_P, n_P, b_P, n_P, @rewr_var1, (n_P + @rewr_var1) mod @rewr_var2, b_P))

which previously looked like

Removing unnecessary example information for other player.
[debug]   X = Y(1, 0, true), psi = Y(2, 0, true) && Zpos_1_a2(1, 0, true, 2, 0, true) && Y(1, 1, true) && Zpos_2_a1(1, 0, true, 0, 1, 1, true) && (Zpos_1_a2(1, 0, true, 2, 0, true) || Zpos_2_a1(1, 0, true, 0, 1, 1, true))

[mlaveaux]

I can reproduce this issue. Looking at the final structure graph it does seem like the expressions are rewritten eventually, but not yet when psi is printed in pbesinst_lazy_counter_example:

[debug]   Solved structure graph 
[debug]      0 vertex(formula = Y(1, 0, true), decoration = conjunction, rank = 0, predecessors = [ 9, 13 ], successors = [ 1, 2, 3, 4, 5 ], strategy = undefined)
[debug]      1 vertex(formula = Y(2, 0, true), decoration = conjunction, rank = 0, predecessors = [ 0 ], successors = [ 6, 7 ], strategy = undefined)
[debug]      2 vertex(formula = Y(1, 1, true), decoration = conjunction, rank = 0, predecessors = [ 0, 24 ], successors = [ 8, 9, 10, 11, 12 ], strategy = undefined)
[debug]      3 vertex(formula = Zpos_1_a2(1, 0, true, 2, 0, true), decoration = true, rank = 0, predecessors = [ 0, 5 ], successors = [  ], strategy = undefined)
[debug]      4 vertex(formula = Zpos_2_a1(1, 0, true, 0, 1, 1, true), decoration = true, rank = 0, predecessors = [ 0, 5 ], successors = [  ], strategy = undefined)
[debug]      5 vertex(formula = Zpos_1_a2(1, 0, true, 2, 0, true) || Zpos_2_a1(1, 0, true, 0, 1, 1, true), decoration = disjunction, rank = undefined, predecessors = [ 0 ], successors = [ 3, 4 ], strategy = 3)
...