Symex target equation: convert assignments first

Converting assignments (equalities) permits the optimisation of re-using
variables generated for a right-hand side to represent the left-hand
side. Consequently, no free variables need to be introduced for those
left-hand sides when the symbol is seen. If converting, e.g., guards
before assignments, no such optimisation is possible.

Author: tautschnig

src/goto-symex/symex_target_equation.cpp

@@ -332,9 +332,13 @@ void symex_target_equationt::convert_without_assertions(
     hardness.register_ssa_size(SSA_steps.size());
   });
 
-  convert_guards(decision_procedure);
+  // The order matters here: the decision procedure may be able to re-use
+  // variables obtained from constructing the right-hand side of an assignment
+  // for the left-hand side. Those left-hand sides might then appear in guards
+  // or assumptions, so do assignments and decls before any of the others.
   convert_assignments(decision_procedure);
   convert_decls(decision_procedure);
+  convert_guards(decision_procedure);
   convert_assumptions(decision_procedure);
   convert_goto_instructions(decision_procedure);
   convert_function_calls(decision_procedure);