Merge pull request diffblue#3366 from tautschnig/vs-member-init

Add missing member initializers of string_constraintst-typed value [blocks: diffblue#2310]

Author: tautschnig

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -571,8 +571,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_char_at(
   PRECONDITION(f.arguments().size() == 2);
   array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
   symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
-  const exprt constraint = equal_exprt(char_sym, str[f.arguments()[1]]);
-  return {char_sym, {{constraint}}};
+  string_constraintst constraints;
+  constraints.existential = {equal_exprt(char_sym, str[f.arguments()[1]])};
+  return {std::move(char_sym), std::move(constraints)};
 }
 
 exprt minimum(const exprt &a, const exprt &b)

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -136,10 +136,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_empty(
 
   symbol_exprt is_empty = fresh_symbol("is_empty");
   array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]);
-  std::vector<exprt> constraints;
-  constraints.push_back(implies_exprt(is_empty, length_eq(s0, 0)));
-  constraints.push_back(implies_exprt(length_eq(s0, 0), is_empty));
-  return {typecast_exprt(is_empty, f.type()), {constraints}};
+  string_constraintst constraints;
+  constraints.existential = {implies_exprt(is_empty, length_eq(s0, 0)),
+                             implies_exprt(length_eq(s0, 0), is_empty)};
+  return {typecast_exprt(is_empty, f.type()), std::move(constraints)};
 }
 
 /// Test if the target is a suffix of the string

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -312,8 +312,10 @@ std::pair<exprt, string_constraintst> add_axioms_from_char(
   const array_string_exprt &res,
   const exprt &c)
 {
-  const and_exprt lemma(equal_exprt(res[0], c), length_eq(res, 1));
-  return {from_integer(0, get_return_code_type()), {{lemma}}};
+  string_constraintst constraints;
+  constraints.existential = {
+    and_exprt(equal_exprt(res[0], c), length_eq(res, 1))};
+  return {from_integer(0, get_return_code_type()), std::move(constraints)};
 }
 
 /// Add axioms making the return value true if the given string is a correct