letify: use irep_hash_mapt when hashing is expensive

Fixes: #344
Fixes: #1944

Author: kroening

regression/cbmc/Float-smt2-1/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main (void) {
+float f;
+
+    assert(f * f > 28);
+
+    return 0;
+}
+

regression/cbmc/Float-smt2-1/test.desc

@@ -0,0 +1,8 @@
+CORE smt-backend
+main.c
+--smt2
+^EXIT=10$
+^SIGNAL=0$
+--
+Tests a floating-point operation encoding for SMT2 without --fpa.
+Owing to heavy use of sharing, this requires sharing-aware hashing.

src/solvers/smt2/smt2_conv.h

@@ -16,6 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/byte_operators.h>
 
+#ifndef HASH_CODE
+#include <util/irep_hash_container.h>
+#endif
+
 #include <solvers/prop/prop_conv.h>
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
@@ -181,7 +185,12 @@ class smt2_convt:public prop_convt
     symbol_exprt let_symbol;
   };
 
+#ifdef HASH_CODE
   typedef std::unordered_map<exprt, let_count_idt, irep_hash> seen_expressionst;
+#else
+  typedef irep_hash_mapt<exprt, let_count_idt> seen_expressionst;
+#endif
+
   std::size_t let_id_count;
   static const std::size_t LET_COUNT = 2;