smt2 frontend: let identifiers must be globally unique

The solver backend assumes that identifiers used in let expressions are
globally unique.  The renamed identifiers are now retained in the id_map to
ensure that they are not re-used.

This enables 11 regression tests to pass.

Author: Daniel Kroening

scripts/delete_failing_smt2_solver_tests

@@ -7,7 +7,6 @@ rm Bitfields3/test.desc
 rm Empty_struct1/test.desc
 rm Endianness4/test.desc
 rm Endianness6/test.desc
-rm Endianness7/test.desc
 rm Float-div2/test.desc
 rm Float-div3/test.desc
 rm Float-no-simp1/test.desc
@@ -37,25 +36,19 @@ rm Linking4/test.desc
 rm Linking7/test.desc
 rm Linking7/member-name-mismatch.desc
 rm Malloc23/test.desc
-rm Malloc24/test.desc
-rm Memory_leak2/test.desc
 rm Multi_Dimensional_Array2/test.desc
 rm Overflow_Leftshift1/test.desc
 rm Overflow_Subtraction1/test.desc
 rm Pointer_Arithmetic11/test.desc
 rm Pointer_byte_extract2/test.desc
-rm Pointer_byte_extract3/test.desc
-rm Pointer_byte_extract4/test.desc
 rm Pointer_byte_extract5/no-simplify.desc
 rm Pointer_byte_extract5/test.desc
-rm Pointer_byte_extract7/test.desc
 rm Pointer_byte_extract9/test.desc
 rm Promotion3/test.desc
 rm Quantifiers-assertion/test.desc
 rm Quantifiers-assignment/test.desc
 rm Quantifiers-invalid-var-range/test.desc
 rm Quantifiers-type/test.desc
-rm Struct_Bytewise2/test.desc
 rm Union_Initialization1/test.desc
 rm address_space_size_limit1/test.desc
 rm array-function-parameters/test.desc
@@ -71,20 +64,16 @@ rm byte_update8/test.desc
 rm byte_update9/test.desc
 rm compact-trace/test.desc
 rm dynamic_size1/stack_object.desc
-rm equality_through_struct_containing_arrays1/test.desc
-rm equality_through_struct_containing_arrays2/test.desc
 rm graphml_witness1/test.desc
 rm integer-assignments1/test.desc
 rm memory_allocation1/test.desc
 rm pointer-function-parameters-struct-mutual-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion-2/test.desc
-rm pointer-function-parameters-struct-simple-recursion-3/test.desc
 rm scanf1/test.desc
 rm stack-trace/test.desc
 rm struct6/test.desc
 rm struct7/test.desc
-rm struct9/test.desc
 rm trace-values/trace-values.desc
 rm trace_show_function_calls/test.desc
 rm union12/test.desc

src/solvers/smt2/smt2_parser.cpp

@@ -206,9 +206,8 @@ exprt smt2_parsert::let_expression()
     result=let;
   }
 
-  // remove bindings from id_map
-  for(const auto &b : bindings)
-    id_map.erase(b.first);
+  // we keep these in the id_map in order to retain globally
+  // unique identifiers
 
   // restore renamings
   renaming_map=old_renaming_map;