Fix consistency error in SSA level 1 renaming

a5bc493 introduced cases where information in the frame may become
inconsistent with the actual renaming being used, as shown in the regression
test.

Author: tautschnig

regression/cbmc/Local_out_of_scope2/main.c

@@ -0,0 +1,25 @@
+inline void foo(int x)
+{
+}
+
+void bar()
+{
+  foo(0);
+}
+
+void foobar()
+{
+  // different argument values must not cause an inconsistency in the
+  // equation system
+  foo(0);
+  bar();
+  foo(1);
+}
+
+int main()
+{
+  foobar();
+  foobar();
+  __CPROVER_assert(0, "");
+  return 0;
+}

regression/cbmc/Local_out_of_scope2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-symex/symex_function_call.cpp

@@ -501,9 +501,9 @@ void goto_symext::locality(
     while(state.l1_history.find(l1_name)!=state.l1_history.end())
     {
       state.level1.increase_counter(l0_name);
+      ++offset;
       ssa.set_level_1(frame_nr+offset);
       l1_name=ssa.get_identifier();
-      ++offset;
     }
 
     // now unique -- store