Reduce variable equivalences unnecessarily generated by set_literals

There is no need to call set_literals for `A == A`, and if we end up
in set_literals via another code path we can still avoid generating the
trivially-true equality of `l == l`.

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -483,10 +483,12 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
 
     const bvt &bv1=convert_bv(expr.rhs());
 
-    const irep_idt &identifier=
-      to_symbol_expr(expr.lhs()).get_identifier();
+    if(expr.rhs() != expr.lhs())
+    {
+      const irep_idt &identifier = to_symbol_expr(expr.lhs()).get_identifier();
 
-    map.set_literals(identifier, type, bv1);
+      map.set_literals(identifier, type, bv1);
+    }
 
     if(freeze_all)
       set_frozen(bv1);

src/solvers/flattening/boolbv_map.cpp

@@ -110,7 +110,11 @@ void boolbv_mapt::set_literals(
       INVARIANT(
         bit < map_entry.literal_map.size(), "bit index shall be within bounds");
 
-      prop.set_equal(map_entry.literal_map[bit], literal);
+      if(map_entry.literal_map[bit] != literal)
+      {
+        // this branch should be avoided wherever possible
+        prop.set_equal(map_entry.literal_map[bit], literal);
+      }
     }
   }
 }