adjust debugging code to print SMT var name comment as prefix
This code is disabled, but was intended to allow developers to print the Murphi name of a variable as a following comment to the SMT symbol used. This is useful for debugging subtle problems in the SMT translation. Following commit 5bb6144f, forall expressions used a second variable of the form "s42_iteration". Because we append the "_iteration" text this broke the debugging support here. I.e. with the debug flag enabled, this would be printed as something like "s42 ; foo\n_iteration". We now print the comment *preceding* the SMT variable instead of following, so this debugging functionality should once again work.
parent
d5cb6a6f
Please register or sign in to comment