boolbv backend honors forall/exists scopes

The boolbv backend now introduces new names for the bound symbols.  This
matches the new behavior for let expressions.

Author: kroening

src/solvers/flattening/boolbv.cpp

@@ -552,6 +552,29 @@ bool boolbvt::is_unbounded_array(const typet &type) const
   return false;
 }
 
+binding_exprt::variablest boolbvt::fresh_binding(const binding_exprt &binding)
+{
+  // to ensure freshness of the new identifiers
+  scope_counter++;
+
+  binding_exprt::variablest result;
+  result.reserve(binding.variables().size());
+
+  for(const auto &binding : binding.variables())
+  {
+    const auto &old_identifier = binding.get_identifier();
+
+    // produce a new identifier
+    const irep_idt new_identifier =
+      "boolbvt::scope::" + std::to_string(scope_counter) +
+      "::" + id2string(old_identifier);
+
+    result.emplace_back(new_identifier, binding.type());
+  }
+
+  return result;
+}
+
 void boolbvt::print_assignment(std::ostream &out) const
 {
   arrayst::print_assignment(out);

src/solvers/flattening/boolbv.h

@@ -274,6 +274,9 @@ class boolbvt:public arrayst
 
   // scopes
   std::size_t scope_counter = 0;
+
+  /// create new, unique variables for the given binding
+  binding_exprt::variablest fresh_binding(const binding_exprt &);
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H

src/solvers/flattening/boolbv_quantifier.cpp

@@ -12,7 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/optional.h>
+#include <util/range.h>
 #include <util/replace_expr.h>
+#include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
 
 /// A method to detect equivalence between experts that can contain typecast
@@ -206,6 +208,22 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
 {
   PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
 
+  // We first worry about the scoping of the symbols bound by the quantifier.
+  auto fresh_symbols = fresh_binding(src);
+
+  // replace in where()
+  replace_symbolt replace_symbol;
+
+  for(const auto &pair : make_range(src.variables()).zip(fresh_symbols))
+    replace_symbol.insert(pair.first, pair.second);
+
+  exprt renamed_where = src.where();
+  replace_symbol(renamed_where);
+
+  // produce new quantifier expression
+  auto new_src =
+    quantifier_exprt(src.id(), std::move(fresh_symbols), renamed_where);
+
   const auto res = instantiate_quantifier(src, ns);
 
   if(res)