String refinement: support pointers

We need to use bv_pointerst to convert address_of expressions.

Author: tautschnig

jbmc/regression/strings-smoke-tests/java_set_length/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 test_set_length
 --function test_set_length.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$

src/solvers/strings/string_constraint.cpp

@@ -11,7 +11,7 @@ Author: Diffblue Ltd.
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
-#include <solvers/flattening/boolbv.h>
+#include <solvers/flattening/bv_pointers.h>
 #include <solvers/sat/satcheck.h>
 
 /// Runs a solver instance to verify whether an expression can only be
@@ -24,7 +24,7 @@ static bool cannot_be_neg(const exprt &expr, message_handlert &message_handler)
   satcheck_no_simplifiert sat_check(message_handler);
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
-  boolbvt solver{ns, sat_check, message_handler};
+  bv_pointerst solver{ns, sat_check, message_handler};
   const exprt zero = from_integer(0, expr.type());
   const binary_relation_exprt non_neg(expr, ID_lt, zero);
   solver << non_neg;

src/solvers/strings/string_refinement.cpp

@@ -1912,7 +1912,7 @@ static optionalt<exprt> find_counter_example(
   message_handlert &message_handler)
 {
   satcheck_no_simplifiert sat_check(message_handler);
-  boolbvt solver(ns, sat_check, message_handler);
+  bv_pointerst solver(ns, sat_check, message_handler);
   solver << axiom;
 
   if(solver() == decision_proceduret::resultt::D_SATISFIABLE)