Skip to content

Commit 04b016b

Browse files
committed
Add missing member initializers of string_constraintst-typed value
add_axioms_for_char_at, add_axioms_for_is_empty, add_axioms_from_char only initialized one of the three vectors.
1 parent 8d3c9aa commit 04b016b

File tree

3 files changed

+3
-3
lines changed

3 files changed

+3
-3
lines changed

src/solvers/refinement/string_constraint_generator_main.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -576,7 +576,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_char_at(
576576
array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
577577
symbol_exprt char_sym = fresh_symbol("char", str.type().subtype());
578578
const exprt constraint = equal_exprt(char_sym, str[f.arguments()[1]]);
579-
return {char_sym, {{constraint}}};
579+
return {char_sym, {{constraint}, {}, {}}};
580580
}
581581

582582
exprt minimum(const exprt &a, const exprt &b)

src/solvers/refinement/string_constraint_generator_testing.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_is_empty(
139139
std::vector<exprt> constraints;
140140
constraints.push_back(implies_exprt(is_empty, length_eq(s0, 0)));
141141
constraints.push_back(implies_exprt(length_eq(s0, 0), is_empty));
142-
return {typecast_exprt(is_empty, f.type()), {constraints}};
142+
return {typecast_exprt(is_empty, f.type()), {constraints, {}, {}}};
143143
}
144144

145145
/// Test if the target is a suffix of the string

src/solvers/refinement/string_constraint_generator_valueof.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -332,7 +332,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_char(
332332
const exprt &c)
333333
{
334334
const and_exprt lemma(equal_exprt(res[0], c), length_eq(res, 1));
335-
return {from_integer(0, get_return_code_type()), {{lemma}}};
335+
return {from_integer(0, get_return_code_type()), {{lemma}, {}, {}}};
336336
}
337337

338338
/// Add axioms making the return value true if the given string is a correct

0 commit comments

Comments
 (0)