Skip to content

Commit 42971da

Browse files
Remove default axiom in associate array to pointer
These default axioms are not useful, as constraints are already added on input strings and fresh strings. This also moves default axoims from associate_char_array_of_pointer to char_array_of_pointer, because the first function will be pulled out of the class.
1 parent f5adb47 commit 42971da

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/solvers/refinement/string_constraint_generator_main.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -249,7 +249,6 @@ string_constraint_generatort::associate_char_array_to_char_pointer(
249249
auto insert_result =
250250
arrays_of_pointers_.insert(std::make_pair(char_pointer, array_sym));
251251
array_string_exprt result = to_array_string_expr(insert_result.first->second);
252-
add_default_axioms(result);
253252
return result;
254253
}
255254

@@ -410,6 +409,7 @@ array_string_exprt string_constraint_generatort::char_array_of_pointer(
410409
const array_typet array_type(pointer.type().subtype(), length);
411410
const array_string_exprt array =
412411
associate_char_array_to_char_pointer(pointer, array_type);
412+
add_default_axioms(array);
413413
return array;
414414
}
415415

0 commit comments

Comments
 (0)