bv_utilst::equal: stop early when the result will be false

There is no need to create any further bit-level equalities when the
result will be false anyway. On aws-c-common/aws_hash_iter_next, this
reduces the number of Boolean variables from 2291304 to 584628, and the
time spent in CaDiCaL from 191 seconds to 22 seconds.

Author: tautschnig

src/solvers/flattening/bv_utils.cpp

@@ -1185,6 +1185,16 @@ literalt bv_utilst::equal(const bvt &op0, const bvt &op1)
     return equal_const(op0, op1);
   #endif
 
+  // If the eventual result would be "false" anyway, avoid constructing
+  // equalities that would end up not affecting the satisfiability of the
+  // formula (effectively doing preprocessing steps that the SAT solver would
+  // otherwise have to undertake).
+  for(std::size_t i = 0; i < op0.size(); i++)
+  {
+    if(op0[i] != op1[i] && op0[i].var_no() == op1[i].var_no())
+      return const_literal(false);
+  }
+
   bvt equal_bv;
   equal_bv.resize(op0.size());