Remove default axiom in associate array to pointer

romainbrenguier · romainbrenguier · commit 42971da4553f · 2018-03-10T13:01:07.000Z
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.
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -249,7 +249,6 @@ string_constraint_generatort::associate_char_array_to_char_pointer(
   auto insert_result =
     arrays_of_pointers_.insert(std::make_pair(char_pointer, array_sym));
   array_string_exprt result = to_array_string_expr(insert_result.first->second);
-  add_default_axioms(result);
   return result;
 }
 
@@ -410,6 +409,7 @@ array_string_exprt string_constraint_generatort::char_array_of_pointer(
   const array_typet array_type(pointer.type().subtype(), length);
   const array_string_exprt array =
     associate_char_array_to_char_pointer(pointer, array_type);
+  add_default_axioms(array);
   return array;
 }
 

Original file line number	Diff line number	Diff line change
`@@ -249,7 +249,6 @@ string_constraint_generatort::associate_char_array_to_char_pointer(`
`249`	`249`	`auto insert_result =`
`250`	`250`	`arrays_of_pointers_.insert(std::make_pair(char_pointer, array_sym));`
`251`	`251`	`array_string_exprt result = to_array_string_expr(insert_result.first->second);`
`252`		`- add_default_axioms(result);`
`253`	`252`	`return result;`
`254`	`253`	`}`
`255`	`254`
`@@ -410,6 +409,7 @@ array_string_exprt string_constraint_generatort::char_array_of_pointer(`
`410`	`409`	`const array_typet array_type(pointer.type().subtype(), length);`
`411`	`410`	`const array_string_exprt array =`
`412`	`411`	`associate_char_array_to_char_pointer(pointer, array_type);`
	`412`	`+ add_default_axioms(array);`
`413`	`413`	`return array;`
`414`	`414`	`}`
`415`	`415`